Metamath distribution

[Mario Carneiro]

This is to give more visibility to issue https://github.com/metamath/metamath-exe/issues/19 . This came up when I put a .gitignore in the metamath-exe repo: We currently distribute the metamath sources via tar file, and it would be odd to distribute the .gitignore as well.

I think we should move to a release process entirely hosted on github, with the web site pointing to the https://github.com/metamath/metamath-exe/releases page, which will be semi-automatically populated with releases built in CI.

[Glauco]

Running a "verify markup" with a recent set.mm I'm getting a

There is no "Version of " comment at the top of the file

warning. It looks like the date is not at the top of the file anymore (as it was discussed some time ago, in this forum).

I'm on Version 0.198 7-Aug-2021 , that's the current one (according to the metamath.org page).

I've checked

https://github.com/metamath/metamath-exe/releases

but there aren't any releases, yet.

Will CI block my PR ?

Glauco

[Jim Kingdon]

No, because CI runs scripts/verify --top_date_skip which includes VERIFY MARKUP * / TOP_DATE_SKIP

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d1f1e874-d61f-4d80-a8bc-96bfbc0e5f38n%40googlegroups.com.

[Benoit]

This is the result of https://github.com/metamath/set.mm/pull/2392

In MM, it suffices to type "MM> v m */t/f" to obtain the "top_date_skip" and "file_skip" behavior.  I guess this behavior should eventually be made default (while keeping the useless options /top_date_skip and /file_skip for compatibility), and options /top_date_check and /file_check should be created.

Benoît

[Mario Carneiro]

Could someone summarize the design changes required in an issue on the metamath-exe repo? I think I know how to do the change but I'm not sure what flags we're adding or deleting or how the defaults change.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7979554e-9af8-4fc2-8d16-295e09b4c662n%40googlegroups.com.

[Benoit]

On Monday, January 3, 2022 at 5:55:46 AM UTC+1 di....@gmail.com wrote:

Could someone summarize the design changes required in an issue on the metamath-exe repo? I think I know how to do the change but I'm not sure what flags we're adding or deleting or how the defaults change.

This is now https://github.com/metamath/metamath-exe/issues/28

Benoît