metamath / metamath-exe

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

The `clock()` function doesn't work #157

Closed GinoGiotto closed 10 months ago

GinoGiotto commented 1 year ago

The clock() function used to work fine for version 0.198, but it doesn't work anymore for version 0.199. Below I show four commands examples comparing the outputs of the two versions:


Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> SHOW ELAPSED_TIME
Time since last SHOW ELAPSED_TIME command =  27.58 s; total =  27.58 s
MM> SHOW ELAPSED_TIME
Time since last SHOW ELAPSED_TIME command =   4.79 s; total =  32.37 s
MM> 
Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> SHOW ELAPSED_TIME
The clock() function is not implemented on this computer.
Time since last SHOW ELAPSED_TIME command =   0.00 s; total =   0.00 s
MM> SHOW ELAPSED_TIME
The clock() function is not implemented on this computer.
Time since last SHOW ELAPSED_TIME command =   0.00 s; total =   0.00 s
MM> 

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> SAVE PROOF bezout /TIME
The proof of "bezout" has been reformatted and saved internally.
SAVE PROOF run time =   0.01 sec for "bezout"
Remember to use WRITE SOURCE to save changes permanently.
MM> 
Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> SAVE PROOF bezout /TIME
The clock() function is not implemented on this computer.
The proof of "bezout" has been reformatted and saved internally.
The clock() function is not implemented on this computer.
SAVE PROOF run time =   0.00 sec for "bezout"
Remember to use WRITE SOURCE to save changes permanently.
MM> 

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> PROVE bezout
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT bezout"):
$d x y A $.  $d x B y $.
51633 bezout $p |- ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B
      ) = ( ( A x. x ) + ( B x. y ) ) ) $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /TIME
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
No shorter proof was found.
MINIMIZE_WITH run time =   12.12 sec for "bezout"
MM-PA> 
Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> PROVE bezout
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT bezout"):
$d x y A $.  $d x B y $.
51633 bezout $p |- ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B
      ) = ( ( A x. x ) + ( B x. y ) ) ) $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /TIME
The clock() function is not implemented on this computer.
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
No shorter proof was found.
The clock() function is not implemented on this computer.
MINIMIZE_WITH run time =    0.00 sec for "bezout"
MM-PA> 

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> VERIFY PROOF *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 13.53 s.
MM>
Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43241860 bytes
43241860 bytes were read into the source buffer.
The source has 205865 statements; 2746 are $a and 40947 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> VERIFY PROOF *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified.
MM>

To me this looks like a bug, how can I make it work for version 0.199 too?

digama0 commented 10 months ago

fixed in 98c89f5a