Greetings!
Matt Kaufmann <[EMAIL PROTECTED]> writes:
> Hi, Camm --
>
> I'm attempting to build an experimental version of ACL2 on top of a recent GCL
> 2.7.0 built by Bob Boyer, and have run into one problem and two confusing
> (sets
> of) warnings.
>
> [I'd be happy to spare Bob or include gcl-devel on 2.7.0 emails like this;
> someone please let me know if I should do either.]
>
> ============================================================
>
> This one has an easy work-around, but it wasn't a problem in earlier versions
> of GCL (or any other Lisp I've built ACL2 upon).
>
> >(setf (documentation nil 'variable) "Some documentation.")
>
> NIL is not of type (AND SYMBOL (NOT NULL)).
>
> Fast links are on: do (si::use-fast-links nil) for debugging
> Broken at ERROR. Type :H for Help.
> 1 (Continue) The value NIL bound to variable OBJECT is not (AND SYMBOL (NOT
> NULL)) -- choose a new value
> 2 Return to top level.
> dbl:>>
I'll fix this, I don't think this should be an error, its just a bug
in my documentation 'fix'.
>
> ============================================================
>
> On another issue: What should I make of this warning (and many others like
> it)?
>
> ; (DEFUN FLSZ-INTEGER ...) is being compiled.
> ;; Warning: arg type mismatch in auto-proclamation (T (UNSIGNED-BYTE 5)
> (SIGNED-BYTE 29)) -> (T
>
> LISP:SEQIND
>
> FIXNUM)
>
As you know, 2.7.0 is right in the middle of an autoproclamation
feature installation. I'm glad you are testing as is it most helpful
-- I especially glad that you are apparently not faint of heart :-)
(We need more of such.)
The algorithm in place right now for function signature inference
cannot support the full granularity of types gcl knows about. This is
to support recursive function inference -- we start assuming the
return type is nil, calculate the type, bump the type upwards into a
set of "useful" types, and recompile, until we get the same answer. I
ran into this compiling an old maxima function like
(defun foo (x)
(declare (fixnum x))
(cond ((<= x 0) 0) (t (the fixnum (+ 1 (foo (the fixnum (1-
x))))))))
First the return type was '(integer 0 0), then '(integer 0 1) ....
Eventually we'll improve the granularity. You can ignore this warning
for now. 'seqind is something like '(unsigned-byte 28), btw.
> ============================================================
>
> Finally, I don't know why there is a complaint about ACTUAL-ALIST in the
> warning below. It goes away (of course, since it's from /tmp/recompile.lsp)
> if
> I start with (setq si::*disable-recompile* t), which is what I'm doing for
> now.
>
> ;; Compiling /tmp/recompile.lsp.
> ; (DEFUN INCLUDE-BOOK-FN ...) is being compiled.
> ;; Warning: The variable CERT-ANNOTATIONS is not used.
> ;; Warning: The variable ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL is not used.
> ;; Warning: The variable ACTUAL-ALIST is not used.
> ;; Warning: The variable ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL is not used.
> ;; Warning: The variable ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL is not used.
> ;; Warning: The variable ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL is not used.
> ;; End of Pass 1.
> ;; End of Pass 2.
>
To support recompilation, we try to capture the compile time state as
best as possible. This might not yet be perfect. On the other hand,
infomation obtained from previous recompiles might have made the
compiler think that it could eliminate an unreachable branch. I would
suggest:
compile with *disable-recompile* to t
(in-package 'si)
(function-src 'include-book-fn)
(setq compiler::*suppress-compiler-notes* nil)
(disassemble (function-src 'include-book-fn) nil)
I'll try to do same soon.
The function that computes the 'portable' source is
compiler::portable-source. I just committed an enhancement to
preserve '(case ccase and ecase) as opposed to macroexpanding them,
FYI.
I hope you are OK with this being a work in progress over the next few
days or maybe weeks. That said, I'd appreciate knowing what you think
of the concept. Perhaps Bob could share earlier emails on the subject
with you if you have interest.
You might also be interested in the automatic mutual-recursion ->
state function code I'm working on. If so:
cd unixport
./saved_ansi_gcl
(compile-file "../bench/takr.cl")
(load "../bench/takr.o")
(dotimes (i 100) (tak0 18 12 6))
(compile (si::convert-to-state 'tak0))
(dotimes (i 100) (tak0 18 12 6))
Comments suggestions most welcome.
Also, Please ignore the build time increase for now -- it should be
temporary. All recompilations should be postponed to the end via the
*disable-recompile* switch. We could even flush the hash table too
before image finalization for spae reasons too if desired.
Take care,
> (defun include-book-fn (user-book-name state
> load-compiled-file
> expansion-alist
> uncertified-okp
> defaxioms-okp
> skip-proofs-okp
> doc
> dir
> event-form)
>
> ; Expansion-alist is :none if this is not called by certify-book-fn.
> ; Otherwise, it is an expansion-alist generated from make-event calls.
>
> (with-ctx-summarized
> (if (output-in-infixp state) event-form (cons 'include-book
> user-book-name))
> (let* ((wrld0 (w state))
> (behalf-of-certify-flg (not (eq expansion-alist :none)))
> #-acl2-loop-only (*inside-include-book-fn* t)
> (old-include-book-path
> (global-val 'include-book-path wrld0))
> (saved-acl2-defaults-table
> (table-alist 'acl2-defaults-table wrld0))
> (cddr-event-form
> (if event-form
> (cddr event-form)
> (append
> (if (not (eq load-compiled-file :warn))
> (list :load-compiled-file
> load-compiled-file)
> nil)
> (if (not (eq uncertified-okp t))
> (list :uncertified-okp
> uncertified-okp)
> nil)
> (if (not (eq defaxioms-okp t))
> (list :defaxioms-okp
> defaxioms-okp)
> nil)
> (if (not (eq skip-proofs-okp t))
> (list :skip-proofs-okp
> skip-proofs-okp)
> nil)
> (if doc
> (list :doc doc)
> nil))))
> #+(and clisp (not acl2-loop-only))
> (custom::*suppress-check-redefinition* t)
> #+(and allegro (not acl2-loop-only))
> (excl:*redefinition-warnings* nil)
> )
> (er-let*
> ((dir-value
> (cond (dir (include-book-dir-with-chk soft ctx dir))
> (t (value (cbd))))))
> (mv-let
> (full-book-name directory-name familiar-name)
> (parse-book-name dir-value user-book-name ".lisp" (os (w state)))
>
> ; If you add more keywords to the suspect-book-action-alist, make sure you do
> ; the same to the list constructed by certify-book-fn. You might wish to
> ; handle the new warning summary in warning1.
>
> (let ((suspect-book-action-alist
> (list (cons :uncertified-okp
> (if (assoc 'certify-book
> (global-val 'embedded-event-lst
> wrld0))
> nil
> uncertified-okp))
> (cons :defaxioms-okp defaxioms-okp)
> (cons :skip-proofs-okp skip-proofs-okp))))
> (er-progn
> (chk-book-name user-book-name full-book-name ctx state)
> (chk-input-object-file full-book-name ctx state)
> (revert-world-on-error
> (cond
> ((and (not (global-val 'boot-strap-flg wrld0))
> full-book-name
> (assoc-equal full-book-name
> (global-val 'include-book-alist wrld0)))
> (stop-redundant-event state))
> (t
> (let ((wrld1 (global-set
> 'include-book-path
> (cons full-book-name old-include-book-path)
> wrld0)))
> (pprogn
> (set-w 'extension wrld1 state)
> (er-let*
> ((redef (chk-new-stringp-name 'include-book full-book-name
> ctx wrld1 state))
> (doc-pair (translate-doc full-book-name doc ctx state))
> (cert-obj (if behalf-of-certify-flg
> (value nil)
> (chk-certificate-file full-book-name nil ctx
> state
> suspect-book-action-alist
> t)))
> (expansion-alist (value (if behalf-of-certify-flg
> expansion-alist
> (and cert-obj
> (access cert-obj cert-obj
>
> :expansion-alist)))))
> (post-alist (value (and cert-obj
> (access cert-obj cert-obj
> :post-alist))))
> (cert-full-book-name (value (car (car post-alist)))))
> (cond
>
> ; We try the redundancy check again, because it will be cert-full-book-name
> ; that is stored on the world's include-book-alist, not full-book-name (if the
> ; two book names differ).
>
> ((and (not (equal full-book-name cert-full-book-name))
> (not (global-val 'boot-strap-flg wrld1))
> cert-full-book-name
> (assoc-equal cert-full-book-name
> (global-val 'include-book-alist wrld1)))
>
> ; Chk-certificate-file calls chk-certificate-file1, which calls
> ; chk-raise-portcullis, which calls chk-raise-portcullis1, which evaluates,
> for
> ; example, maybe-install-acl2-defaults-table. So we need to revert the world
> ; here.
>
> (pprogn (set-w 'retraction wrld0 state)
> (stop-redundant-event state)))
> (t
> (er-let*
> ((ev-lst (read-object-file full-book-name ctx state)))
>
> ; Cert-obj above is either nil, indicating that the file is uncertified, or is
> ; a cert-obj record, which contains the now raised portcullis and the check
> sum
> ; alist of the files that should be brought in by this inclusion. The first
> ; element of post-alist is the one for this book. It should look like this:
> ; (full-book-name' user-book-name' familiar-name cert-annotations
> ; . ev-lst-chk-sum), where the first two names are irrelevant here because
> they
> ; reflect where the book was when it was certified rather than where the book
> ; resides now. However, the familiar-name, cert-annotations and the
> ; ev-lst-chk-sum ought to be those for the current book.
>
> (mv-let
> (ev-lst-chk-sum state)
> (check-sum-obj (append expansion-alist ev-lst) state)
> (cond
> ((not (integerp ev-lst-chk-sum))
>
> ; This error should never arise because check-sum-obj is only called on
> ; something produced by read-object, which checks that the object is ACL2
> ; compatible, and perhaps make-event expansion. The next form causes a soft
> ; error, assigning proper blame.
>
> (mv-let
> (raw-ev-lst-chk-sum state)
> (check-sum-obj ev-lst state)
> (cond ((not (integerp raw-ev-lst-chk-sum))
> (er soft ctx
> "The file ~x0 is not a legal list of ~
> embedded event forms because it ~
> contains an object, ~x1, which check ~
> sum was unable to handle."
> full-book-name raw-ev-lst-chk-sum))
> (t
> (mv-let
> (expansion-chk-sum state)
> (check-sum-obj expansion-alist state)
> (cond
> ((not (integerp expansion-chk-sum))
> (er soft ctx
> "The expansion-alist (from ~
> make-event) for file ~x0 is not a ~
> legal list of embedded event forms ~
> because it contains an object, ~x1, ~
> which check sum was unable to
> handle."
> full-book-name expansion-chk-sum))
> (t (er soft ctx
> "The append of expansion-alist ~
> (from make-event) and command for ~
> file ~x0 is not a legal list of ~
> embedded event forms because it ~
> contains an object, ~x1, which ~
> check sum was unable to handle. ~
> This is very surprising,because ~
> check sums were computed ~
> successfully for the ~
> expansion-alist and the commands.
> ~
> It would be helpful for you to ~
> send a replayable example of this ~
> behavior to the ACL2 implementors."
> full-book-name
> ev-lst-chk-sum))))))))
> (t (er-progn
>
> ; Notice that we are reaching inside the certificate object to retrieve
> ; information about the book from the post-alist. (Car post-alist)) is in
> fact
> ; of the form (full-book-name user-book-name familiar-name cert-annotations
> ; . ev-lst-chk-sum).
>
>
> (cond
> ((and cert-obj
> (not (equal (caddr (car post-alist))
> familiar-name)))
> (include-book-er
> full-book-name nil
> (cons
> "The cer~-ti~-fi~-cate on file for ~x0 lists ~
> the book under the name ~x3 whereas we were ~
> expecting it to give the name ~x4. While we
> ~
> allow a certified book to be moved from one ~
> directory to another after ~
> cer~-ti~-fi~-ca~-tion, we insist that it
> keep ~
> the same familiar name. This allows the ~
> cer~-ti~-fi~-cate file to contain the ~
> familiar name, making it easier to identify ~
> which cer~-ti~-fi~-cates go with which files
> ~
> and inspiring a little more confidence that ~
> the cer~-ti~-fi~-cate really does describe ~
> the alleged file. In the present case, it ~
> looks as though the familiar book name was ~
> changed after cer~-ti~-fi~-ca~-tion. For ~
> what it is worth, the check sum of the file ~
> at cer~-ti~-fi~-ca~-tion was ~x5. Its check
> ~
> sum now is ~x6."
> (list (cons #\3 (caddr (car post-alist)))
> (cons #\4 familiar-name)
> (cons #\5 (cddddr (car post-alist)))
> (cons #\6 ev-lst-chk-sum)))
> :uncertified-okp
> suspect-book-action-alist
> ctx state))
> (t (value nil)))
>
> (cond
> ((and cert-obj
> (not (equal (cddddr (car post-alist))
> ev-lst-chk-sum)))
> (include-book-er
> full-book-name nil
> (cons
> "The certificate on file for ~x0 lists the ~
> check sum of the certified book as ~x3. But
> ~
> the check sum of the events now in the file ~
> is ~x4. This generally indicates that the ~
> file has been modified since it was last ~
> certified."
> (list (cons #\3 (cddddr (car post-alist)))
> (cons #\4 ev-lst-chk-sum)))
> :uncertified-okp
> suspect-book-action-alist
> ctx state))
> (t (value nil)))
>
> (let ((cert-annotations (cadddr (car
> post-alist))))
>
> ; It is possible for cert-annotations to be nil now. That is because
> cert-obj was
> ; nil. But we never use it if cert-obj is nil.
>
> (cond
> ((and cert-obj
> (or (cdr (assoc :skipped-proofsp
> cert-annotations))
> (cdr (assoc :axiomsp
> cert-annotations))))
>
> (chk-cert-annotations cert-annotations
> (access cert-obj
> cert-obj
> :cmds)
> full-book-name
>
> suspect-book-action-alist
> ctx state))
> (t (value nil))))
>
> ; The following process-embedded-events is protected by the revert-world-
> ; on-error above. See the Essay on Guard Checking for a discussion of the
> ; binding of guard-checking-on below.
>
> (state-global-let*
> ((skipped-proofsp nil)
> (axiomsp nil)
> (connected-book-directory directory-name)
> (match-free-error nil)
> (guard-checking-on nil)
> (in-local-flg
>
> ; As we start processing the events in the book, we are no longer in the
> ; lexical scope of LOCAL for purposes of disallowing setting of the
> ; acl2-defaults-table.
>
> (and (f-get-global 'in-local-flg state)
> 'dynamic)))
> (let ((skip-proofsp
> (if (or cert-obj behalf-of-certify-flg)
> 'include-book
>
> ; If we are including an uncertified book, then we want to do some of the
> checks.
>
> 'initialize-acl2)))
> (process-embedded-events
> 'include-book
> event-form
> saved-acl2-defaults-table
> skip-proofsp
> (cadr (car ev-lst))
> (list 'include-book full-book-name)
> (subst-by-position expansion-alist
> (cdr ev-lst)
> 1)
> 1
> (eq skip-proofsp 'include-book)
> ctx state)))
>
> ; This function returns what might be called proto-wrld3, which is
> ; equivalent to the current world of state before the
> ; process-embedded-events (since the insigs argument is nil), but it has
> ; an incremented embedded-event-depth. We don't care about this
> ; world. The interesting world is the one current in the state
> ; returned by by process-embedded-events. It has all the embedded
> ; events in it and we are done except for certification issues.
>
> (let* ((wrld2 (w state))
> (actual-alist (global-val
> 'include-book-alist
> wrld2)))
> (er-progn
> (cond
> ((and cert-obj
> (not (include-book-alist-subsetp
>
> (unmark-and-delete-local-included-books
> (cdr post-alist))
> actual-alist)))
> (include-book-er
> full-book-name nil
> (cons "The certified book ~x0 requires ~*3
> but ~
> we have ~*4."
> (list
> (cons #\3
> (tilde-*-book-check-sums-phrase
> t
>
> (unmark-and-delete-local-included-books
> (cdr post-alist))
> actual-alist))
> (cons #\4
> (tilde-*-book-check-sums-phrase
> nil
>
> (unmark-and-delete-local-included-books
> (cdr post-alist))
> actual-alist))))
> :uncertified-okp
> suspect-book-action-alist
> ctx state))
> (t (value nil)))
>
> ; Now we check that all the subbooks of this one are also compatible with the
> ; current settings of suspect-book-action-alist. The car of post-alist is the
> ; part that deals with full-book-name itself. So we deal below with the cdr,
> ; which lists the subbooks. The cert-obj may be nil, which makes the test
> ; below a no-op.
>
> (chk-cert-annotations-post-alist
> (cdr post-alist)
> (and cert-obj
> (access cert-obj cert-obj :cmds))
> full-book-name
> suspect-book-action-alist
> ctx state)
>
> (let* ((cert-annotations
> (cadddr (car post-alist)))
>
> ; If cert-obj is nil, then cert-annotations is nil. If cert-obj is
> ; non-nil, then cert-annotations is non-nil. Cert-annotations came
> ; from a .cert file, and they are always non-nil. But in the
> ; following, cert-annotations may be nil.
>
> (certification-tuple
> (cond
> ((and cert-obj
> (equal (caddr (car post-alist))
> familiar-name)
> (equal (cddddr (car post-alist))
> ev-lst-chk-sum)
> (include-book-alist-subsetp
>
> (unmark-and-delete-local-included-books
> (cdr post-alist))
> actual-alist))
>
> ; Below we use the full book name from the certificate, cert-full-book-name,
> ; rather than full-book-name (from the parse of the user-book-name), in
> ; certification-tuple, Intuitively, cert-full-book-name is the unique
> ; representative of the class of all legal full book names (including those
> ; that involve soft links). Before Version_2.7 we used full-book-name rather
> ; than cert-full-book-name, and this led to problems as shown in the example
> ; below.
>
> #|
> % ls temp*/*.lisp
> temp1/a.lisp temp2/b.lisp temp2/c.lisp
> % cat temp1/a.lisp
> (in-package "ACL2")
> (defun foo (x) x)
> % cat temp2/b.lisp
> (in-package "ACL2")
> (defun goo (x) x)
> % cat temp2/c.lisp
> (in-package "ACL2")
> (defun hoo (x) x)
> %
>
> Below, two absolute pathnames are abbreviated as <path1> and <path2>.
>
> In temp2/ we LD a file with the following forms.
>
> (certify-book "<path1>/a")
> :u
> (include-book "../temp1/a")
> (certify-book "b" 1)
> :ubt! 1
> (include-book "b")
> (certify-book "c" 1)
>
> We then see the following error. The problem is that <path1> involved
> symbolic
> links, and hence did not match up with the entry in the world's
> include-book-alist made by (include-book "../temp1/a") which expanded to an
> absolute pathname that did not involve symbolic links.
>
> ACL2 Error in (CERTIFY-BOOK "c" ...): During Step 3 , we loaded different
> books than were loaded by Step 2! Perhaps some other user of your
> file system was editing the books during our Step 3? You might think
> that some other job is recertifying the books (or subbooks) and has
> deleted the certificate files, rendering uncertified some of the books
> needed here. But more has happened! Some file has changed!
>
> Here is the include-book-alist as of the end of Step 2:
> (("<path2>/temp2/c.lisp"
> "c" "c" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 48180423)
> ("<path2>/temp2/b.lisp"
> "b" "b" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 46083312)
> (LOCAL ("<path1>/a.lisp"
> "<path1>/a"
> "a" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 43986201))).
>
> And here is the alist as of the end of Step 3:
> (("<path2>/temp2/c.lisp"
> "c" "c" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 48180423)
> ("<path2>/temp2/b.lisp"
> "b" "b" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 46083312)
> ("<path2>/temp1/a.lisp"
> "<path2>/temp1/a"
> "a" ((:SKIPPED-PROOFSP) (:AXIOMSP))
> . 43986201)).
>
> Frequently, the former has more entries than the latter because the
> former includes LOCAL books. So compare corresponding entries, focusing
> on those in the latter. Each entry is of the form (name1 name2 name3
> alist . chk-sum). Name1 is the full name, name2 is the name as written
> in an include-book event, and name3 is the ``familiar'' name of the
> file. The alist indicates the presence or absence of problematic forms
> in the file, such as DEFAXIOM events. For example, (:AXIOMSP . T)
> means there were defaxiom events; (:AXIOMSP . NIL) -- which actually
> prints as (:AXIOMSP) -- means there were no defaxiom events. Finally,
> chk-sum is either an integer check sum on the contents of the file
> at the time it was certified or else chk-sum is nil indicating that
> the file is not certified. Note that if the chk-sum is nil, the entry
> prints as (name1 name2 name3 alist). Go figure.
>
>
> Summary
> Form: (CERTIFY-BOOK "c" ...)
> Rules: NIL
> Warnings: Guards
> Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
>
> ******** FAILED ******** See :DOC failure ******** FAILED ********
> :ERROR
> ACL2 !>
>
> |#
>
> (list* cert-full-book-name
> user-book-name
> familiar-name
> cert-annotations
> ev-lst-chk-sum))
> (t
>
> ; The certification tuple below is marked as uncertified because the
> ; ev-lst-chk-sum is nil. What about cert-annotations? It may or may
> ; not correctly characterize the file, it may even be nil. Is that
> ; bad? No, the check sum will always save us.
>
> (list* full-book-name
> user-book-name
> familiar-name
> cert-annotations
> nil))))
> (wrld3
> (global-set
> 'include-book-path
> old-include-book-path
> (update-doc-data-base
> full-book-name doc doc-pair
> (global-set
> 'certification-tuple
> certification-tuple
> (global-set 'include-book-alist
> (add-to-set-equal
> certification-tuple
> (global-val
> 'include-book-alist
> wrld2))
> wrld2))))))
> (pprogn
> #-acl2-loop-only
> (progn
> (load-compiled-file-if-more-recent
> ctx load-compiled-file full-book-name
> directory-name expansion-alist ev-lst)
> state)
> (redefined-warning redef ctx state)
> (f-put-global 'include-book-alist-state
> (add-to-set-equal
> certification-tuple
> (union-equal
> (cdr post-alist)
> (f-get-global
> 'include-book-alist-state
> state)))
> state)
> (install-event
> (if behalf-of-certify-flg
> ev-lst-chk-sum
> (or cert-full-book-name
> full-book-name))
> (list* 'include-book
>
> ; We use the the unique representative of the full book name provided by the
> ; one in the .cert file, when the certificate is valid before execution of
> this
> ; event), namely, cert-full-book-name; otherwise, we use the full-book-name
> ; parsed from what the user supplied. Either way, we have an absolute path
> ; name, which is useful for the :puff and :puff* commands. These could fail
> ; before Version_2.7 because the relative path name stored in the event was
> not
> ; sufficient to find the book at :puff/:puff* time.
>
> (or cert-full-book-name
> full-book-name)
> cddr-event-form)
> 'include-book
> full-book-name
> nil nil t ctx wrld3
> state)))))))))))))))))))))))))
>
> In case it helps, here are the functions that are called above on
> actual-alist.
>
> (defun tilde-*-book-check-sums-phrase (flg reqd-alist actual-alist)
>
> ; Flg is t or nil and the two alists each contain pairs of the form
> ; (full-book-name user-book-name familiar-name cert-annotations
> ; . ev-lst-chk-sum). Reqd-Alist shows what is required and
> ; actual-alist shows that is actual. We know reqd-alist ought to be a
> ; `include-book alist subset' of actual-alist but it is not. If flg
> ; is t we complete the phrase "this book requires ..." and if flg is
> ; nil we complete "but we have ...".
>
> (list "" "[EMAIL PROTECTED]" "[EMAIL PROTECTED] and " "[EMAIL PROTECTED], "
> (tilde-*-book-check-sums-phrase1 flg
> (strip-cddrs reqd-alist)
> (strip-cddrs actual-alist))))
>
> (defun include-book-alist-subsetp (alist1 alist2)
>
> ; The include-book-alist contains elements of the
> ; general form example value
>
> ; (full-book-name ; "/usr/home/moore/project/arith.lisp"
> ; user-book-name ; "project/arith.lisp"
> ; familiar-name ; "arith"
> ; cert-annotations ; ((:SKIPPED-PROOFSP . sp) (:AXIOMSP . axp))
> ; . ev-lst-chk-sum) ; 12345678
>
> ; The include-book-alist becomes part of the certificate for a book,
> ; playing a role in both the pre-alist and the post-alist. In the
> ; latter role some elements may be marked (LOCAL &). When we refer to
> ; parts of the include-book-alist entries we have tried to use the
> ; tedious names above, to help us figure out what is used where.
> ; Please try to preserve this convention.
>
> ; Cert-annotations is an alist. As of this writing (ACL2 Version_2.5)
> ; the alist has two possible keys, :SKIPPED-PROOFSP and :AXIOMSP. The
> ; possible values of both are t, nil, or ?, indicating the presence, absence,
> ; or possible presence of skip-proof forms or defaxioms, respectively. The
> ; forms in question may be either LOCAL or non-LOCAL and are in the book
> ; itself (not just in some subbook). Even though the cert-annotations is an
> ; alist, we compare include-book-alists with equality on that component, not
> ; ``alist equality.'' So we are NOT free to drop or rearrange keys in these
> ; annotations.
>
> ; If the book is uncertified, the chk-sum entry is nil.
>
> ; Suppose the two alist arguments are each include-book-alists from
> ; different times. We check that the first is a subset of the second,
> ; in the sense that the (familiar-name cert-annotations . chk-sum)
> ; parts of the first are all among those of the second. We ignore the
> ; full names and the user names because they may change as the book or
> ; connected book directory moves around.
>
> (subsetp-equal (strip-cddrs alist1)
> (strip-cddrs alist2)))
>
> ============================================================
>
> Thanks --
> -- Matt
>
>
>
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
_______________________________________________
Gcl-devel mailing list
Gcl-devel@gnu.org
http://lists.gnu.org/mailman/listinfo/gcl-devel
