BUG CHECK 2322

[GinoGiotto]

I created a file called "issue134.mm", the content of the file is simply:

$c A $.

ax1 $a A $.

Since it doesn't contain a $t comment, it's not possible to produce LaTeX statements and proofs from it (as expected). Now, if the user ignores this and still tries to produce a TeX file, then a bug check appears. If I understand correctly, Metamath should just produce an error message, not a bug check, so I decided to report this.

This is the complete log sequence that generates the bug:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read issue134.mm
Reading source file "issue134.mm"... 21 bytes
21 bytes were read into the source buffer.
The source has 2 statements; 1 are $a and 0 are $p.
SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> open tex test.tex
Created LaTeX output file "test.tex".
Reading definitions from $t statement of issue134.mm...
?Error: There is no $t command in the file "issue134.mm".
The file should have exactly one comment of the form $(...$t...$) with
the LaTeX and HTML definitions between $t and $).
?There was an error in the $t comment's LaTeX/HTML definitions.
MM> show statement ax1 /tex
Outputting statement "ax1"...
?Warning: Statement "ax1" has no comment
?BUG CHECK:  *** DETECTED BUG 2322

To get technical support, please send Norm Megill (nm@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(2322)" 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.

?BUG CHECK:  *** DETECTED BUG 2320
Press S  to step to next bug, I  to ignore further bugs,
or A  to abort program:  S
?Warning: In the comment for statement "ax1", math symbol token "A" does not
have a LaTeX and/or an HTML definition.
The LaTeX source was written to "test.tex".
MM>

I'm not sure how relevant it is since Metamath already provides error messages after open tex test.tex that explain the problem. The user would have to ignore those messages to encounter this bug, so I doubt this event would be a common occurrence.

[david-a-wheeler]

That's fair. This is an edge case obviously, since the user is requesting something nonsensical, but I agree we could do better.

[GinoGiotto]

Thanks for the fix!