Closed GinoGiotto closed 6 months ago
digama0
commented
6 months ago Could you try this on the latest version? I was not able to reproduce (running the latest metamath-knife on your branch produces a discouraged file containing Proof modification of "19.21a3con13vVD" is discouraged (107 steps). among other things).
GinoGiotto
commented
6 months ago I believe I already had the most recent metamath-knife version, but to be sure I did the following:
I downloaded the zip file from https://github.com/metamath/metamath-knife
I extracted the files
I executed cargo build --release on the extracted folder.
I renamed the produced executable metamath-knife-test to be sure I wasn't executing the one I already installed.
Then I created a new branch discouraged-test2 and executed metamath-knife-test set.mm --discouraged discuraged on it and the output is still the same.
What I've been done is somewhat redundant considering that the last commit of metamath-knife fixes issue https://github.com/metamath/metamath-knife/issues/147#issuecomment-1829350039, so once I tested that metamath-knife demo0.mm --dump-formula produced the fixed output I knew that it must be the newest version.
digama0
commented
6 months ago Could you try the following:
git clone https://github.com/metamath/set.mm
cd set.mm
git checkout b8e5ee3affd6f73b88a656600d2cb5b92c13ef65 # the parent of discouraged-test2
cd ..
git clone https://github.com/metamath/metamath-knife
cd metamath-knife
git checkout ee02227e5feddb0d60133ed27f43de3a49f6008b # current main
cargo run --release -- ../set.mm/set.mm --discouraged ../set.mm/discouraged2
diff ../set.mm/discouraged ../set.mm/discouraged2The final diff should be empty, and when I do this I get an empty diff (and the resulting file is 19532 lines long according to wc -l)
GinoGiotto
commented
6 months ago git clone https://github.com/metamath/set.mm
My internet connection is giving me problems, hope it's ok if I did git clone --depth 1 https://github.com/metamath/set.mm (b8e5ee.. is still the latest commit, so I think it's ok for now).
diff ../set.mm/discouraged ../set.mm/discouraged2
I am on Windows, so I did fc discouraged discouraged2
The final diff should be empty, and when I do this I get an empty diff (and the resulting file is 19532 lines long according to wc -l)
The final diff is not empty for me, and with a quick look it seems to be the same as the github diff. The file "discouraged" has 19532 lines + a blank line, while "discouraged2" has 19485 lines + a blank line.
GinoGiotto
commented
6 months ago I think I'm getting somewhere. The metamath.exe rewrapping algorithm does not break inside a (Proof modification is discouraged.) tag or inside a (New usage is discouraged.) tag, but for these theorems the metamath.exe rewrapping algorithm fails (I still have to figure out why, but it seems related to the presence of the html tables), so for these theorems the first tag gets breaked (and usually the (Proof modification is discouraged.) tag is written before the (New usage is discouraged.) one, so it does not happen that the second one gets breaked as well since it's not long enough). Since metamath-knife assumes that those tags are not breaked, it cannot read the (Proof modification is discouraged.) one because in these cases it is breaked.
In this minimal test case metamath-knife cannot read the (Proof modification is discouraged.) tag, can you replicate this?
$c A $. axiom $a A $. $( (Proof modification is discouraged.) (New usage is discouraged.) $) theorem $p A $= axiom $.
Generated discouraged:
New usage of "theorem" is discouraged (0 uses).
digama0
commented
6 months ago No, metamath-knife understands line breaking and this should not be a problem... unless the set.mm file you have uses \r\n newlines instead of \n!
GinoGiotto
commented
6 months ago No, metamath-knife understands line breaking and this should not be a problem... unless the set.mm file you have uses
\r\nnewlines instead of\n!
Ah, so the problem might be related to the fact that I'm on Windows then.
GinoGiotto
commented
6 months ago It works now! Thank you.
A question: what I mentioned before about metamath-exe rewrapping does happen tho. If I read the following minimal example and run write source test1.mm /rewrap then the comment above theorem is not rewrapped. Is this a bug or is it done on purpose to not mess up the tables?
Input:
$c A $.
axiom $a A $.
${
$( <HTML> <TABLE>
</TABLE> </HTML>
(Contributed by GG, 03-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) $)
theorem $p A $= axiom $.
$}
Output:
$c A $.
$( PLEASE PUT DESCRIPTION HERE. $)
axiom $a A $.
${
$( <HTML> <TABLE>
</TABLE> </HTML>
(Contributed by GG, 03-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) $)
theorem $p A $= axiom $.
$}
digama0
commented
6 months ago I think metamath-exe will deliberately not rewrap comments containing <HTML> to avoid breaking manual formatting.
GinoGiotto
commented
6 months ago I think metamath-exe will deliberately not rewrap comments containing
<HTML>to avoid breaking manual formatting.
Then it's ok with me.
Being able to update the discouraged file automatically is a very nice feature, unfortunately it is currently not usable due to incorrect output generation.
I created a new branch in my set.mm fork called discouraged-test. I updated that branch with the most recent version of set.mm, then I executed:
metamath-knife set.mm --discouraged discouragedAfter committing the newly produced discouraged file, these errors appear:
https://github.com/GinoGiotto/set.mm/actions/runs/7398403197/job/20127485347
Basically metamath-knife incorrectly removes some lines about proof modification. I observed that these theorems contain an HTML table in their comments, which might be related to why the
(Proof modification is discouraged.)tag isn't being read for them.