Dates below proofs in set.mm
50 views
Skip to first unread message
Norman Megill
May 13, 2017, 3:51:46 PM5/13/17
to Metamath
Starting with metamath.exe version 0.142
http://us2.metamath.org:88/index.html#mmprog
the redundant dates below the proofs are no longer checked nor used for anything.
If someone is using the dates for another purpose, let me know. Otherwise I will delete them from set.mm in a few days, reducing the set.mm size by 850kB.
"save new_proof" and "save proof" now add the "(Contributed by ...)" date automatically to a theorem's comment if it is missing, provided the proof is complete. The default contributor is called "?who?", which can be updated with a global edit to replace it with your name. "verify markup */f" will warn if any "?who?"s aren't updated. Since this is a trivial edit, needed only once before a GitHub submission, I don't plan to add a "set contributor" command unless there is a clamoring demand for yet another command to remember.
If you work by manually pasting proofs into set.mm, then when you are done you can run "save proof */c/f" to add all missing contributor dates, followed by a global edit replacing "?who?" with your name.
Norm
http://us2.metamath.org:88/index.html#mmprog
the redundant dates below the proofs are no longer checked nor used for anything.
If someone is using the dates for another purpose, let me know. Otherwise I will delete them from set.mm in a few days, reducing the set.mm size by 850kB.
"save new_proof" and "save proof" now add the "(Contributed by ...)" date automatically to a theorem's comment if it is missing, provided the proof is complete. The default contributor is called "?who?", which can be updated with a global edit to replace it with your name. "verify markup */f" will warn if any "?who?"s aren't updated. Since this is a trivial edit, needed only once before a GitHub submission, I don't plan to add a "set contributor" command unless there is a clamoring demand for yet another command to remember.
If you work by manually pasting proofs into set.mm, then when you are done you can run "save proof */c/f" to add all missing contributor dates, followed by a global edit replacing "?who?" with your name.
Norm
Norman Megill
May 19, 2017, 12:41:09 AM5/19/17
to Metamath
Version 0.144 of the metamath program http://us2.metamath.org:88/index.html#mmprog adds a "set contributor" command. Its use is optional; if it isn't used, the contributor will be "?who?" as before (which will trigger a warning in "verify markup */f" if you forget to update it by hand).
Old .mm's that have the date only below the proof can be updated with "save proof */fast/compressed". If there is a date below the proof but no contributor, a contributor tag will be added using the date below the proof. If there are two dates below the proof, both a contributor tag and a reviser tag will be added using those dates. The contributor name will be taken from the "set contributor" command if that command was used; otherwise it will be "?who?". The reviser name will always be "?who?" and must be updated by hand ("verify markup" will warn if this wasn't done). If the proof was shortened, "Revised by" should be changed by hand to "Proof shortened by".
After an old .mm is updated as above, the date(s) below a proof are obsolete and may be deleted.
Norm
Old .mm's that have the date only below the proof can be updated with "save proof */fast/compressed". If there is a date below the proof but no contributor, a contributor tag will be added using the date below the proof. If there are two dates below the proof, both a contributor tag and a reviser tag will be added using those dates. The contributor name will be taken from the "set contributor" command if that command was used; otherwise it will be "?who?". The reviser name will always be "?who?" and must be updated by hand ("verify markup" will warn if this wasn't done). If the proof was shortened, "Revised by" should be changed by hand to "Proof shortened by".
After an old .mm is updated as above, the date(s) below a proof are obsolete and may be deleted.
Norm
Norman Megill
May 19, 2017, 8:11:42 AM5/19/17
to Metamath
All dates below proofs have been removed from set.mm starting with develop commit 732f3a0.
https://github.com/metamath/set.mm/commits/develop
Norm
https://github.com/metamath/set.mm/commits/develop
Norm
Reply all
Reply to author
Forward
0 new messages