metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
77 stars 25 forks source link

bug check 1717 #156

Open GinoGiotto opened 1 year ago

GinoGiotto commented 1 year ago

If I execute the MM> DBG command without reading a .mm file first, then a bug check appears:

Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> DBG test
DEBUGGING MODE IS FOR DEVELOPER'S USE ONLY!
Argument:  test
?BUG CHECK:  *** DETECTED BUG 1717

To get technical support, please open an issue 
(https://github.com/metamath/metamath-exe/issues) with the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used.  See HELP OPEN LOG for help on
recording a session.  See HELP SUBMIT for help on command files.  Search
for "bug(1717)" 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  to step to next bug, I  to ignore further bugs,
or A  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.

?Error:
test
^^^^
This math symbol was not declared (with a "$c" or "$v" statement).
Trying depth 0

After pressing S metamath-exe crashes.

Also I wasn't able to find instructions about this command nor in the book, nor in MM> help. How does it work and what is its purpose?