digama0
commented
1 year ago My diagnosis of this issue is that arguments containing spaces are allowed (you should put the argument in quotes if you write it in one line rather than in the prompted mode), but the switch position calculation was incorrect when previous arguments have spaces. TBH it's surprising that we didn't run into this before, since I have typed search * "foo + bar" /j many times and one would think that the /j calculation would go out of bounds.
Using spaces won't actually work here as an argument to minimize_with though; it will just look for a label containing a space, which will fail.
While I was experimenting with the minimize command I had the idea to allow introduction of
|-definitions andwffdefinitions. I noticed thatwffdefinitions in set.mm start withw*, so I tried the command:MM-PA> MINIMIZE_WITH * /ALLOW_NEW_AXIOMS df-* w* ^^ ?Expected / or nothing. MM-PA>This produces an error, so it seems to be an invalid request.
However if I write the same thing in this form:
Then it doesn't complain and starts scanning, which is inconsistent with the behaviour of the first version of the command.
Not only this behaviour is inconsistent, but it also generates bugs in some circumstances, I was able to find 2 of them, the first one:
Which generates the following msgbox. Pressing the OK button will make the program close by itself. In this case Metamath doesn't start minimizing and it doesn't even produce a bug check.
The second circumstance that generates this bug is:
which produces this msgbox (and then Metamath closes by itself when the OK button is pressed, as in the first example).
These bugs presents themselves in this form in the 0.198 version. In the 0.199 one the program just crashes without showing any msgbox.
As a side note I guess the right way to allow both
|-definitions andwffdefinitions would be:but I'm not sure if this kind of request was contemplated in the design. Does metamath takes care of both
/ALLOW_NEW_AXIOMSor one nullifies the other? (question for Metamath developers).Finally here is an example of a complete log sequence to reproduce one version of these issues:
Metamath - Version 0.199.pre 29-Jan-2022 Type HELP for help, EXIT to exit. MM> READ set.mm Reading source file "set.mm"... 43107244 bytes 43107244 bytes were read into the source buffer. The source has 204913 statements; 2734 are $a and 40822 are $p. No errors were found. However, proofs were not checked. Type VERIFY PROOF * if you want to check them. MM> PROVE bezout Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. You will be working on statement (from "SHOW STATEMENT bezout"): $d x y A $. $d x B y $. 51216 bezout $p |- ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) ) $= ... $. Note: The proof you are starting with is already complete. MM-PA> MINIMIZE_WITH * / VERBOSE, MAY_GROW, EXCEPT, OVERRIDE, INCLUDE_MATHBOXES, ALLOW_NEW_AXIOMS, NO_NEW_AXIOMS_FROM, FORBID, or TIME? ALLOW_NEW_AXIOMS
What statement label match pattern? df-* w*
/ or nothing <nothing>? /
VERBOSE, MAY_GROW, EXCEPT, OVERRIDE, INCLUDE_MATHBOXES, ALLOW_NEW_AXIOMS,
NO_NEW_AXIOMS_FROM, FORBID, or TIME ? FORBID
What statement label match pattern? ax-13
/ or nothing <nothing>? However my assumption is that these behaviours will show no matter what database you use or what theorem you are trying to minimize.