Bug 256 when showing HTML in a file which has errors (metamath.exe)

[jkingdon]

If I am working on a file with several proofs that don't verify, it is pretty common for show statement /alt_html to cause metamath to abort with a BUG 256 message.

I was not able to find a small file which reproduces the problem, but here is a non-small file which does. I've enclosed the file and the sequence of metamath commands. The desired behavior would be for the HTML display to continue to work (possibly with some output like ?Error but with the parts of the page unaffected by the error intact).

iset.mm.txt

$ rlwrap ../metamath/metamath/metamath 
Metamath - Version 0.161 2-Feb-2018           Type HELP for help, EXIT to exit.
MM> read iset.mm
Reading source file "iset.mm"... 1417403 bytes
1417403 bytes were read into the source buffer.
The source has 13506 statements; 139 are $a and 3685 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show statement snprc
11592 snprc $p |- ( -. A e. _V <-> { A } = (/) ) $= ... $.
MM> show statement snprc/alt_html
Creating HTML file "snprc.html"...
Reading definitions from $t statement of iset.mm...
143 typesetting statements were read from "iset.mm".
Reading HTML bibliographic tags from file "mmil.html"...
?BUG CHECK:  *** DETECTED BUG 256

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(256)" in the m*.c source code to find its origin.

Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  A

The program was aborted.
$ ^C
$ 

[nmegill]

OK, I can reproduce it. I will look into it soon and fix it. It occurs at line 1129 of mmcmds.c where it expected the cumulative output string to the HTML file to have been emptied by a previous write. My instinct is that it is probably OK to answer "i" to ignore it so you can go on, although it might not be wise to trust a 'write source' from that point unless you check the diff from the previous .mm version.

Thanks for reporting it.

Norm

[nmegill]

This has been fixed.