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 issue169.mm /verify
Reading source file "issue169.mm"... 32 bytes
32 bytes were read into the source buffer.
The source has 2 statements; 1 are $a and 1 are $p.
?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a":
ax1 $a A $.
^
This math symbol was not declared (with a "$c" or "$v" statement).
?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a":
ax1 $a A $.
^
The first symbol must be a constant in a "$a" statement.
?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a":
ax1 $a A $.
^
This variable does not occur in any active "$e" or "$f" hypothesis. All
variables in "$a" and "$p" statements must appear in at least one such
hypothesis.
SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a":
ax1 $a A $.
The variable "A" does not appear in an active "$f" statement.
?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p":
th1 $p A $= ax1 $.
^
This math symbol was not declared (with a "$c" or "$v" statement).
?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p":
th1 $p A $= ax1 $.
^
The first symbol must be a constant in a "$p" statement.
?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p":
th1 $p A $= ax1 $.
^
This variable does not occur in any active "$e" or "$f" hypothesis. All
variables in "$a" and "$p" statements must appear in at least one such
hypothesis.
?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p":
th1 $p A $= ax1 $.
The variable "A" does not appear in an active "$f" statement.
0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................?BUG CHECK: *** DETECTED BUG 2103
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(2103)" 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.
8 errors were found.
MM>
Without the /VERIFY option the bug does not occur (the verify proof * command triggers the bug as well).
File that generates the bug:
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 issue169.mm /verify Reading source file "issue169.mm"... 32 bytes 32 bytes were read into the source buffer. The source has 2 statements; 1 are $a and 1 are $p. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ This math symbol was not declared (with a "$c" or "$v" statement). ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ The first symbol must be a constant in a "$a" statement. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ This variable does not occur in any active "$e" or "$f" hypothesis. All variables in "$a" and "$p" statements must appear in at least one such hypothesis. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. The variable "A" does not appear in an active "$f" statement. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ This math symbol was not declared (with a "$c" or "$v" statement). ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ The first symbol must be a constant in a "$p" statement. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ This variable does not occur in any active "$e" or "$f" hypothesis. All variables in "$a" and "$p" statements must appear in at least one such hypothesis. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. The variable "A" does not appear in an active "$f" statement. 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% ..................................................?BUG CHECK: *** DETECTED BUG 2103 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(2103)" 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.
8 errors were found.
MM>
Without the
/VERIFYoption the bug does not occur (theverify proof *command triggers the bug as well).