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
