[acl2-books] r986 committed - Mods for ACL2(p) regression, make in consultion with David Rager.

0 views

Skip to first unread message

acl2-...@googlecode.com

unread,

Feb 28, 2012, 12:25:06 AM2/28/12

to acl2-...@googlegroups.com

Revision: 986
Author: kauf...@cs.utexas.edu
Date: Mon Feb 27 21:23:51 2012
Log: Mods for ACL2(p) regression, make in consultion with David Rager.
http://code.google.com/p/acl2-books/source/detail?r=986

Added:
/trunk/coi/quantification/quantification.acl2
/trunk/rtl/rel7/support/lib1.delta1/mult-proofs.acl2
/trunk/rtl/rel8/support/lib1.delta1/mult-proofs.acl2
Modified:
/trunk/clause-processors/SULFA/books/sat-tests/benchmark.acl2
/trunk/clause-processors/SULFA/books/sat-tests/benchmark.lisp
/trunk/clause-processors/SULFA/books/sat-tests/sudoku.acl2
/trunk/clause-processors/SULFA/books/sat-tests/test-incremental.acl2
/trunk/clause-processors/SULFA/books/sat-tests/tutorial.acl2
/trunk/clause-processors/basic-examples.acl2
/trunk/clause-processors/equality.acl2
/trunk/hints/basic-tests.acl2
/trunk/hints/consider-hint-tests.acl2
/trunk/misc/profiling.acl2
/trunk/models/jvm/m5/apprentice.acl2

=======================================
--- /dev/null
+++ /trunk/coi/quantification/quantification.acl2 Mon Feb 27 21:23:51 2012
@@ -0,0 +1,6 @@
+#+acl2-par
+; computed hint that modifies state
+(set-waterfall-parallelism nil)
+
+(ld "cert.acl2")
+(certify-book "quantification" ?)
=======================================
--- /dev/null
+++ /trunk/rtl/rel7/support/lib1.delta1/mult-proofs.acl2 Mon Feb 27
21:23:51 2012
@@ -0,0 +1,4 @@
+#+acl2-par
+# a proof goes into an infinite loop with waterfall-parallelism enabled
+(set-waterfall-parallelism nil)
+(certify-book "mult-proofs")
=======================================
--- /dev/null
+++ /trunk/rtl/rel8/support/lib1.delta1/mult-proofs.acl2 Mon Feb 27
21:23:51 2012
@@ -0,0 +1,4 @@
+#+acl2-par
+# a proof goes into an infinite loop with waterfall-parallelism enabled
+(set-waterfall-parallelism nil)
+(certify-book "mult-proofs")
=======================================
--- /trunk/clause-processors/SULFA/books/sat-tests/benchmark.acl2 Thu Dec
6 11:36:07 2007
+++ /trunk/clause-processors/SULFA/books/sat-tests/benchmark.acl2 Mon Feb
27 21:23:51 2012
@@ -1,6 +1,10 @@

(acl2::value :q)
(acl2::lp)
+
(ld '((ubt! 1)
(ld "../sat/sat-package.acl2")
- (certify-book "benchmark" 1 t :ttags (sat sat-cl))))
+ (certify-book "benchmark" 1 t
+ :ttags (sat sat-cl
+ #+acl2-par
+ our-waterfall-parallelism-hacks))))
=======================================
--- /trunk/clause-processors/SULFA/books/sat-tests/benchmark.lisp Tue May
13 10:19:53 2008
+++ /trunk/clause-processors/SULFA/books/sat-tests/benchmark.lisp Mon Feb
27 21:23:51 2012
@@ -3,6 +3,18 @@

(include-book "test-help" :ttags (sat sat-cl))

+;; -----------------------------------------------------------------
+; This section was added by Matt K. to test waterfall parallelism hacks,
+; specifically, to allow clause processors that modify state. SULFA-THM
fails
+; in ACL2(p) with waterfall-parallelism enabled unless we make some
+; accommodation.
+
+#+acl2-par
+(defttag our-waterfall-parallelism-hacks)
+#+acl2-par
+(set-waterfall-parallelism-hacks-enabled t)
+;; -----------------------------------------------------------------
+
;; -----------------------------------------------------------------
;; Definitions

=======================================
--- /trunk/clause-processors/SULFA/books/sat-tests/sudoku.acl2 Thu Dec 6
11:36:07 2007
+++ /trunk/clause-processors/SULFA/books/sat-tests/sudoku.acl2 Mon Feb 27
21:23:51 2012
@@ -1,6 +1,11 @@

(acl2::value :q)
(acl2::lp)
+
+#+acl2-par
+; clause processors that modify state
+(set-waterfall-parallelism nil)
+
(ld '((ubt! 1)
(ld "../sat/sat-package.acl2")
(certify-book "tutorial" 1 t :ttags (sat sat-cl))))
=======================================
--- /trunk/clause-processors/basic-examples.acl2 Fri Jun 25 14:02:26 2010
+++ /trunk/clause-processors/basic-examples.acl2 Mon Feb 27 21:23:51 2012
@@ -1,1 +1,5 @@
+#+acl2-par
+; clause processors that modify state
+(set-waterfall-parallelism nil)
+
(certify-book "basic-examples" 0 t :ttags (my-ttag) :defaxioms-okp t)
=======================================
--- /trunk/clause-processors/equality.acl2 Wed Sep 15 06:40:11 2010
+++ /trunk/clause-processors/equality.acl2 Mon Feb 27 21:23:51 2012
@@ -1,2 +1,6 @@
+#+acl2-par
+; clause processors that modify state
+(set-waterfall-parallelism nil)
+
(ld "tools/flag-package.lsp" :dir :system)
(certify-book "equality" ? t)
=======================================
--- /trunk/hints/basic-tests.acl2 Thu Dec 6 11:36:07 2007
+++ /trunk/hints/basic-tests.acl2 Mon Feb 27 21:23:51 2012
@@ -1,4 +1,8 @@
; Enable proof output.
(set-inhibit-output-lst '(proof-tree))

+#+acl2-par
+; computed hints that modify state
+(set-waterfall-parallelism nil)
+
(certify-book "basic-tests" 0 t :skip-proofs-okp t :defaxioms-okp t)
=======================================
--- /trunk/hints/consider-hint-tests.acl2 Thu Dec 6 11:36:07 2007
+++ /trunk/hints/consider-hint-tests.acl2 Mon Feb 27 21:23:51 2012
@@ -1,1 +1,5 @@
+#+acl2-par
+; custom keyword hint that modifies state
+(set-waterfall-parallelism nil)
+
(certify-book "consider-hint-tests" 0 t :skip-proofs-okp t)
=======================================
--- /trunk/misc/profiling.acl2 Fri Oct 22 05:14:22 2010
+++ /trunk/misc/profiling.acl2 Mon Feb 27 21:23:51 2012
@@ -1,1 +1,5 @@
+#+acl2-par
+; You can't load profiling after threads are already started.
+(set-waterfall-parallelism nil)
+
(certify-book "profiling" 0 t :ttags (:profiling))
=======================================
--- /trunk/models/jvm/m5/apprentice.acl2 Mon Apr 28 09:26:50 2008
+++ /trunk/models/jvm/m5/apprentice.acl2 Mon Feb 27 21:23:51 2012
@@ -1,2 +1,7 @@
+#+acl2-par
+(set-total-parallelism-work-limit-error nil state)
+#+acl2-par
+(set-total-parallelism-work-limit 3000 state)
+
(include-book "m5")
(certify-book "apprentice" 1)

Reply all

Reply to author

Forward

0 new messages