$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:
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.mmhas either the/VERIFYoption active or when theverify proof *command follows.EDIT: The following simpler file produces the same bug:
$c A $. ax1 $ A $. ${ th1 $p A $= ax1 $.