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.
