← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/ccg/ccg.acl2

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/ccg/ccg.acl2
1
 
; cert-flags: ? nil :ttags (:ccg)
2
 
 
3
 
; Here is a low-level explanation of the change by Matt Kaufmann, 8/4/2013, of
4
 
; the third argument of certify-book (below) from t to nil:
5
 
 
6
 
; We avoid compiling this book in order to avoid certification errors in some
7
 
; Lisps (in particular, we have seen one in an ACL2(h) regression with
8
 
; Lispworks), and to avoid errors when attempting to include this book in
9
 
; perhaps every Lisp.  It appears that the problem is with the use of
10
 
; defmacro-raw, which calls assert-unbound to cause an error when such a
11
 
; macro's definition is attempted while the macro is already defined.  If you
12
 
; save the expansion file (ccg@expansion.lsp) when attempting to certify this
13
 
; book, using (assign save-expansion-file t), then you'll see that the macro
14
 
; context-fn, defined by defmacro-raw, isn't mentioned in *hcomp-macro-alist*,
15
 
; and hence isn't made undefined after an early load of the compiled file.
16
 
; Indeed, if we look at the definition of defmacro-raw in hacking/raw.lisp,
17
 
; we'll see that while there is some attempt to maintain the undo-stack
18
 
; appropriately, there appears to be nothing that addresses the problem
19
 
; mentioned above of failing to unbind the definition after early load of the
20
 
; compiled file.  I'm not sufficiently familiar with the hacking/ stuff to know
21
 
; how best to fix this, but since trust tags are used, that's the
22
 
; responsibility of whomever is maintaining these books.
23
 
 
24
 
(certify-book "ccg" ? nil :ttags (:ccg))