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?

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

The difference between HOL and HOL proofs is not wether you use proof terms or not. It is whether you export them or not.

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

This is faster than explicitly building and storing them

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: Oct 13 2024 at 01:36 UTC