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 Il giorno domenica 20 novembre 2022 alle 02:39:32 UTC+1 di....@gmail.com 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 <ginogiott...@gmail.com> > 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 (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 >> >> -- >> 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 >> >> <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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7d0b07ba-0fc3-41a3-92c2-3c8ab8940b87n%40googlegroups.com.
