Dan,

On Mon, 2021-01-25 at 14:40 +0100, D. J. Bernstein wrote:
> I have another newbie question regarding HOL Light; again happy to
> hear about other HOL variants if those have easier answers.

Since you mentioned other HOL variants, I would like to point out that
Isabelle can take advantage of multi-core architectures: see, e.g.,
https://doi.org/10.1007/978-3-642-39634-2_30

This might give you a speedup on the order of 10x or so, depending on
your hardware.

> I'd guess that >99% of the CPU time I'm seeing comes from HOL Light
> searching for proofs (e.g., the computation in REAL_LINEAR_PROVER),

Generic proof replay (as discussed by Mike) could indeed be a solution,
but if you don't need the full power of REAL_LINEAR_PROVER in your
proofs, there is also a good chance that you could significantly reduce
CPU time by implementing your own (more specific) optimized tactic.

This really depends on what your proof obligations look like. It'd be
great if you could say more about them.

Best,
Tjark









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att 
vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du 
läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For 
more information on how this is performed, please read here: 
http://www.uu.se/en/about-uu/data-protection-policy


_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to