waynee95 (Mar 06 2023 at 21:25): waynee95 (Mar 06 2023 at 21:25):I know that you can see proof terms if you enable them and that you can use them with ML.
I always thought that the choice for not having proof terms exposed to the user was because how the philosophy of Isabelle wants proofs to look like, focusing on structured proofs.
But in a discussion it came up that Isabelle doesn't expose proof terms and doesn't use them because of performance reasons.
So is it the case that proof terms, as a whole, are only an opt-in addon?
Mathias Fleury (Mar 07 2023 at 06:12):I assume that you are refering to the session HOL-proofs
Mathias Fleury (Mar 07 2023 at 06:14):The difference between HOL and HOL proofs is not wether you use proof terms or not. It is whether you export them or not.
Mathias Fleury (Mar 07 2023 at 06:14):Normally the proofs passes through the Isabelle kernel and is not stored anyway.
Mathias Fleury (Mar 07 2023 at 06:15):This is faster than explicitly building and storing them
Mathias Fleury (Mar 07 2023 at 06:25):Proper timings on my machine:
$ 2022isabelle build -c -j6 -o "threads=20" -b HOL-Proofs
Timing HOL-Proofs (20 threads, 186.387s elapsed time, 599.244s cpu time, 364.895s GC time, factor 3.22)
Finished HOL-Proofs (0:03:33 elapsed time, 0:11:19 cpu time, factor 3.18)
Finished at Tue Mar 7 07:22:04 GMT+1 2023
0:03:39 elapsed time, 0:11:19 cpu time, factor 3.10
$ 2022isabelle build -c -j6 -o "threads=20" -b HOL-Proofs
Finished HOL (0:01:40 elapsed time, 0:11:29 cpu time, factor 6.88)
0:01:45 elapsed time, 0:11:29 cpu time, factor 6.55
Last updated: Apr 23 2024 at 12:29 UTC