Stream: Beginner Questions

Topic: Proof terms in Isabelle


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (Mar 07 2023 at 06:12):

I assume that you are refering to the session HOL-proofs

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Mar 07 2023 at 06:14):

Normally the proofs passes through the Isabelle kernel and is not stored anyway.

view this post on Zulip Mathias Fleury (Mar 07 2023 at 06:15):

This is faster than explicitly building and storing them

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC