Thanks for the fix and the explanation! I understand what was going on now :)
Il giorno domenica 20 novembre 2022 alle 04:37:58 UTC+1 [email protected] ha scritto: > 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/b63cbfe9-dffd-4305-b52a-27794fa8533bn%40googlegroups.com.
