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 | |
parent | 0df29cabce37b1bfd05e1feaa2eab817149aa326 (diff) |
Clean flag settings for profiling. Add AHundredProofs.
-rw-r--r-- | etc/isar/AHundredProofs.thy | 1008 | ||||
-rw-r--r-- | isar/isar-autotest.el | 12 | ||||
-rw-r--r-- | isar/isar-profiling.el | 14 |
3 files changed, 1023 insertions, 11 deletions
diff --git a/etc/isar/AHundredProofs.thy b/etc/isar/AHundredProofs.thy new file mode 100644 index 00000000..6f59f4e0 --- /dev/null +++ b/etc/isar/AHundredProofs.thy @@ -0,0 +1,1008 @@ +theory AHundredProofs imports Main +begin + +ML {* val start = start_timing(); *} + +theorem and_comms1: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms2: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms3: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms4: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms5: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms6: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms7: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms8: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms9: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms10: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms11: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms12: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms13: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms14: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms15: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms16: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms17: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms18: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms19: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms20: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms21: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms22: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms23: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms24: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms25: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms26: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms27: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms28: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms29: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms30: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms31: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms32: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms33: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms34: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms35: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms36: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms37: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms38: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms39: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms40: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms41: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms42: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms43: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms44: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms45: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms46: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms47: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms48: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms49: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms50: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms51: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms52: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms53: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms54: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms55: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms56: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms57: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms58: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms59: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms60: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms61: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms62: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms63: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms64: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms65: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms66: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms67: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms68: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms69: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms70: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms71: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms72: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms73: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms74: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms75: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms76: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms77: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms78: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms79: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms80: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms81: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms82: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms83: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms84: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms85: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms86: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms87: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms88: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms89: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms90: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms91: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms92: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms93: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms94: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms95: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms96: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms97: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms98: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms99: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +theorem and_comms100: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +ML {* Output.warning (#message (end_timing start)); *} + +end 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? diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 22777c5b..8984f1b0 100644 --- a/isar/isar-profiling.el +++ b/isar/isar-profiling.el @@ -12,8 +12,9 @@ (require 'proof-site) (proof-ready-for-assistant 'isar)) -(declare-function isar-tracing:auto-quickcheck-toggle "isar.el") (declare-function isar-tracing:auto-solve-toggle "isar.el") +(declare-function isar-tracing:auto-quickcheck-toggle "isar.el") +(declare-function isar-proof:parallel-proofs-toggle "isar.el") (require 'pg-autotest) (require 'pg-dev) @@ -26,8 +27,8 @@ (pg-autotest-find-file "etc/isar/AHundredTheorems.thy") (pg-autotest eval (proof-shell-ready-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 (isar-tracing:auto-quickcheck-toggle 0)) (pg-autotest eval (isar-proof:parallel-proofs-toggle 0)) (pg-autotest eval (proof-full-annotation-toggle 0)) (proof-shell-wait) @@ -36,12 +37,6 @@ (pg-autotest timestart) (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") (pg-autotest timetaken) - (pg-autotest timestart) - (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest timetaken) - (pg-autotest timestart) - (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest timetaken) ;; Same again with profiling (profile-pg) @@ -51,6 +46,9 @@ (pg-autotest timestart) (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") (pg-autotest timetaken) + (pg-autotest timestart) + (pg-autotest process-wholefile "etc/isar/AHundredProofs.thy") + (pg-autotest timetaken) (elp-results) (let ((results (with-current-buffer "*ELP Profiling Results*" |