Tweaked comments in check-system-guards.lisp. Updated info for next ACL2 Workshop.

Author: MattKaufmann

books/system/check-system-guards.lisp

@@ -33,15 +33,18 @@
 ; One can do more, for example as follows.
 
 #||
+(value :q)
+(load "check-system-guards-raw.lsp")
+(add-guards-as-assertions-all)
 (lp)
 (set-rewrite-stack-limit nil)
 ; This may cause a stack overflow, but that's OK.
 (ld ; linebreak to avoid warning during regression
  "../workshops/2004/legato/support/proof-by-generalization-mult.lisp") ; ;
-:ubt 1
+(ubt 1)
 (ld ; linebreak to avoid warning during regression
  "../projects/hexnet/hexnet-model.lisp")
-:q
+(value :q)
 (report-guard-checks) ; should show lots of checking
 ||#
 
@@ -69,5 +72,7 @@
                (mini-proveall)))
 
 ; We can report results during both passes of certification.
+; But note that we will not be able to include this book in
+; a new session, because report-guard-checks will be undefined!
 (progn! (set-raw-mode t)
         (report-guard-checks))

workshops.html

@@ -15,7 +15,8 @@ <H1>The <A HREF="http://www.cs.utexas.edu/users/moore/acl2/index.html">ACL2</A>
 (Formal Methods in Computer Aided Design).
 <p>
 <UL>
-<LI>ACL2 Workshop 2020: (Details to come later) About two days between 26 May and 29 May, 2020, Austin, Texas, USA.</LI>
+<LI><A HREF="http://www.acl2-2020.info">ACL2 Workshop 2020</A>: May
+  28-29, 2020 (held online via video streaming).</LI>
 <LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2018/index.html">ACL2
     Workshop 2018</A>: November 5-6, 2018, Austin, Texas, USA.</LI>
 <LI><A HREF="http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/index.html">ACL2 Workshop 2017</A>: May 22 - 23, 2017, Austin, Texas, USA.</LI>