Open
Description
File that generates the bug:
$c A $. ax1 $ A $. ${ in.1 $e A $. in $a A $. $} th1 $p A $= ax1 in $.
Metamath-exe interface:
Metamath - Version 0.199.pre 29-Jan-2022 Type HELP for help, EXIT to exit. MM> set scroll continuous Continuous scrolling is now in effect. MM> read issue168.mm /verify Reading source file "issue168.mm"... 78 bytes ?Error on line 3 of file "issue168.mm": ax1 $ A $. ^ A keyword must be followed by white space. 78 bytes were read into the source buffer. ?Error on line 3 of file "issue168.mm" at statement 1, type "$c": ax1 $ A $. ^^ Expected "$c", "$v", "$e", "$f", "$d", "$a", "$p", "${", or "$}" here. ?Error on line 3 of file "issue168.mm" at statement 1, type "$c": ax1 $ A $. ^^ Expected "$c", "$v", "$e", "$f", "$d", "$a", "$p", "${", or "$}" here. The source has 6 statements; 1 are $a and 1 are $p. ?Error on line 3 of file "issue168.mm" at statement 2, type "${": ax1 $ A $. ^^^ A label isn't allowed for this statement type. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% ..................................................?BUG CHECK: *** DETECTED BUG 1710 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(1710)" 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 2102 Press S to step to next bug, I to ignore further bugs, or A to abort program: S 4 errors were found. MM>
The bug occurs when read issue168.mm
has either the /VERIFY
option active or when the verify proof *
command follows.
EDIT: The following simpler file produces the same bug:
$c A $. ax1 $ A $. ${ th1 $p A $= ax1 $.
Metadata
Metadata
Assignees
Labels
No labels