diff options
| author | David Aspinall | 2010-08-03 23:08:39 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-03 23:08:39 +0000 |
| commit | 35f05f9f85e02ff7f03f73d884983289c5f4bebb (patch) | |
| tree | b5b025076941b9cbc902102d904247e33ac76670 /isar/isar-autotest.el | |
| parent | 1a70304eb6a283abeae1df8c0ed12da34a60d6e4 (diff) | |
Separate profiling from testing
Diffstat (limited to 'isar/isar-autotest.el')
| -rw-r--r-- | isar/isar-autotest.el | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index cc3d6640..398b6942 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -27,11 +27,16 @@ (pg-autotest script-wholefile "isar/Example.thy") (pg-autotest script-wholefile "isar/Example-Tokens.thy") - (pg-autotest remark "Testing random jumps") + (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 remark "Testing random jumps") (pg-autotest script-randomjumps "isar/Example.thy" 5) - (pg-autotest script-randomjumps "etc/isar/AHundredTheorems.thy" 10) + (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10) ; better test? (pg-autotest remark "Testing restarting the prover") (pg-autotest quit-prover) @@ -40,10 +45,6 @@ (pg-autotest eval (proof-unicode-tokens-toggle)) (pg-autotest script-wholefile "isar/Example-Tokens.thy") - (pg-autotest remark "A larger file:") - (pg-autotest timestart) - (pg-autotest script-wholefile "isar/ex/Tarski.thy") - (pg-autotest timetaken) (pg-autotest remark "Simple test of multiple file behaviour:") (pg-autotest script-wholefile "etc/isar/multiple/C.thy") |