diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 11:19:04 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 11:19:04 +0000 |
| commit | 64da00694c65af10da343f8ffad4a0088c8bb845 (patch) | |
| tree | f2b1d73e3b184961e51a4db3265f5a2e885782da /isar/isar-autotest.el | |
| parent | 0df29cabce37b1bfd05e1feaa2eab817149aa326 (diff) | |
Clean flag settings for profiling. Add AHundredProofs.
Diffstat (limited to 'isar/isar-autotest.el')
| -rw-r--r-- | isar/isar-autotest.el | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 9c63140b..cdf69a1b 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -17,6 +17,7 @@ (declare-function isar-tracing:auto-quickcheck-toggle "isar.el") (declare-function isar-tracing:auto-solve-toggle "isar.el") +(declare-function isar-proof:parallel-proofs-toggle "isar.el") (require 'pg-autotest) @@ -31,6 +32,14 @@ (pg-autotest remark "Testing standard Example.thy, Example-Xsym.thy") (pg-autotest script-wholefile "isar/Example.thy") + + ;; Speed up prover + (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) + (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! + (pg-autotest eval (proof-full-annotation-toggle 0)) + (pg-autotest eval (isar-proof:parallel-proofs-toggle 0)) + (proof-shell-wait) + (pg-autotest script-wholefile "isar/Example-Tokens.thy") (pg-autotest remark "Testing prove-as-you-go (not replay)") @@ -58,9 +67,6 @@ (when isar-long-tests (pg-autotest remark "Larger files...") - (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) - (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! - (pg-autotest eval (proof-full-annotation-toggle 0)) (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") (pg-autotest script-wholefile "isar/ex/Tarski.thy") (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test? |