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. On Sat, Nov 19, 2022 at 9:24 PM Mario Carneiro <[email protected]> wrote: > 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 [email protected] anymore but recommendations to send messages > there are all over the metamath website and tools. > > On Sat, Nov 19, 2022 at 9:20 PM Gino Giotto <[email protected]> > wrote: > >> 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 ([email protected]) 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 >> Il giorno domenica 20 novembre 2022 alle 02:39:32 UTC+1 [email protected] >> ha scritto: >> >>> 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". >>> >>> On Sat, Nov 19, 2022 at 8:20 PM Gino Giotto <[email protected]> >>> wrote: >>> >>>> 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 ([email protected]) >>>> 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 >>>> >>>> -- >>>> 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 [email protected]. >>>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/metamath/649af2ef-1103-4384-9037-955dc5543335n%40googlegroups.com >>>> <https://groups.google.com/d/msgid/metamath/649af2ef-1103-4384-9037-955dc5543335n%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- >> 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 [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/7d0b07ba-0fc3-41a3-92c2-3c8ab8940b87n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/7d0b07ba-0fc3-41a3-92c2-3c8ab8940b87n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStHiG9wmB0aKU2YgVzQegBLaSRRjsBnFEzfOa2gj3ighw%40mail.gmail.com.
