metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

MM gets stuck after pressing q #141

Closed GinoGiotto closed 1 year ago

GinoGiotto commented 1 year ago

Metamath.exe seems to enter some sort of infinite loop after pressing q in this circumstance:

Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> r set.mm
Reading source file "set.mm"... 43107244 bytes
43107244 bytes were read into the source buffer.
The source has 204913 statements; 2734 are $a and 40822 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> sh tr *
The proof of statement "a1ii" uses the following earlier statements:
  (None)
The proof of statement "idi" uses the following earlier statements:
  (None)
The proof of statement "mp2" uses the following earlier statements:
  wi($a) ax-mp($a)
The proof of statement "mp2b" uses the following earlier statements:
  ax-mp($a)
The proof of statement "a1i" uses the following earlier statements:
  wi($a) ax-mp($a) ax-1($a)
The proof of statement "2a1i" uses the following earlier statements:
  wi($a) ax-mp($a) ax-1($a) a1i
The proof of statement "mp1i" uses the following earlier statements:
  wi($a) ax-mp($a) ax-1($a) a1i
The proof of statement "a2i" uses the following earlier statements:
  wi($a) ax-mp($a) ax-2($a)
The proof of statement "mpd" uses the following earlier statements:
  wi($a) ax-mp($a) ax-2($a) a2i
The proof of statement "imim2i" uses the following earlier statements:
  wi($a) ax-mp($a) ax-1($a) ax-2($a) a1i a2i
The proof of statement "syl" uses the following earlier statements:
  wi($a) ax-mp($a) ax-1($a) ax-2($a) a1i a2i mpd
The proof of statement "3syl" uses the following earlier statements:
Press  for more, Q  to quit, S  to scroll to end... q

If I'm not wrong after pressing q Metamath is supposed to return: MM>

But it doesn't happen here.

digama0 commented 1 year ago

I think this is expected. Q silences the remainder of the output, but it is not actually an abort command. Presumably it is actually working, and it is just producing and suppressing a whole lot of output.

GinoGiotto commented 1 year ago

That seems to be a likely diagnosis, if I try show trace_back bezout* it takes around 3-4 seconds to show the MM> text which is consistent with how long the answer would be if I didn't silence it with q.

However if this is the correct diagnosis it means that the user would have to wait in the range of time of an hour before getting the MM> response, which looks bad to me. Anyone would probably just close and open metamath.exe, but this would be inconvenient if some proof were saved internally without the write source command, because any previous work would be lost.