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/CAFXXJStRy7m_0_i2GhC8C8oJGs0zSGZTCYxjiR1_TL0%2BNhqDGQ%40mail.gmail.com.
