Bugs in Metamath

[Gino Giotto]

Hello, I am a new user of the Metamath software. While checking a few commands I found one that generates a bug and Metamath recommended me to report it. Here is the complete log text:

----------------------------------------------------------------------------------------------------------

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 42559898 bytes
42559898 bytes were read into the source buffer.
The source has 202975 statements; 2691 are $a and 40449 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show proof ex3 /unknown
?BUG CHECK:  *** DETECTED BUG 1337

To get technical support, please send Norm Megill (n...@alum.mit.edu) the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used.  See HELP LOG for help on
recording a session.  See HELP SUBMIT for help on command files.  Search
for "bug(1337)" in the m*.c source code to find its origin.
If earlier errors were reported, try fixing them first, because they
may occasionally lead to false bug detection

Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:

----------------------------------------------------------------------------------------------------------

The set.mm file that I'm using is just the untouched version I downloaded on October 6th 2022 on https://us.metamath.org/.

Also it looks like the "help log" command doesn't work, here is the log history:

----------------------------------------------------------------------------------------------------------

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> HELP LOG
         ^^^
?Expected LANGUAGE, PROOF_ASSISTANT, MM-PA, BEEP, EXIT, QUIT, READ, ERASE,
OPEN, CLOSE, SHOW, SEARCH, SET, VERIFY, SUBMIT, SYSTEM, PROVE, FILE, WRITE,
MARKUP, ASSIGN, REPLACE, MATCH, UNIFY, LET, INITIALIZE, DELETE, IMPROVE,
MINIMIZE_WITH, EXPAND, UNDO, REDO, SAVE, DEMO, INVOKE, CLI, EXPLORE, TEX,
LATEX, HTML, COMMENTS, BIBLIOGRAPHY, MORE, TOOLS, MIDI, or nothing.
MM>

----------------------------------------------------------------------------------------------------------

Thanks in advance for anyone's time, as I said I'm new so I'm just learning everything now.

Regards

Gino

[Mario Carneiro]

Thanks for the report. I think we would like bug reports against metamath.exe to be reported at https://github.com/metamath/metamath-exe/issues since it's a bit easier to track them there, but while we're here:

I can replicate the issue on the latest metamath.exe / set.mm. The text suggesting "HELP LOG" was in error, it should have said "HELP OPEN LOG". (This has been fixed.) I will try to track down the issue with "show proof ex3 /unknown".

--
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/649af2ef-1103-4384-9037-955dc5543335n%40googlegroups.com.

[Gino Giotto]

Thanks for the reply and sorry for the misconduct, I will report next bugs on https://github.com/metamath/metamath-exe/issues in the future. For this one I also noticed that if I press "S" the terminal shows another bug, here is the complete log text:

-----------------------------------------------------------------------------------------------------------------------------

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read set.mm

Reading source file "set.mm"... 42616323 bytes
42616323 bytes were read into the source buffer.
The source has 202900 statements; 2702 are $a and 40449 are $p.

No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show proof ex3 /unknown
?BUG CHECK:  *** DETECTED BUG 1337

To get technical support, please send Norm Megill (n...@alum.mit.edu) the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used.  See HELP LOG for help on
recording a session.  See HELP SUBMIT for help on command files.  Search
for "bug(1337)" in the m*.c source code to find its origin.
If earlier errors were reported, try fixing them first, because they
may occasionally lead to false bug detection

Press S <return> to step to next bug, I <return> to ignore further bugs,

or A <return> to abort program:  S

Warning!!!  A bug was detected, but you are continuing anyway.
The program may be corrupted, so you are proceeding at your own risk.

?BUG CHECK:  *** DETECTED BUG 1338

Press S <return> to step to next bug, I <return> to ignore further bugs,

or A <return> to abort program:  S
MM>

------------------------------------------------------------------------------------------------------------------------------

I also tested the same commands on the latest version of metamath.exe and set.mm and found the same results.

Regards

Gino

[Mario Carneiro]

It's no misconduct, we're still figuring out our processes since the original author is no longer around to take bug reports anymore.  I'm glad you were at least able to figure out to post here, I think no one is checking n...@alum.mit.edu anymore but recommendations to send messages there are all over the metamath website and tools.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7d0b07ba-0fc3-41a3-92c2-3c8ab8940b87n%40googlegroups.com.

[Mario Carneiro]

The bug is now fixed on master: https://github.com/metamath/metamath-exe/commit/77285d4 . (FTR, you should see nothing when you run that command, as ex3 has no unknown proof steps in it.) The follow on error with S isn't that important, it was reading nonsense memory anyway.

For the curious:
It appears that there was once a bug check which would report if you try to use "show proof /unknown" outside of MM-PA mode (that is, before running "prove foo"). The purpose of the command is to show proof steps proved by '?', which usually only occurs when you are in the middle of a proof, but you are allowed to read and write proofs containing '?' in the input mm file itself so it is not crazy to be using the command outside of MM-PA mode and hence the bug check was removed. But it was reading the proof-in-progress state, which is not valid (an empty list) if you are not in MM-PA mode, and so it crashes and burns in that case. The fix is to access the proof of the specified command instead of the proof-in-progress.

[Gino Giotto]

Thanks for the fix and the explanation! I understand what was going on now :)