3050
3092
theory invariant by setting the invariant to ~c[t], or eliminate all theory
3051
3093
invariants with the command ~c[(table theory-invariant-table nil nil :clear)].
3053
~c[Theory-invariant-table] maps arbitrary keys to terms mentioning, at
3054
most, the variables ~ilc[theory] and ~ilc[world]. Every time an alleged theory
3055
expression is evaluated, e.g., in the ~ilc[in-theory] event or ~c[:]~ilc[in-theory]
3056
hint, each of the terms in ~c[theory-invariant-table] is evaluated with
3057
~ilc[theory] bound to the runic theory (~pl[theories]) obtained from
3058
the theory expression and ~ilc[world] bound to the current ACL2 ~il[world]
3059
(~pl[world]). If the result is ~c[nil], a message is printed and an error
3060
occurs (except, only a warning occurs if ~c[:error nil] is specified). Thus,
3061
the ~il[table] can be thought of as a list of conjuncts. Each ~c[term] in
3062
the ~il[table] has a ``name,'' which is just the key under which the term is
3063
stored. When a theory violates the restrictions specified by some term, both
3064
the name and the term are printed. By calling ~c[theory-invariant] with a
3065
new term but the same name, you can overwrite that conjunct of the theory
3066
invariant; but see the Local Redefinition Caveat at the end of this note.
3067
You may want to avoid using explicit names, since otherwise the subsequent
3068
inclusion of another book that defines a theory invariant with the same name
3069
will override your theory invariant.
3095
~c[Theory-invariant-table] maps arbitrary keys to records containing terms
3096
that mention, at most, the variables ~c[ens] and ~ilc[state]. Every time an
3097
alleged theory expression is evaluated, e.g., in the ~ilc[in-theory] event or
3098
~c[:]~ilc[in-theory] hint, each of the terms in ~c[theory-invariant-table] is
3099
evaluated with ~c[ens] bound to a so-called ``enabled structure'' obtained
3100
from the theory expression and ~ilc[state] bound to the current ACL2 state
3101
(~pl[state]). Users generally need not know about the enabled structure,
3102
other than that it can be accessed using the macros ~c[active-runep] and
3103
~c[incompatible]; ~pl[active-runep] and ~pl[incompatible]. If the result is
3104
~c[nil], a message is printed and an error occurs (except, only a warning
3105
occurs if ~c[:error nil] is specified). Thus, the ~il[table] can be thought
3106
of as a list of conjuncts. Each ~c[term] in the ~il[table] has a ``name,''
3107
which is just the key under which the term is stored. When a theory violates
3108
the restrictions specified by some term, both the name and the term are
3109
printed. By calling ~c[theory-invariant] with a new term but the same name,
3110
you can overwrite that conjunct of the theory invariant; but see the Local
3111
Redefinition Caveat at the end of this note. You may want to avoid using
3112
explicit names, since otherwise the subsequent inclusion of another book that
3113
defines a theory invariant with the same name will override your theory
3071
Theory invariants are particularly useful in the context of large
3072
rule sets intended for re-use. Such sets often contain conflicting
3073
rules, e.g., rules that are to be ~il[enable]d when certain function
3074
symbols are ~il[disable]d, rules that rewrite in opposite directions and
3075
thus loop if simultaneously ~il[enable]d, groups of rules which should be
3076
~il[enable]d in concert, etc. The developer of such rule sets
3077
understands these restrictions and probably documents them. The
3078
theory invariant mechanism allows the developer to codify his
3079
restrictions so that the user is alerted when they are violated.
3116
Theory invariants are particularly useful in the context of large rule sets
3117
intended for re-use. Such sets often contain conflicting rules, e.g., rules
3118
that are to be ~il[enable]d when certain function symbols are ~il[disable]d,
3119
rules that rewrite in opposite directions and thus loop if simultaneously
3120
~il[enable]d, groups of rules which should be ~il[enable]d in concert, etc.
3121
The developer of such rule sets understands these restrictions and probably
3122
documents them. The theory invariant mechanism allows the developer to
3123
codify his restrictions so that the user is alerted when they are violated.
3081
3125
Since theory invariants are arbitrary terms, macros may be used to
3082
3126
express commonly used restrictions. For example, executing the event
4336
4436
(t (append (car wrappers)
4337
4437
(list (rebuild-expansion (cdr wrappers) form))))))
4339
(defun eval-event-lst (index expansion-alist ev-lst orig-form quietp
4340
in-encapsulatep in-local-flg last-val
4341
make-event-chk ctx channel state)
4439
(defun set-raw-mode-on (state)
4441
(cond ((raw-mode-p state)
4442
(fms "No change: raw mode is already on.~|"
4443
nil (standard-co state) state nil))
4445
(pprogn (fms "Entering raw-mode.~|" nil (standard-co state) state nil)
4446
(f-put-global 'acl2-raw-mode-p t state))))
4447
(value :invisible)))
4449
(defun set-raw-mode-off (state)
4451
(cond ((raw-mode-p state)
4452
(pprogn (fms "Leaving raw-mode.~|" nil (standard-co state) state nil)
4453
(f-put-global 'acl2-raw-mode-p nil state)))
4455
(fms "No change: raw mode is already off.~|"
4456
nil (standard-co state) state nil)))
4457
(value :invisible)))
4459
(defmacro set-raw-mode-on! ()
4463
enter ``raw mode,'' a raw Lisp environment~/
4465
This is the same as ~c[(]~ilc[set-raw-mode]~c[ t)] except that it first
4466
introduces a so-called ``trust tag'' (``ttag'') so that ~c[set-raw-mode] will
4467
be legal. ~l[defttag] for a discussion of ttags and how they affect
4468
~ilc[certify-book] and ~ilc[include-book].~/~/"
4470
'(er-progn (ld '((defttag :raw-mode-hack)
4471
(set-raw-mode-on state))
4472
:ld-prompt nil :ld-verbose nil :ld-post-eval-print nil)
4473
(value :invisible)))
4475
(defmacro set-raw-mode (flg)
4476
(declare (xargs :guard (member-equal flg '(t 't nil 'nil))))
4480
enter or exit ``raw mode,'' a raw Lisp environment~/
4482
ACL2 users often find its careful syntax checking to be helpful during code
4483
development. Sometimes it is even useful to do code development in
4484
~c[:]~ilc[logic] mode, where ACL2 can be used to check termination of
4485
(mutually) recursive functions, verify guards, or even prove properties of
4488
However, loading code using ~ilc[include-book] is much slower than using
4489
Common Lisp ~c[load] in raw Lisp, and in this sense ACL2 can get in the way
4490
of efficient execution. Unfortunately, it is error-prone to use ACL2 sources
4491
(or their compilations) in raw Lisp, primarily because a number of ACL2
4492
primitives will not let you do so. Perhaps you have seen this error message
4493
when trying to do so:
4495
HARD ACL2 ERROR in ACL2-UNWIND-PROTECT: Apparently you have tried
4496
to execute a form in raw Lisp that is only intended to be executed
4497
inside the ACL2 loop.
4499
Even without this problem it is important to enter the ACL2 loop (~pl[lp]),
4500
for example in order to set the ~ilc[cbd] and (to get more technical) the
4503
ACL2 provides a ``raw mode'' for execution of raw Lisp forms. In this mode,
4504
~ilc[include-book] reduces essentially to a Common Lisp ~c[load]. More
4505
generally, the ACL2 logical ~ilc[world] is not routinely extended in raw mode
4506
(some sneaky tricks are probably required to make that happen). To turn raw
4509
:set-raw-mode t ; turn raw mode on
4510
:set-raw-mode nil ; turn raw mode off
4513
The way you can tell that you are in raw mode is by looking at the prompt
4514
(~pl[default-print-prompt]), which uses a capital ``~c[P]'' (suggesting
4515
something like program mode, but more so).
4520
Typical benefits of raw mode are fast loading of source and compiled files
4521
and the capability to hack arbitrary Common Lisp code in an environment with
4522
the ACL2 sources loaded (and hence with ACL2 primitives available). In
4523
addition, ACL2 hard errors will put you into the Lisp debugger, rather than
4524
returning you to the ACL2 loop, and this may be helpful for debugging;
4525
~pl[hard-error] and ~pl[illegal], but also ~pl[break-on-error]. However, it
4526
probably is generally best to avoid raw mode unless these advantages seem
4527
important. We expect the main benefit of raw mode to be in deployment of
4528
applications, where load time is much faster than the time required for a
4529
full-blown ~ilc[include-book], although in certain cases the fast loading of
4530
books and treatment of hard errors discussed above may be useful during
4533
Raw mode is also useful for those who want to build extensions of ACL2. For
4534
example, the following form can be put into a certifiable book to load an
4535
arbitrary Common Lisp source or compiled file.
4537
(progn! (defttag my-application)
4539
(load \"some-file\"))
4541
Also see ~c[with-raw-mode] defined in ~c[books/misc/hacker.lisp],
4542
~pl[defttag], and ~pl[progn!].
4544
Below are several disadvantages to raw mode. These should discourage users
4545
from using it for general code development, as ~c[:]~ilc[program] mode is
4546
generally preferable.
4548
-- Forms are in essence executed in raw Lisp. Hence:
4549
-- Syntax checking is turned off; and
4550
-- Guard checking is completely disabled.
4551
-- Table events, including ~ilc[logic], are ignored, as are many
4552
other ~ilc[events], including ~ilc[defthm] and ~ilc[comp].
4553
-- Soundness claims are weakened for any ACL2 session in which raw
4554
mode was ever entered; ~pl[defttag].
4555
-- The normal undoing mechanism (~pl[ubt]) is not supported.
4558
We conclude with some details.
4560
~em[Printing results]. The rules for printing results are unchanged for raw
4561
mode, with one exception. If the value to be printed would contain any Lisp
4562
object that is not a legal ACL2 object, then the ~c[print] routine is used
4563
from the host Lisp, rather than the usual ACL2 printing routine. The
4564
following example illustrates the printing used when an illegal ACL2 object
4565
needs to be printed. Notice how that ``command conventions'' are observed
4566
(~pl[ld-post-eval-print]); the ``~c[[Note]'' occurs one space over in the
4567
second example, and no result is printed in the third example.
4569
ACL2 P>(find-package \"ACL2\")
4570
[Note: Printing non-ACL2 result.]
4572
ACL2 P>(mv nil (find-package \"ACL2\") state)
4573
[Note: Printing non-ACL2 result.]
4575
ACL2 P>(mv t (find-package \"ACL2\") state)
4576
ACL2 P>(mv 3 (find-package \"ACL2\"))
4577
[Note: Printing non-ACL2 result.]
4578
(3 #<The ACL2 package>)
4581
If you have trouble with large structures being printed out, you might want
4582
to execute appropriate Common Lisp forms in raw mode, for example,
4583
~c[(setq *print-length* 5)] and ~c[(setq *print-level* 5)].
4585
~em[Packages]. Raw mode disallows the use of ~ilc[defpkg]. If you want to
4586
create a new package, first exit raw mode with ~c[:set-raw-mode nil];
4587
you can subsequently re-enter raw mode with ~c[:set-raw-mode t] if you
4591
(equal flg '(quote nil)))
4592
'(set-raw-mode-off state)
4593
'(set-raw-mode-on state)))
4596
(defun-one-output stobj-out (val)
4598
; Warning: This function assumes that we are not in the context of a local
4599
; stobj. As of this writing, it is only used in raw mode, so this does not
4600
; concern us too much. With raw mode, there are no guarantees.
4602
(if (eq val *the-live-state*)
4604
(car (rassoc val *user-stobj-alist* :test 'eq))))
4606
#-(or acl2-loop-only acl2-mv-as-values)
4609
; This silly function is just mv-ref, but without the restriction that the
4610
; argument be an explicit number.
4644
(otherwise (error "Illegal value for mv-ref!"))))
4646
(defmacro add-raw-arity (name val)
4647
(declare (xargs :guard (and (symbolp name)
4648
(or (and (integerp val) (<= 0 val))
4651
":Doc-Section Set-raw-mode
4653
add arity information for raw mode~/
4655
Technical note: This macro is a no-op, and is not necessary, when ACL2 is
4656
built with #-acl2-mv-as-values.
4658
Users of raw mode (~pl[set-raw-mode]) can use arbitrary raw Lisp functions
4659
that are not known inside the usual ACL2 loop. In such cases, ACL2 may not
4660
know how to display a multiple value returned by ACL2's ~ilc[mv] macro. The
4661
following example should make this clear.
4663
ACL2 P>(defun foo (x y) (mv y x))
4667
Note: Unable to compute number of values returned by this evaluation
4668
because function FOO is not known in the ACL2 logical world. Presumably
4669
it was defined in raw Lisp or in raw mode. Returning the first (perhaps
4670
only) value for calls of FOO.
4672
ACL2 P>(add-raw-arity foo 2)
4678
The first argument of ~c[add-raw-arity] should be a symbol, representing the
4679
name of a function, macro, or special form, and the second argument should
4680
either be a non-negative integer (denoting the number of values returned by
4681
ACL2) or else the symbol ~c[:LAST], meaning that the number of values
4682
returned by the call is the number of values returned by the last
4685
The current arity assignments can be seen by evaluating
4686
~c[(@ raw-arity-alist)]. ~l[remove-raw-arity] for how to undo a call of
4687
~c[add-raw-arity].~/"
4689
#+acl2-mv-as-values (declare (ignore name val))
4690
#+acl2-mv-as-values '(value nil)
4692
`(pprogn (f-put-global 'raw-arity-alist
4693
(put-assoc-eq ',name
4695
(f-get-global 'raw-arity-alist state))
4697
(value 'raw-arity-alist)))
4699
(defmacro remove-raw-arity (name)
4700
(declare (xargs :guard (symbolp name)))
4702
":Doc-Section Set-raw-mode
4704
remove arity information for raw mode~/
4706
Technical note: This macro is a no-op, and is not necessary, when ACL2 is
4707
built with #-acl2-mv-as-values.
4709
The form ~c[(remove-raw-arity fn)] undoes the effect of an earlier
4710
~c[(remove-raw-arity fn val)]. ~l[add-raw-arity].~/~/"
4712
#+acl2-mv-as-values (declare (ignore name))
4713
#+acl2-mv-as-values '(value nil)
4715
`(pprogn (f-put-global 'raw-arity-alist
4716
(delete-assoc-eq ',name
4717
(f-get-global 'raw-arity-alist
4720
(value 'raw-arity-alist)))
4722
#-(or acl2-loop-only acl2-mv-as-values)
4723
(defun raw-arity (form wrld state)
4726
((eq (car form) 'mv)
4727
(length (cdr form)))
4728
((eq (car form) 'if)
4729
(let ((arity1 (raw-arity (caddr form) wrld state)))
4731
(let ((arity2 (raw-arity (cadddr form) wrld state)))
4732
(if (eql arity1 arity2)
4734
(let ((min-arity (min arity1 arity2)))
4736
(warning$ 'top-level "Raw"
4737
"Unable to compute arity of the following ~
4738
IF-expression in raw mode because the true branch ~
4739
has arity ~x0 but the false branch has arity ~x1, ~
4740
so we assume an arity of ~x2 ~
4741
(see :DOC add-raw-arity):~% ~x3."
4742
arity1 arity2 min-arity form)
4745
(t (let ((arity (cdr (assoc-eq (car form)
4746
(f-get-global 'raw-arity-alist state)))))
4749
(raw-arity (car (last form)) wrld state))
4750
((and (integerp arity)
4754
(error "Ill-formed value of *raw-arity-alist*."))
4757
(getprop (car form) 'stobjs-out t 'current-acl2-world wrld)))
4760
(multiple-value-bind
4762
(macroexpand-1 form)
4765
; Remember that our notion of multiple value here is ACL2's notion, not Lisp's
4766
; notion. So the arity is 1 for calls of Common Lisp functions.
4768
(when (not (member-eq
4770
*common-lisp-symbols-from-main-lisp-package*))
4771
(fms "Note: Unable to compute number of values ~
4772
returned by this evaluation because function ~x0 ~
4773
is not known in the ACL2 logical world. ~
4774
Presumably it was defined in raw Lisp or in raw ~
4775
mode. Returning the first (perhaps only) value ~
4776
for calls of ~x0. See :DOC add-raw-arity.~|"
4777
(list (cons #\0 (car form)))
4778
*standard-co* state nil))
4780
(t (raw-arity new-form wrld state)))))
4781
(t (length stobjs-out))))))))))
4783
(defun alist-to-bindings (alist)
4786
(t (cons (list (caar alist) (kwote (cdar alist)))
4787
(alist-to-bindings (cdr alist))))))
4790
(defun-one-output acl2-raw-eval-form-to-eval (form)
4791
`(let ((state *the-live-state*)
4792
,@(alist-to-bindings *user-stobj-alist*))
4794
; OpenMCL prints "Unused lexical variable" warnings unless we take some
4795
; measures, which we do now. We notice that we need to include #+cmu for the
4796
; second form, so we might as well include it for the first, too.
4798
#+(or openmcl cmu sbcl)
4799
,@(mapcar #'(lambda (x) `(declare (ignorable ,(car x))))
4801
#+(or openmcl cmu sbcl)
4802
(declare (ignorable state))
4803
,(cond ((and (consp form)
4804
(eq (car form) 'in-package)
4805
(or (and (consp (cdr form))
4808
"IN-PACKAGE takes one argument. The form ~p0 is ~
4812
; The package must be one that ACL2 knows about, or there are likely to be
4813
; problems involving the prompt and the ACL2 reader. Also, we want the
4814
; in-package form to reflect in the prompt.
4816
(list 'in-package-fn (list 'quote (cadr form)) 'state))
4819
#-(or acl2-loop-only acl2-mv-as-values)
4820
(defun acl2-raw-eval (form state)
4821
(or (eq state *the-live-state*)
4822
(error "Unexpected state in acl2-raw-eval!"))
4823
(if (or (eq form :q) (equal form '(EXIT-LD STATE)))
4824
(mv nil '((NIL NIL STATE) NIL :Q REPLACED-STATE) state)
4825
(let ((val (eval (acl2-raw-eval-form-to-eval form)))
4826
(index-bound (raw-arity form (w state) state)))
4827
(if (<= index-bound 1)
4828
(mv nil (cons (list (stobj-out val)) val) state)
4831
(do ((i (1- index-bound) (1- i)))
4833
(let ((x (mv-ref! i)))
4838
(cons (cons (stobj-out val) stobjs-out)
4842
#+(and (not acl2-loop-only) acl2-mv-as-values)
4843
(defun acl2-raw-eval (form state)
4844
(or (eq state *the-live-state*)
4845
(error "Unexpected state in acl2-raw-eval!"))
4846
(if (or (eq form :q) (equal form '(EXIT-LD STATE)))
4847
(mv nil '((NIL NIL STATE) NIL :Q REPLACED-STATE) state)
4848
(let* ((vals (multiple-value-list
4849
(eval (acl2-raw-eval-form-to-eval form))))
4850
(arity (length vals)))
4852
(let ((val (car vals)))
4853
(mv nil (cons (list (stobj-out val)) val) state))
4855
(loop for val in vals
4856
collect (stobj-out val) into stobjs-out
4857
finally (return (cons stobjs-out vals)))
4861
(defun acl2-raw-eval (form state)
4862
(trans-eval form 'top-level state))
4864
(defun get-and-chk-last-make-event-expansion (form wrld ctx state names)
4865
(let ((expansion (f-get-global 'last-make-event-expansion state)))
4871
((inhibit-output-lst *valid-output-names*))
4872
(chk-embedded-event-form form
4874
wrld ctx state names
4877
nil ; in-encapsulatep
4878
nil ; make-event-chk
4880
(declare (ignore val))
4881
(cond (erp (er soft ctx
4882
"Make-event is only legal in event contexts, where it ~
4883
can be tracked properly; see :DOC embedded-event-form. ~
4884
The form ~p0 has thus generated an illegal call of ~
4885
make-event. This form's evaluation will have no ~
4886
effect on the ACL2 logical world."
4888
(t (value expansion)))))
4891
(defun eval-event-lst (index expansion-alist ev-lst quietp in-encapsulatep
4892
in-local-flg last-val other-control ctx channel
4343
4895
; This function takes a true list of forms, ev-lst, and successively evals each
4344
4896
; one, cascading state through successive elements. However, it insists that
4345
4897
; each form is an embedded-event-form. We return a tuple (mv erp value
4346
; expansion-alist state): erp is 'non-event if some member of ev-lst is not an
4347
; embedded event form and is t or nil otherwise; and if erp is nil, then value
4348
; is the final value (or nil if ev-lst is empty), and expansion-alist
4349
; associates the (+ index n)th member E of ev-lst with its expansion if there
4350
; is was any make-event expansion subsidiary to E, and is ordered by index from
4351
; smallest to largest (accumulated in reverse order).
4898
; expansion-alist state), where erp is 'non-event if some member of ev-lst is
4899
; not an embedded event form and otherwise is as explained below. If erp is
4900
; nil, then value is the final value (or nil if ev-lst is empty), and
4901
; expansion-alist associates the (+ index n)th member E of ev-lst with its
4902
; expansion if there was any make-event expansion subsidiary to E, ordered by
4903
; index from smallest to largest (accumulated in reverse order). If erp is not
4904
; nil, then let n be the (zero-based) index of the event in ev-lst that
4905
; translated or evaluated to some (mv erp0 ...) with non-nil erp0. Then we
4906
; return (mv t (+ index n) state) if the error was during translation, else (mv
4907
; (list erp0) (+ index n) state). Except, in the special case that there is no
4908
; error but we find that make-event was called under some non-embedded-event
4909
; form, we return (mv 'make-event-problem (+ index n) state).
4911
; Other-control is either :non-event-ok, used for progn!, or else t or nil for
4912
; the make-event-chk in chk-embedded-event-form.
4353
4914
; Channel is generally (proofs-co state), but doesn't have to be.
4355
; If orig-form is non-nil, then it will be mentioned in error reporting by
4356
; chk-embedded-event-form. This is the only use of orig-form.
4358
4916
; A non-nil value of quietp suppresses printing of the event and the result.
7765
8381
; (full-book-name ; "/usr/home/moore/project/arith.lisp"
7766
8382
; user-book-name ; "project/arith.lisp"
7767
8383
; familiar-name ; "arith"
7768
; cert-annotations ; ((:SKIPPED-PROOFSP . sp) (:AXIOMSP . axp))
8384
; cert-annotations ; ((:SKIPPED-PROOFSP . sp)
8386
; (:TTAGS . ttag-alistp))
7769
8387
; . ev-lst-chk-sum) ; 12345678
7771
; The include-book-alist becomes part of the certificate for a book,
7772
; playing a role in both the pre-alist and the post-alist. In the
7773
; latter role some elements may be marked (LOCAL &). When we refer to
7774
; parts of the include-book-alist entries we have tried to use the
7775
; tedious names above, to help us figure out what is used where.
7776
; Please try to preserve this convention.
8389
; The include-book-alist becomes part of the certificate for a book, playing a
8390
; role in both the pre-alist and the post-alist. In the latter role some
8391
; elements may be marked (LOCAL &). When we refer to parts of the
8392
; include-book-alist entries we have tried to use the tedious names above, to
8393
; help us figure out what is used where. Please try to preserve this
7778
; Cert-annotations is an alist. As of this writing (ACL2 Version_2.5)
7779
; the alist has two possible keys, :SKIPPED-PROOFSP and :AXIOMSP. The
7780
; possible values of both are t, nil, or ?, indicating the presence, absence,
7781
; or possible presence of skip-proof forms or defaxioms, respectively. The
7782
; forms in question may be either LOCAL or non-LOCAL and are in the book
7783
; itself (not just in some subbook). Even though the cert-annotations is an
7784
; alist, we compare include-book-alists with equality on that component, not
7785
; ``alist equality.'' So we are NOT free to drop or rearrange keys in these
8396
; Cert-annotations is an alist. The alist has three possible keys:
8397
; :SKIPPED-PROOFSP, :AXIOMSP, and :TTAGS. The possible values of the first two
8398
; are t, nil, or ?, indicating the presence, absence, or possible presence of
8399
; skip-proof forms or defaxioms, respectively. The forms in question may be
8400
; either LOCAL or non-LOCAL and are in the book itself (not just in some
8401
; subbook). Even though the cert-annotations is an alist, we compare
8402
; include-book-alists with equality on that component, not ``alist equality.''
8403
; So we are NOT free to drop or rearrange keys in these annotations.
7788
8405
; If the book is uncertified, the chk-sum entry is nil.
7790
; Suppose the two alist arguments are each include-book-alists from
7791
; different times. We check that the first is a subset of the second,
7792
; in the sense that the (familiar-name cert-annotations . chk-sum)
7793
; parts of the first are all among those of the second. We ignore the
7794
; full names and the user names because they may change as the book or
7795
; connected book directory moves around.
8407
; Suppose the two alist arguments are each include-book-alists from different
8408
; times. We check that the first is a subset of the second, in the sense that
8409
; the (familiar-name cert-annotations . chk-sum) parts of the first are all
8410
; among those of the second. We ignore the full names and the user names
8411
; because they may change as the book or connected book directory moves around.
7797
8413
(subsetp-equal (strip-cddrs alist1)
7798
8414
(strip-cddrs alist2)))
7800
(defun remove-after-last-directory-separator (p)
7801
(let* ((p-rev (reverse p))
7802
(posn (position *directory-separator* p-rev)))
7804
(subseq p 0 (1- (- (length p) posn)))
7805
(er hard 'remove-after-last-directory-separator
7806
"Implementation error! Unable to handle a directory string."))))
7808
(defun merge-using-dot-dot (p s)
7810
; P is a directory pathname without the final "/". S is a pathname (for a file
7811
; or a directory) that may start with any number of sequences "../" and "./".
7812
; We want to "cancel" the leading "../"s in s against directories at the end of
7813
; p, and eliminate leading "./"s from s (including leading "." if that is all
7814
; of s). The result should syntactically represent a directory (end with a "/"
7815
; or "." or be "") if and only if s syntactically represents a directory.
7817
; This code is intended to be simple, not necessarily efficient.
7822
(concatenate 'string
7823
(remove-after-last-directory-separator p)
7824
*directory-separator-string*))
7826
(concatenate 'string
7828
*directory-separator-string*))
7829
((and (>= (length s) 3)
7830
(eql (char s 0) #\.)
7831
(eql (char s 1) #\.)
7832
(eql (char s 2) #\/))
7833
(merge-using-dot-dot (remove-after-last-directory-separator p)
7834
(subseq s 3 (length s))))
7835
((and (>= (length s) 2)
7836
(eql (char s 0) #\.)
7837
(eql (char s 1) #\/))
7838
(merge-using-dot-dot p (subseq s 2 (length s))))
7840
(concatenate 'string p *directory-separator-string* s))))
7842
(defun our-merge-pathnames (p s)
7844
; This is something like the Common Lisp function merge-pathnames. P and s are
7845
; (Unix-style) pathname strings, where s is a relative pathname. (If s may be
7846
; an absolute pathname, use extend-pathname instead.) We allow p to be nil,
7847
; which is a case that arises when p is (f-get-global 'connected-book-directory
7848
; state) during boot-strapping; otherwise p should be an absolute directory
7849
; pathname (though we allow "" as well).
7852
((and (not (equal s ""))
7853
(eql (char s 0) *directory-separator*))
7854
(er hard 'our-merge-pathnames
7855
"Attempt to merge with an absolute filename, ~p0. Please contact the ~
7858
((or (null p) (equal p ""))
7860
((stringp p) ; checked because of structured pathnames before Version_2.5
7861
(merge-using-dot-dot
7862
(if (eql (char p (1- (length p)))
7863
*directory-separator*)
7864
(subseq p 0 (1- (length p)))
7868
(er hard 'our-merge-pathnames
7869
"The first argument of our-merge-pathnames must be a string, ~
7870
but the following is not: ~p0."
7873
8416
(defun get-portcullis-cmds (wrld ans wrld-segs wrld-list names ctx state)
7875
8418
; When certify-book is called, we scan down wrld to collect all the user
9523
10088
(os wrld) ctx state)))
9524
10089
(value (cons fixed-cmds pre-alist)))))))))
10091
; We next develop chk-well-formed-ttags. But first we need to develop
10092
; extend-pathname, which is called by translate-book-names, which supports
10093
; chk-well-formed-ttags.
10095
(defun remove-after-last-directory-separator (p)
10096
(let* ((p-rev (reverse p))
10097
(posn (position *directory-separator* p-rev)))
10099
(subseq p 0 (1- (- (length p) posn)))
10100
(er hard 'remove-after-last-directory-separator
10101
"Implementation error! Unable to handle a directory string."))))
10103
(defun merge-using-dot-dot (p s)
10105
; P is a directory pathname without the final "/". S is a pathname (for a file
10106
; or a directory) that may start with any number of sequences "../" and "./".
10107
; We want to "cancel" the leading "../"s in s against directories at the end of
10108
; p, and eliminate leading "./"s from s (including leading "." if that is all
10109
; of s). The result should syntactically represent a directory (end with a "/"
10110
; or "." or be "") if and only if s syntactically represents a directory.
10112
; This code is intended to be simple, not necessarily efficient.
10117
(concatenate 'string
10118
(remove-after-last-directory-separator p)
10119
*directory-separator-string*))
10121
(concatenate 'string
10123
*directory-separator-string*))
10124
((and (>= (length s) 3)
10125
(eql (char s 0) #\.)
10126
(eql (char s 1) #\.)
10127
(eql (char s 2) #\/))
10128
(merge-using-dot-dot (remove-after-last-directory-separator p)
10129
(subseq s 3 (length s))))
10130
((and (>= (length s) 2)
10131
(eql (char s 0) #\.)
10132
(eql (char s 1) #\/))
10133
(merge-using-dot-dot p (subseq s 2 (length s))))
10135
(concatenate 'string p *directory-separator-string* s))))
10137
(defun our-merge-pathnames (p s)
10139
; This is something like the Common Lisp function merge-pathnames. P and s are
10140
; (Unix-style) pathname strings, where s is a relative pathname. (If s may be
10141
; an absolute pathname, use extend-pathname instead.) We allow p to be nil,
10142
; which is a case that arises when p is (f-get-global 'connected-book-directory
10143
; state) during boot-strapping; otherwise p should be an absolute directory
10144
; pathname (though we allow "" as well).
10147
((and (not (equal s ""))
10148
(eql (char s 0) *directory-separator*))
10149
(er hard 'our-merge-pathnames
10150
"Attempt to merge with an absolute filename, ~p0. Please contact the ~
10151
ACL2 implementors."
10153
((or (null p) (equal p ""))
10155
((stringp p) ; checked because of structured pathnames before Version_2.5
10156
(merge-using-dot-dot
10157
(if (eql (char p (1- (length p)))
10158
*directory-separator*)
10159
(subseq p 0 (1- (length p)))
10163
(er hard 'our-merge-pathnames
10164
"The first argument of our-merge-pathnames must be a string, ~
10165
but the following is not: ~p0."
10168
(defun extend-pathname (dir file-name os)
10170
; Dir is a string representing an absolute directory name, and file-name is a
10171
; string representing a file or directory name. We want to extend dir by
10172
; file-name if subdir is relative, and otherwise return file-name.
10175
((absolute-pathname-string-p file-name nil os)
10178
(our-merge-pathnames dir file-name))))
10180
(defun registered-full-book-name (filename ctx state)
10182
; Returns an error triple whose value is the name of the file corresponding to
10183
; filename, a full book name, that is found in the filename's certificate file,
10184
; if such exists. Otherwise the value is nil.
10187
((inhibit-output-lst *valid-output-names*))
10188
(mv-let (erp cert-obj state)
10189
(chk-certificate-file filename t ctx state
10190
'((:uncertified-okp . t)
10192
(:skip-proofs-okp t))
10194
(value (and (null erp)
10196
(caar (access cert-obj cert-obj :post-alist)))))))
10198
(defun translate-book-names (filenames ctx cbd os state acc)
10199
(declare (xargs :guard (true-listp filenames))) ; one member can be nil
10200
(cond ((endp filenames)
10201
(value (reverse acc)))
10202
((null (car filenames))
10203
(translate-book-names (cdr filenames) ctx cbd os state
10205
(t (let ((file0 (extend-pathname cbd
10206
(possibly-add-lisp-extension
10209
(er-let* ((file1 (registered-full-book-name file0 ctx state)))
10210
(translate-book-names (cdr filenames) ctx cbd os state
10211
(cons (or file1 file0) acc)))))))
10213
(defun fix-ttags (ttags ctx cbd os state seen acc)
10215
; Seen is a list of symbols, nil at the top level. We use this argument to
10216
; enforce the lack of duplicate ttags. Acc is the accumulated list of ttags to
10217
; return, which may include symbols and lists (sym file1 ... filek).
10219
(declare (xargs :guard (true-listp ttags)))
10220
(cond ((endp ttags)
10221
(value (reverse acc)))
10222
(t (let* ((ttag (car ttags))
10223
(sym (if (consp ttag) (car ttag) ttag)))
10225
((not (and (symbolp sym)
10228
(string-listp (remove1-eq nil (cdr ttag))))))
10230
"A :ttags value for certify-book or include-book must ~
10231
either be the keyword :ALL or else a list, each of whose ~
10232
members is one of the following: a non-nil symbol, or the ~
10233
CONS of a non-nil symbol onto a true list consisting of ~
10234
strings and at most one nil. The value ~x0 is thus an ~
10235
illegal member of such a list."
10237
((member-eq sym seen)
10239
"A :ttags list may not mention the same ttag symbol more ~
10240
than once, but the proposed list mentions ~x0 more than ~
10244
(fix-ttags (cdr ttags) ctx cbd os state (cons sym seen)
10247
(er-let* ((full-book-names
10248
(translate-book-names (cdr ttag) ctx cbd os state
10250
(fix-ttags (cdr ttags) ctx cbd os state (cons sym seen)
10251
(cons (cons sym full-book-names)
10254
(defun chk-well-formed-ttags (ttags cbd ctx state)
10255
(cond ((or (null ttags) ; optimization
10258
((not (true-listp ttags))
10260
"A valid list of ttags must be a true list, unlike: ~x0."
10262
(t (fix-ttags ttags ctx cbd (os (w state)) state nil nil))))
10264
(defun cbd-fn (state)
10265
(or (f-get-global 'connected-book-directory state)
10267
"The connected book directory has apparently not yet been set. ~
10268
This could be a sign that the top-level ACL2 loop, generally ~
10269
entered using (LP), has not yet been entered.")))
10272
":Doc-Section Books
10274
connected book directory string~/
10278
\"/usr/home/smith/\"
10280
The connected book directory is a nonempty string that specifies a
10281
directory as an absolute pathname. (~l[pathname] for a
10282
discussion of file naming conventions.) When ~ilc[include-book] is given
10283
a relative book name it elaborates it into a full book name,
10284
essentially by appending the connected book directory string to the
10285
left and ~c[\".lisp\"] to the right. (For details,
10286
~pl[book-name] and also ~pl[full-book-name].) Furthermore,
10287
~ilc[include-book] temporarily sets the connected book directory to the
10288
directory string of the resulting full book name so that references
10289
to inferior ~il[books] in the same directory may omit the directory.
10290
~l[set-cbd] for how to set the connected book directory string.~/
10295
This is a macro that expands into a term involving the single free
10296
variable ~ilc[state]. It returns the connected book directory string.
10298
The connected book directory (henceforth called the ``~c[cbd]'') is
10299
used by ~ilc[include-book] to elaborate the supplied book name into a
10300
full book name (~pl[full-book-name]). For example, if the ~c[cbd]
10301
is ~c[\"/usr/home/smith/\"] then the elaboration of the ~il[book-name]
10302
~c[\"project/task-1/arith\"] (to the ~c[\".lisp\"] extension) is
10303
~c[\"/usr/home/smith/project/task-1/arith.lisp\"]. That
10304
~il[full-book-name] is what ~il[include-book] opens to read the
10305
source text for the book.
10307
The ~c[cbd] may be changed using ~ilc[set-cbd] (~pl[set-cbd]).
10308
Furthermore, during the processing of the ~il[events] in a book,
10309
~ilc[include-book] sets the ~c[cbd] to be the directory string of the
10310
~il[full-book-name] of the book. Thus, if the ~c[cbd] is
10311
~c[\"/usr/home/smith/\"] then during the processing of ~il[events] by
10313
(include-book \"project/task-1/arith\")
10315
the ~c[cbd] will be set to ~c[\"/usr/home/smith/project/task-1/\"].
10316
Note that if ~c[\"arith\"] recursively includes a subbook, say
10317
~c[\"naturals\"], that resides on the same directory, the
10318
~ilc[include-book] event for it may omit the specification of that
10319
directory. For example, ~c[\"arith\"] might contain the event
10321
(include-book \"naturals\").
10323
In general, suppose we have a superior book and several inferior
10324
~il[books] which are included by ~il[events] in the superior book. Any
10325
inferior book residing on the same directory as the superior book
10326
may be referenced in the superior without specification of the
10329
We call this a ``relative'' as opposed to ``absolute'' naming. The
10330
use of relative naming is preferred because it permits ~il[books]
10331
(and their accompanying inferiors) to be moved between directories
10332
while maintaining their ~il[certificate]s and utility. Certified
10333
~il[books] that reference inferiors by absolute file names are unusable
10334
(and rendered uncertified) if the inferiors are moved to new
10337
~em[Technical Note and a Challenge to Users:]
10339
After elaborating the book name to a full book name, ~ilc[include-book]
10340
opens a channel to the file to process the ~il[events] in it. In some
10341
host Common Lisps, the actual file opened depends upon a notion of
10342
``connected directory'' similar to our connected book directory.
10343
Our intention in always elaborating book names into absolute
10344
filename strings (~pl[pathname] for terminology) is to
10345
circumvent the sensitivity to the connected directory. But we may
10346
have insufficient control over this since the ultimate file naming
10347
conventions are determined by the host operating system rather than
10348
Common Lisp (though, we do check that the operating system
10349
``appears'' to be one that we ``know'' about). Here is a question,
10350
which we'll pose assuming that we have an operating system that
10351
calls itself ``Unix.'' Suppose we have a file name, filename, that
10352
begins with a slash, e.g., ~c[\"/usr/home/smith/...\"]. Consider two
10353
successive invocations of CLTL's
10355
(open filename :direction :input)
10357
separated only by a change to the operating system's notion of
10358
connected directory. Must these two invocations produce streams to
10359
the same file? A candidate string might be something like
10360
~c[\"/usr/home/smith/*/usr/local/src/foo.lisp\"] which includes some
10361
operating system-specific special character to mean ``here insert
10362
the connected directory'' or, more generally, ``here make the name
10363
dependent on some non-ACL2 aspect of the host's state.'' If such
10364
``tricky'' name strings beginning with a slash exist, then we have
10365
failed to isolate ACL2 adequately from the operating system's file
10366
naming conventions. Once upon a time, ACL2 did not insist that the
10367
~c[cbd] begin with a slash and that allowed the string
10368
~c[\"foo.lisp\"] to be tricky because if one were connected to
10369
~c[\"/usr/home/smith/\"] then with the empty ~c[cbd] ~c[\"foo.lisp\"]
10370
is a full book name that names the same file as
10371
~c[\"/usr/home/smith/foo.lisp\"]. If the actual file one reads is
10372
determined by the operating system's state then it is possible for
10373
ACL2 to have two distinct ``full book names'' for the same file, the
10374
``real'' name and the ``tricky'' name. This can cause ACL2 to
10375
include the same book twice, not recognizing the second one as
9526
10380
(defun chk-acceptable-certify-book (book-name full-book-name k ctx state
9527
10381
suspect-book-action-alist)
9549
10403
((f-get-global 'in-local-flg state)
9551
10405
"Certify-book may not be called inside a LOCAL command."))
9552
((global-val 'skip-proofs-seen (w state))
10406
((global-val 'skip-proofs-seen wrld)
9554
10408
"At least one command in the current ACL2 world was executed ~
9555
while the value of state global variable 'LD-SKIP-PROOFSP ~
9556
was not nil:~|~% ~x0~|~%(If you did not explicitly use ~
10409
while the value of state global variable '~x0 was not ~
10410
nil:~|~% ~y1~%(If you did not explicitly use ~
9557
10411
set-ld-skip-proofsp or call ld with :ld-skip-proofsp not ~
9558
10412
nil, then some other function did so, for example, rebuild.) ~
9559
Certification is therefore not allowed in this world. If ~
10413
Certification is therefore not allowed in this world. If ~
9560
10414
the intention was for proofs to be skipped for one or more ~
9561
10415
events in the certification world, consider wrapping those ~
9562
10416
events explicitly in skip-proofs forms. See :DOC ~
9564
(global-val 'skip-proofs-seen (w state))))
10419
(global-val 'skip-proofs-seen wrld)))
10420
((global-val 'redef-seen wrld)
10422
"At least one command in the current ACL2 world was executed ~
10423
while the value of state global variable '~x0 was not ~
10424
nil:~|~% ~y1~%Certification is therefore not allowed in ~
10425
this world. You can use :ubt to undo back through this ~
10426
command; see :DOC ubt."
10427
'ld-redefinition-action
10428
(global-val 'redef-seen wrld)))
10431
; We disallow active ttag at certification time because we don't want to think
10432
; about certain oddly redundant defttag events. Consider for example executing
10433
; (defttag foo), and then certifying a book containing the following forms,
10434
; (certify-book "foo" 1 nil :ttags ((foo nil))), indicating that ttag foo is
10435
; only active at the top level, not inside a book.
10440
; (declare (xargs :mode :program))
10441
; (sys-call "ls" nil))
10443
; The defttag expands to a redundant table event, hence would be allowed.
10444
; Perhaps this is OK, but it is rather scary since we then have a case of a
10445
; book containing a defttag of which there is no evidence of this in any "TTAG
10446
; NOTE" string or in the book's certificate. While we see no real problem
10447
; here, since the defttag really is ignored, still it's very easy for the user
10448
; to work around this situation by executing (defttag nil) before
10449
; certification; so we take this conservative approach.
10452
"It is illegal to certify a book while there is an active ~
10453
ttag, in this case, ~x0. Consider undoing the corresponding ~
10454
defttag event (see :DOC ubt) or else executing ~x1. See ~
9565
10458
(t (value nil)))
9566
10459
(chk-book-name book-name full-book-name ctx state)
9568
10461
((certp (certificate-filep full-book-name state)))
9569
(let ((wrld (w state)))
9571
(erp cmds wrld-segs wrld-list state)
9572
(get-portcullis-cmds wrld nil nil nil names ctx state)
10463
(erp cmds wrld-segs wrld-list state)
10464
(get-portcullis-cmds wrld nil nil nil names ctx state)
10466
(erp (silent-error state))
9574
(erp (silent-error state))
9579
"When you tell certify-book to recover the certification ~
9580
world from the old certificate, you must call certify-book ~
9581
in the initial ACL2 logical world -- so we don't have to ~
9582
worry about the certification world clashing with the ~
9583
existing logical world. But you are not in the initial ~
9584
logical world. Use :pbt 1 to see the world."))
9587
"There is no certificate on file for ~x0. But you told ~
9588
certify-book to recover the certi~-fication world from the ~
9589
old certificate. You will have to construct the ~
9590
certi~-fication world by hand (by executing the desired ~
9591
commands in the current logical world) and then call ~
9592
certify-book again."
10471
"When you tell certify-book to recover the certification world ~
10472
from the old certificate, you must call certify-book in the ~
10473
initial ACL2 logical world -- so we don't have to worry about ~
10474
the certification world clashing with the existing logical ~
10475
world. But you are not in the initial logical world. Use ~
10476
:pbt 1 to see the world."))
10479
"There is no certificate on file for ~x0. But you told ~
10480
certify-book to recover the certi~-fication world from the ~
10481
old certificate. You will have to construct the ~
10482
certi~-fication world by hand (by executing the desired ~
10483
commands in the current logical world) and then call ~
10484
certify-book again."
9596
10488
; So k is t, we are in the initial world, and there is a certificate file
9597
10489
; from which we can recover the portcullis. Do it.
9601
(chk-certificate-file full-book-name t ctx state
9602
(cons '(:uncertified-okp . nil)
9603
suspect-book-action-alist)
9605
(cert-obj-cmds (value (and cert-obj
9606
(access cert-obj cert-obj :cmds)))))
9607
(chk-acceptable-certify-book1 full-book-name
9608
(length cert-obj-cmds) ;; k
9609
cert-obj-cmds ;; cmds
9610
:omitted ;; wrld-segs
9615
(t (chk-acceptable-certify-book1 full-book-name k cmds wrld-segs
9616
wrld-list names wrld ctx
10493
(chk-certificate-file full-book-name t ctx state
10494
(cons '(:uncertified-okp . nil)
10495
suspect-book-action-alist)
10497
(cert-obj-cmds (value (and cert-obj
10498
(access cert-obj cert-obj :cmds)))))
10499
(chk-acceptable-certify-book1 full-book-name
10500
(length cert-obj-cmds) ;; k
10501
cert-obj-cmds ;; cmds
10502
:omitted ;; wrld-segs
10507
(t (chk-acceptable-certify-book1 full-book-name k cmds wrld-segs
10508
wrld-list names wrld ctx
9619
10511
(defun print-objects (lst ch state)
9620
10512
(cond ((null lst) state)
9858
10749
(value (cons (list 'in-package new-current-package)
9861
(defun cbd-fn (state)
9862
(or (f-get-global 'connected-book-directory state)
9864
"The connected book directory has apparently not yet been set. ~
9865
This could be a sign that the top-level ACL2 loop, generally ~
9866
entered using (LP), has not yet been entered.")))
9871
connected book directory string~/
9875
\"/usr/home/smith/\"
9877
The connected book directory is a nonempty string that specifies a
9878
directory as an absolute pathname. (~l[pathname] for a
9879
discussion of file naming conventions.) When ~ilc[include-book] is given
9880
a relative book name it elaborates it into a full book name,
9881
essentially by appending the connected book directory string to the
9882
left and ~c[\".lisp\"] to the right. (For details,
9883
~pl[book-name] and also ~pl[full-book-name].) Furthermore,
9884
~ilc[include-book] temporarily sets the connected book directory to the
9885
directory string of the resulting full book name so that references
9886
to inferior ~il[books] in the same directory may omit the directory.
9887
~l[set-cbd] for how to set the connected book directory string.~/
9892
This is a macro that expands into a term involving the single free
9893
variable ~ilc[state]. It returns the connected book directory string.
9895
The connected book directory (henceforth called the ``~c[cbd]'') is
9896
used by ~ilc[include-book] to elaborate the supplied book name into a
9897
full book name (~pl[full-book-name]). For example, if the ~c[cbd]
9898
is ~c[\"/usr/home/smith/\"] then the elaboration of the ~il[book-name]
9899
~c[\"project/task-1/arith\"] (to the ~c[\".lisp\"] extension) is
9900
~c[\"/usr/home/smith/project/task-1/arith.lisp\"]. That
9901
~il[full-book-name] is what ~il[include-book] opens to read the
9902
source text for the book.
9904
The ~c[cbd] may be changed using ~ilc[set-cbd] (~pl[set-cbd]).
9905
Furthermore, during the processing of the ~il[events] in a book,
9906
~ilc[include-book] sets the ~c[cbd] to be the directory string of the
9907
~il[full-book-name] of the book. Thus, if the ~c[cbd] is
9908
~c[\"/usr/home/smith/\"] then during the processing of ~il[events] by
9910
(include-book \"project/task-1/arith\")
9912
the ~c[cbd] will be set to ~c[\"/usr/home/smith/project/task-1/\"].
9913
Note that if ~c[\"arith\"] recursively includes a subbook, say
9914
~c[\"naturals\"], that resides on the same directory, the
9915
~ilc[include-book] event for it may omit the specification of that
9916
directory. For example, ~c[\"arith\"] might contain the event
9918
(include-book \"naturals\").
9920
In general, suppose we have a superior book and several inferior
9921
~il[books] which are included by ~il[events] in the superior book. Any
9922
inferior book residing on the same directory as the superior book
9923
may be referenced in the superior without specification of the
9926
We call this a ``relative'' as opposed to ``absolute'' naming. The
9927
use of relative naming is preferred because it permits ~il[books]
9928
(and their accompanying inferiors) to be moved between directories
9929
while maintaining their ~il[certificate]s and utility. Certified
9930
~il[books] that reference inferiors by absolute file names are unusable
9931
(and rendered uncertified) if the inferiors are moved to new
9934
~em[Technical Note and a Challenge to Users:]
9936
After elaborating the book name to a full book name, ~ilc[include-book]
9937
opens a channel to the file to process the ~il[events] in it. In some
9938
host Common Lisps, the actual file opened depends upon a notion of
9939
``connected directory'' similar to our connected book directory.
9940
Our intention in always elaborating book names into absolute
9941
filename strings (~pl[pathname] for terminology) is to
9942
circumvent the sensitivity to the connected directory. But we may
9943
have insufficient control over this since the ultimate file naming
9944
conventions are determined by the host operating system rather than
9945
Common Lisp (though, we do check that the operating system
9946
``appears'' to be one that we ``know'' about). Here is a question,
9947
which we'll pose assuming that we have an operating system that
9948
calls itself ``Unix.'' Suppose we have a file name, filename, that
9949
begins with a slash, e.g., ~c[\"/usr/home/smith/...\"]. Consider two
9950
successive invocations of CLTL's
9952
(open filename :direction :input)
9954
separated only by a change to the operating system's notion of
9955
connected directory. Must these two invocations produce streams to
9956
the same file? A candidate string might be something like
9957
~c[\"/usr/home/smith/*/usr/local/src/foo.lisp\"] which includes some
9958
operating system-specific special character to mean ``here insert
9959
the connected directory'' or, more generally, ``here make the name
9960
dependent on some non-ACL2 aspect of the host's state.'' If such
9961
``tricky'' name strings beginning with a slash exist, then we have
9962
failed to isolate ACL2 adequately from the operating system's file
9963
naming conventions. Once upon a time, ACL2 did not insist that the
9964
~c[cbd] begin with a slash and that allowed the string
9965
~c[\"foo.lisp\"] to be tricky because if one were connected to
9966
~c[\"/usr/home/smith/\"] then with the empty ~c[cbd] ~c[\"foo.lisp\"]
9967
is a full book name that names the same file as
9968
~c[\"/usr/home/smith/foo.lisp\"]. If the actual file one reads is
9969
determined by the operating system's state then it is possible for
9970
ACL2 to have two distinct ``full book names'' for the same file, the
9971
``real'' name and the ``tricky'' name. This can cause ACL2 to
9972
include the same book twice, not recognizing the second one as
9977
10752
(defun maybe-add-separator (str)
9978
10753
(if (and (not (equal str ""))
9979
10754
(eql (char str (1- (length str))) *directory-separator*))
10367
11133
(cond (dir (include-book-dir-with-chk soft ctx dir))
10368
11134
(t (value (cbd))))))
10370
(full-book-name directory-name familiar-name)
10371
(parse-book-name dir-value user-book-name ".lisp" (os (w state)))
11136
(full-book-name directory-name familiar-name)
11137
(parse-book-name dir-value user-book-name ".lisp" (os (w state)))
10373
11139
; If you add more keywords to the suspect-book-action-alist, make sure you do
10374
11140
; the same to the list constructed by certify-book-fn. You might wish to
10375
11141
; handle the new warning summary in warning1.
10377
(let ((suspect-book-action-alist
10378
(list (cons :uncertified-okp
10379
(if (assoc-eq 'certify-book
10380
(global-val 'embedded-event-lst
10384
(cons :defaxioms-okp defaxioms-okp)
10385
(cons :skip-proofs-okp skip-proofs-okp))))
10387
(chk-book-name user-book-name full-book-name ctx state)
10388
(chk-input-object-file full-book-name ctx state)
10389
(revert-world-on-error
10391
((and (not (global-val 'boot-strap-flg wrld0))
10393
(assoc-equal full-book-name
10394
(global-val 'include-book-alist wrld0)))
10395
(stop-redundant-event state))
10397
(let ((wrld1 (global-set
10399
(cons full-book-name old-include-book-path)
10402
(set-w 'extension wrld1 state)
10404
((redef (chk-new-stringp-name 'include-book full-book-name
10406
(doc-pair (translate-doc full-book-name doc ctx state))
10407
(cert-obj (if behalf-of-certify-flg
10409
(chk-certificate-file full-book-name nil ctx state
10410
suspect-book-action-alist
10412
(wrld-after-certificate (value (w state)))
10413
(expansion-alist (value (if behalf-of-certify-flg
10416
(access cert-obj cert-obj
10417
:expansion-alist)))))
10418
(post-alist (value (and cert-obj
10419
(access cert-obj cert-obj
10421
(cert-full-book-name (value (car (car post-alist)))))
11143
(let ((suspect-book-action-alist
11144
(list (cons :uncertified-okp
11145
(if (assoc-eq 'certify-book
11146
(global-val 'embedded-event-lst
11150
(cons :defaxioms-okp defaxioms-okp)
11151
(cons :skip-proofs-okp skip-proofs-okp)))
11152
(include-book-alist0 (global-val 'include-book-alist wrld0)))
11154
(chk-book-name user-book-name full-book-name ctx state)
11155
(chk-input-object-file full-book-name ctx state)
11156
(revert-world-on-error
11158
((and (not (global-val 'boot-strap-flg wrld0))
11160
(assoc-equal full-book-name include-book-alist0))
11161
(stop-redundant-event state))
11163
(let ((wrld1 (global-set
11165
(cons full-book-name old-include-book-path)
11168
(set-w 'extension wrld1 state)
11170
((redef (chk-new-stringp-name 'include-book full-book-name
11172
(doc-pair (translate-doc full-book-name doc ctx state))
11173
(cert-obj (if behalf-of-certify-flg
11175
(chk-certificate-file full-book-name nil ctx state
11176
suspect-book-action-alist
11178
(wrld2 (value (w state)))
11179
(expansion-alist (value (if behalf-of-certify-flg
11182
(access cert-obj cert-obj
11183
:expansion-alist)))))
11184
(post-alist (value (and cert-obj
11185
(access cert-obj cert-obj
11187
(cert-full-book-name (value (car (car post-alist)))))
10424
11190
; We try the redundancy check again, because it will be cert-full-book-name
10425
11191
; that is stored on the world's include-book-alist, not full-book-name (if the
10426
11192
; two book names differ).
10428
((and (not (equal full-book-name cert-full-book-name))
10429
(not (global-val 'boot-strap-flg wrld1))
10430
cert-full-book-name
10431
(assoc-equal cert-full-book-name
10432
(global-val 'include-book-alist wrld1)))
11194
((and (not (equal full-book-name cert-full-book-name))
11195
(not (global-val 'boot-strap-flg wrld2))
11196
cert-full-book-name
11197
(assoc-equal cert-full-book-name
11198
include-book-alist0))
10434
11200
; Chk-certificate-file calls chk-certificate-file1, which calls
10435
11201
; chk-raise-portcullis, which calls chk-raise-portcullis1, which evaluates, for
10436
11202
; example, maybe-install-acl2-defaults-table. So we need to revert the world
10439
(pprogn (set-w 'retraction wrld0 state)
10440
(stop-redundant-event state)))
10443
((ev-lst (read-object-file full-book-name ctx state)))
11205
(pprogn (set-w 'retraction wrld0 state)
11206
(stop-redundant-event state)))
11209
((ev-lst (read-object-file full-book-name ctx state)))
10445
11211
; Cert-obj above is either nil, indicating that the file is uncertified, or is
10446
11212
; a cert-obj record, which contains the now raised portcullis and the check sum
10452
11218
; resides now. However, the familiar-name, cert-annotations and the
10453
11219
; ev-lst-chk-sum ought to be those for the current book.
10456
(ev-lst-chk-sum state)
10457
(check-sum-obj (append expansion-alist ev-lst) state)
10459
((not (integerp ev-lst-chk-sum))
11222
(ev-lst-chk-sum state)
11223
(check-sum-obj (append expansion-alist ev-lst) state)
11225
((not (integerp ev-lst-chk-sum))
10461
11227
; This error should never arise because check-sum-obj is only called on
10462
11228
; something produced by read-object, which checks that the object is ACL2
10463
11229
; compatible, and perhaps make-event expansion. The next form causes a soft
10464
11230
; error, assigning proper blame.
10467
(raw-ev-lst-chk-sum state)
10468
(check-sum-obj ev-lst state)
10469
(cond ((not (integerp raw-ev-lst-chk-sum))
10471
"The file ~x0 is not a legal list of ~
10472
embedded event forms because it ~
10473
contains an object, ~x1, which check ~
10474
sum was unable to handle."
10475
full-book-name raw-ev-lst-chk-sum))
10478
(expansion-chk-sum state)
10479
(check-sum-obj expansion-alist state)
10481
((not (integerp expansion-chk-sum))
10483
"The expansion-alist (from ~
10484
make-event) for file ~x0 is not a ~
10485
legal list of embedded event forms ~
10486
because it contains an object, ~x1, ~
10487
which check sum was unable to handle."
10488
full-book-name expansion-chk-sum))
10490
"The append of expansion-alist ~
10491
(from make-event) and command for ~
10492
file ~x0 is not a legal list of ~
10493
embedded event forms because it ~
10494
contains an object, ~x1, which ~
10495
check sum was unable to handle. ~
10496
This is very surprising,because ~
10497
check sums were computed ~
10498
successfully for the ~
10499
expansion-alist and the commands. ~
10500
It would be helpful for you to ~
10501
send a replayable example of this ~
10502
behavior to the ACL2 implementors."
10503
full-book-name ev-lst-chk-sum))))))))
11233
(raw-ev-lst-chk-sum state)
11234
(check-sum-obj ev-lst state)
11235
(cond ((not (integerp raw-ev-lst-chk-sum))
11237
"The file ~x0 is not a legal list of ~
11238
embedded event forms because it contains ~
11239
an object, ~x1, which check sum was ~
11241
full-book-name raw-ev-lst-chk-sum))
11244
(expansion-chk-sum state)
11245
(check-sum-obj expansion-alist state)
11247
((not (integerp expansion-chk-sum))
11249
"The expansion-alist (from make-event) ~
11250
for file ~x0 is not a legal list of ~
11251
embedded event forms because it ~
11252
contains an object, ~x1, which check ~
11253
sum was unable to handle."
11254
full-book-name expansion-chk-sum))
11256
"The append of expansion-alist (from ~
11257
make-event) and command for file ~x0 ~
11258
is not a legal list of embedded ~
11259
event forms because it contains an ~
11260
object, ~x1, which check sum was ~
11261
unable to handle. This is very ~
11262
surprising,because check sums were ~
11263
computed successfully for the ~
11264
expansion-alist and the commands. ~
11265
It would be helpful for you to send ~
11266
a replayable example of this ~
11267
behavior to the ACL2 implementors."
11268
full-book-name ev-lst-chk-sum))))))))
10506
11271
; Notice that we are reaching inside the certificate object to retrieve
10507
11272
; information about the book from the post-alist. (Car post-alist)) is in fact
10509
11274
; . ev-lst-chk-sum).
10514
(not (equal (caddr (car post-alist))
10519
"The cer~-ti~-fi~-cate on file for ~x0 lists ~
10520
the book under the name ~x3 whereas we were ~
10521
expecting it to give the name ~x4. While we ~
10522
allow a certified book to be moved from one ~
10523
directory to another after ~
10524
cer~-ti~-fi~-ca~-tion, we insist that it keep ~
10525
the same familiar name. This allows the ~
10526
cer~-ti~-fi~-cate file to contain the ~
10527
familiar name, making it easier to identify ~
10528
which cer~-ti~-fi~-cates go with which files ~
10529
and inspiring a little more confidence that ~
10530
the cer~-ti~-fi~-cate really does describe ~
10531
the alleged file. In the present case, it ~
10532
looks as though the familiar book name was ~
10533
changed after cer~-ti~-fi~-ca~-tion. For ~
10534
what it is worth, the check sum of the file ~
10535
at cer~-ti~-fi~-ca~-tion was ~x5. Its check ~
10537
(list (cons #\3 (caddr (car post-alist)))
10538
(cons #\4 familiar-name)
10539
(cons #\5 (cddddr (car post-alist)))
10540
(cons #\6 ev-lst-chk-sum)))
10542
suspect-book-action-alist
10548
(not (equal (cddddr (car post-alist))
10553
"The certificate on file for ~x0 lists the ~
10554
check sum of the certified book as ~x3. But ~
10555
the check sum of the events now in the file ~
10556
is ~x4. This generally indicates that the ~
10557
file has been modified since it was last ~
10559
(list (cons #\3 (cddddr (car post-alist)))
10560
(cons #\4 ev-lst-chk-sum)))
10562
suspect-book-action-alist
10566
(let ((cert-annotations (cadddr (car post-alist))))
10568
; It is possible for cert-annotations to be nil now. That is because cert-obj was
10569
; nil. But we never use it if cert-obj is nil.
10573
(or (cdr (assoc :skipped-proofsp
10575
(cdr (assoc :axiomsp
10576
cert-annotations))))
10578
(chk-cert-annotations cert-annotations
10579
(access cert-obj cert-obj
10582
suspect-book-action-alist
11279
(not (equal (caddr (car post-alist))
11284
"The cer~-ti~-fi~-cate on file for ~x0 lists ~
11285
the book under the name ~x3 whereas we were ~
11286
expecting it to give the name ~x4. While we ~
11287
allow a certified book to be moved from one ~
11288
directory to another after ~
11289
cer~-ti~-fi~-ca~-tion, we insist that it keep ~
11290
the same familiar name. This allows the ~
11291
cer~-ti~-fi~-cate file to contain the familiar ~
11292
name, making it easier to identify which ~
11293
cer~-ti~-fi~-cates go with which files and ~
11294
inspiring a little more confidence that the ~
11295
cer~-ti~-fi~-cate really does describe the ~
11296
alleged file. In the present case, it looks ~
11297
as though the familiar book name was changed ~
11298
after cer~-ti~-fi~-ca~-tion. For what it is ~
11299
worth, the check sum of the file at ~
11300
cer~-ti~-fi~-ca~-tion was ~x5. Its check sum ~
11302
(list (cons #\3 (caddr (car post-alist)))
11303
(cons #\4 familiar-name)
11304
(cons #\5 (cddddr (car post-alist)))
11305
(cons #\6 ev-lst-chk-sum)))
11307
suspect-book-action-alist
11313
(not (equal (cddddr (car post-alist))
11318
"The certificate on file for ~x0 lists the ~
11319
check sum of the certified book as ~x3. But ~
11320
the check sum of the events now in the file is ~
11321
~x4. This generally indicates that the file ~
11322
has been modified since it was last certified."
11323
(list (cons #\3 (cddddr (car post-alist)))
11324
(cons #\4 ev-lst-chk-sum)))
11326
suspect-book-action-alist
11330
(let* ((cert-annotations
11331
(cadddr (car post-alist)))
11333
(cdr (assoc-eq :ttags cert-annotations))))
11335
; It is possible for cert-annotations to be nil now. That is because cert-obj
11336
; was nil. But we never use it if cert-obj is nil, except for cert-ttags.
11337
; Now, cert-obj is nil when we are including an uncertified book; so the fact
11338
; that the calls of chk-ttags-for-include-book and chk-acceptable-ttags are
11339
; trivial, in this case, is not a problem.
11342
((ttags (chk-well-formed-ttags
11343
ttags directory-name ctx state))
11353
cert-annotations))))
11354
(chk-cert-annotations
11356
(access cert-obj cert-obj :cmds)
11358
suspect-book-action-alist
11362
; The following two calls of chk-acceptable-ttags1 can presumably be skipped if
11363
; state global 'skip-notify-on-defttag has a non-nil value. However, they are
11364
; probably cheap so we go ahead and make them anyhow, for robustness.
11365
; 'Skip-notify-on-defttag will prevent needless subsidiary notification
11368
(chk-acceptable-ttags1
11370
nil ; active-book-name is irrelevant
11372
nil ; ttags-seen is irrelevant
11374
(chk-acceptable-ttags1
11375
cert-ttags active-book-name0
11376
(f-get-global 'ttags-allowed state)
11377
old-ttags-seen t ctx state))))
10586
11379
; The following process-embedded-events is protected by the revert-world-
10587
11380
; on-error above. See the Essay on Guard Checking for a discussion of the
10588
11381
; binding of guard-checking-on below.
10591
((skipped-proofsp nil)
10593
(connected-book-directory directory-name)
10594
(match-free-error nil)
10595
(guard-checking-on nil)
11386
((skipped-proofsp nil)
11388
(ttags-allowed (car ttags-info))
11389
(skip-notify-on-defttag cert-obj)
11390
(connected-book-directory directory-name)
11391
(match-free-error nil)
11392
(guard-checking-on nil)
10598
11395
; As we start processing the events in the book, we are no longer in the
10599
11396
; lexical scope of LOCAL for purposes of disallowing setting of the
10600
11397
; acl2-defaults-table.
10602
(and (f-get-global 'in-local-flg state)
10604
(let ((skip-proofsp
11399
(and (f-get-global 'in-local-flg state)
11401
(let ((skip-proofsp
10606
11403
; At one time we bound this variable to 'initialize-acl2 if (or cert-obj
10607
11404
; behalf-of-certify-flg) is false. But cert-obj is non-nil even if the
10619
11416
; treated by include-book much like certified books, in order to assist his
10620
11417
; development process. That seems reasonable.
10623
(process-embedded-events
10626
saved-acl2-defaults-table
10628
(cadr (car ev-lst))
10629
(list 'include-book full-book-name)
10630
(subst-by-position expansion-alist
10634
(eq skip-proofsp 'include-book)
10637
; This function returns what might be called proto-wrld3, which is
10638
; equivalent to the current world of state before the
10639
; process-embedded-events (since the insigs argument is nil), but it has
10640
; an incremented embedded-event-depth. We don't care about this
10641
; world. The interesting world is the one current in the state
10642
; returned by by process-embedded-events. It has all the embedded
10643
; events in it and we are done except for certification issues.
10645
(let* ((wrld2 (w state))
10646
(actual-alist (global-val 'include-book-alist
10651
(not (include-book-alist-subsetp
10652
(unmark-and-delete-local-included-books
10657
(cons "The certified book ~x0 requires ~*3 but ~
10661
(tilde-*-book-check-sums-phrase
10663
(unmark-and-delete-local-included-books
10667
(tilde-*-book-check-sums-phrase
10669
(unmark-and-delete-local-included-books
10673
suspect-book-action-alist
11421
(process-embedded-events
11424
; We do not allow process-embedded-events-to set the ACL2 defaults table at the
11425
; end. For, consider the case that (defttag foo) has been executed just before
11426
; the (include-book "bar") being processed. At the start of this
11427
; process-embedded-events we clear the acl2-defaults-table, removing any :ttag.
11428
; If we try to restore the acl2-defaults-table at the end of this
11429
; process-embedded-events, we will fail because the include-book-path was
11430
; extended above to include full-book-name (for "bar"), and the restoration
11431
; installs a :ttag of foo, yet in our example there is no :ttags argument for
11432
; (include-book "bar"). So, instead we directly set the 'table-alist property
11433
; of 'acl2-defaults-table directory for the install-event call below.
11437
(cadr (car ev-lst))
11438
(list 'include-book full-book-name)
11439
(subst-by-position expansion-alist
11443
(eq skip-proofsp 'include-book)
11445
(value (f-get-global 'ttags-allowed
11448
; The above process-embedded-events call returns what might be called
11449
; proto-wrld3, which is equivalent to the current world of state before the
11450
; process-embedded-events (since the insigs argument is nil), but it has an
11451
; incremented embedded-event-depth. We don't care about this world. The
11452
; interesting world is the one current in the state returned by by
11453
; process-embedded-events. It has all the embedded events in it and we are
11454
; done except for certification issues.
11456
(let* ((wrld3 (w state))
11457
(actual-alist (global-val 'include-book-alist
11462
(not (include-book-alist-subsetp
11463
(unmark-and-delete-local-included-books
11468
(cons "The certified book ~x0 requires ~
11469
~*3 but we have ~*4."
11472
(tilde-*-book-check-sums-phrase
11474
(unmark-and-delete-local-included-books
11478
(tilde-*-book-check-sums-phrase
11480
(unmark-and-delete-local-included-books
11484
suspect-book-action-alist
10677
11488
; Now we check that all the subbooks of this one are also compatible with the
10678
11489
; current settings of suspect-book-action-alist. The car of post-alist is the
11356
12199
((ev-lst (read-object-file full-book-name ctx state)))
11358
(ev-lst-chk-sum state) ; later we'll include
11359
(check-sum-obj ev-lst state)
11361
((not (integerp ev-lst-chk-sum))
11363
"The file ~x0 is not a legal list of embedded event ~
12201
(ev-lst-chk-sum state) ; later we'll include
12202
(check-sum-obj ev-lst state)
12204
((not (integerp ev-lst-chk-sum))
12206
"The file ~x0 is not a legal list of embedded event ~
11364
12207
forms because it contains an object, ~x1, which check ~
11365
12208
sum was unable to handle."
11366
full-book-name ev-lst-chk-sum))
11368
(io? event nil state
11370
(fms "* Step 2: There ~#0~[were no forms in the ~
11371
file. Why are you making such a silly ~
11372
book?~/was one form in the file.~/were ~n1 ~
11373
forms in the file.~] We now attempt to ~
11374
establish that each form, whether local or ~
11375
non-local, is indeed an admissible embedded ~
11376
event form in the context of the previously ~
11377
admitted ones. Note that proof-tree output ~
11378
is inhibited during this check; see :DOC ~
11380
(list (cons #\0 (zero-one-or-more ev-lst))
11381
(cons #\1 (length ev-lst)))
11382
(proofs-co state) state nil))
12209
full-book-name ev-lst-chk-sum))
12212
(io? event nil state
12214
(fms "* Step 2: There ~#0~[were no forms in the ~
12215
file. Why are you making such a silly ~
12216
book?~/was one form in the file.~/were ~n1 ~
12217
forms in the file.~] We now attempt to ~
12218
establish that each form, whether local or ~
12219
non-local, is indeed an admissible embedded ~
12220
event form in the context of the previously ~
12221
admitted ones. Note that proof-tree output is ~
12222
inhibited during this check; see :DOC ~
12224
(list (cons #\0 (zero-one-or-more ev-lst))
12225
(cons #\1 (length ev-lst)))
12226
(proofs-co state) state nil))
12230
((ttags-allowed (car pair0))
11388
12232
; We ``accumulate'' into the flag skipped-proofsp whether there are any
11389
12233
; skip-proofs in sight. See the Essay on Skip-proofs.
11391
(skipped-proofsp nil)
11392
(include-book-alist-state nil)
12235
(skipped-proofsp nil)
12236
(include-book-alist-state nil)
11394
12238
; We will accumulate into the flag axiomsp whether any axioms have been added,
11395
12239
; starting with those in the portcullis. We can identify axioms in the
11396
12240
; portcullis by asking if the current nonconstructive axioms are different from
11397
12241
; those at the end of boot-strap.
11401
(global-val ;;; axioms as of boot-strap
11402
'nonconstructive-axiom-names
11403
(scan-to-landmark-number
11405
(global-val 'event-number-baseline
11408
(global-val ;;; axioms now.
11409
'nonconstructive-axiom-names
11412
(ld-redefinition-action nil)
11413
(connected-book-directory directory-name))
11414
(revert-world-on-error
11416
(note-certification-world-lst
12245
(global-val ;;; axioms as of boot-strap
12246
'nonconstructive-axiom-names
12247
(scan-to-landmark-number
12249
(global-val 'event-number-baseline
12252
(global-val ;;; axioms now.
12253
'nonconstructive-axiom-names
12255
(ld-redefinition-action nil)
12256
(connected-book-directory directory-name))
12257
(revert-world-on-error
12259
(note-certification-world-lst
11422
12265
; This list of names must be the same as in chk-acceptable-certify-book.
11425
*primitive-event-macros*)
11426
suspect-book-action-alist)
12268
*primitive-event-macros*)
12269
suspect-book-action-alist)
11428
12271
; The fact that we are under 'certify-book means that all calls of
11429
12272
; include-book will insist that the :uncertified-okp action is nil, meaning
11430
12273
; errors will be caused if uncertified books are read.
11434
(process-embedded-events
11437
saved-acl2-defaults-table
11438
nil (cadr (car ev-lst))
11439
(list 'certify-book full-book-name)
11441
1 nil 'certify-book state)))
11442
(value (list (f-get-global 'skipped-proofsp state)
11443
(f-get-global 'axiomsp state)
11445
'include-book-alist-state
11447
expansion-alist))))))))
11448
(let* ((pass1-known-package-alist
11449
(global-val 'known-package-alist (w state)))
11450
(skipped-proofsp (car pass1-result))
11451
(axiomsp (cadr pass1-result))
11452
(new-include-book-alist-state
11453
(caddr pass1-result))
11454
(expansion-alist (cadddr pass1-result))
12277
(process-embedded-events
12279
saved-acl2-defaults-table
12280
nil (cadr (car ev-lst))
12281
(list 'certify-book full-book-name)
12283
1 nil 'certify-book state)))
12284
(value (list (f-get-global 'skipped-proofsp state)
12285
(f-get-global 'axiomsp state)
12286
(global-val 'ttags-seen (w state))
12288
'include-book-alist-state
12290
expansion-alist))))))))
12291
(let* ((pass1-known-package-alist
12292
(global-val 'known-package-alist (w state)))
12293
(skipped-proofsp (car pass1-result))
12294
(axiomsp (cadr pass1-result))
12295
(ttags-seen (caddr pass1-result))
12296
(new-include-book-alist-state
12297
(cadddr pass1-result))
12298
(expansion-alist (cadddr (cdr pass1-result)))
11458
12302
; We set :skipped-proofsp in the certification annotations to t or nil
11459
12303
; according to whether there were any skipped proofs in either the
11460
12304
; portcullis or the body of this book.
11462
(cons :skipped-proofsp
12306
(cons :skipped-proofsp skipped-proofsp)
11465
12308
; We similarly set :axiomsp to t or nil. Note that axioms in subbooks
11466
12309
; are not counted as axioms in this one.
12311
(cons :axiomsp axiomsp)
12312
(cons :ttags ttags-seen))))
12319
(check-sum-obj (append expansion-alist
12323
(t (value ev-lst-chk-sum))))
12325
(value (cons (list* full-book-name
12330
new-include-book-alist-state))))
12332
(chk-cert-annotations cert-annotations
12335
suspect-book-action-alist
12338
(io? event nil state
12340
(fms "* Step 3: That completes the ~
12341
admissibility check. Each form read was ~
12342
an embedded event form and was ~
12343
admissible. We now retract back to the ~
12344
initial world and try to include the ~
12345
book. This may expose local ~
12346
incompatibilities.~%"
12348
(proofs-co state) state nil))
12349
(set-w 'retraction wrld1 state)
11476
(check-sum-obj (append expansion-alist
11480
(t (value ev-lst-chk-sum))))
11482
(value (cons (list* full-book-name
11487
new-include-book-alist-state))))
11489
(chk-cert-annotations cert-annotations
11492
suspect-book-action-alist
11495
(io? event nil state
11497
(fms "* Step 3: That completes the ~
11498
admissibility check. Each form read ~
11499
was an embedded event form and was ~
11500
admissible. We now retract back to the ~
11501
initial world and try to include the ~
11502
book. This may expose local ~
11503
incompatibilities.~%"
11505
(proofs-co state) state nil))
11506
(set-w 'retraction wrld1 state)
11510
pass1-known-package-alist
11514
((ld-redefinition-action nil))
12353
pass1-known-package-alist
12357
((ld-redefinition-action nil))
11516
12359
; Note that we do not bind connected-book-directory before calling
11517
12360
; include-book-fn, because it will bind it for us. We leave the directory set
11518
12361
; as it was when we parsed user-book-name to get full-book-name, so that
11519
12362
; include-book-fn will parse user-book-name the same way again.
11521
(include-book-fn user-book-name state nil
11524
defaxioms-okp skip-proofs-okp
11526
(let* ((wrld2 (w state))
11530
(global-val 'known-package-alist wrld2)))
11531
(new-fns (and (or (not (warning-disabled-p
11533
(eq compile-flg :all))
12364
(include-book-fn user-book-name state nil
12367
defaxioms-okp skip-proofs-okp
12370
(let* ((wrld2 (w state))
12374
(global-val 'known-package-alist wrld2)))
12375
(new-fns (and (or (not (warning-disabled-p
12377
(eq compile-flg :all))
11535
12379
; The test above is an optimization; we don't need new-fns if it's false.
11537
(newly-defined-top-level-fns
11539
(new-fns-exec (and (eq compile-flg :all)
11541
(expansion-filename ; nil for "do not write it"
11542
(and (or (eq save-expansion :save)
11545
(expansion-filename full-book-name)))
11547
(cons (list* full-book-name
12381
(newly-defined-top-level-fns
12383
(new-fns-exec (and (eq compile-flg :all)
12385
(expansion-filename ; nil for "do not write it"
12386
(and (or (eq save-expansion :save)
12389
(expansion-filename full-book-name)))
12391
(cons (list* full-book-name
11551
12395
; We use the cert-annotations from the first pass. They are the ones that
11552
12396
; include the LOCAL events too.
11556
(cdr (global-val 'include-book-alist
12400
(cdr (global-val 'include-book-alist
11559
12403
; The cdr above removes the certification tuple stored by the
11560
12404
; include-book-fn itself. That pair is guaranteed to be last one
11567
12411
; we've included (and hence recognize as redundant) until after we've
11568
12412
; completed the processing.
12416
(new-bad-fns all-bad-fns)
12417
(cond ((not (warning-disabled-p "Guards"))
12418
(mv (collect-ideals new-fns wrld2 nil)
12419
(collect-ideal-user-defuns wrld2)))
12422
((or new-bad-fns all-bad-fns)
12423
(let* ((new-bad-fns
12430
(set-difference-eq-sorted
12436
"~#1~[~/The book ~x0 defines the ~
12437
function~#2~[ ~&2, which has not had ~
12438
its~/s ~&2, which have not had their~] ~
12439
guards verified. ~]~#3~[~/~#1~[For the ~
12440
book ~x0, its~/Moreover, this book's~] ~
12441
included sub-books ~#4~[~/and/or its ~
12442
certification world ~]define ~
12443
function~#5~[ ~&5, which has not had ~
12444
its~/s ~&5, which have not had their~] ~
12445
guards verified. ~]See :DOC guards."
12447
(if new-bad-fns 1 0)
12449
(if extra-bad-fns 1 0)
12454
((not (include-book-alist-subsetp post-alist2
12456
(let ((files (spontaneous-decertificationp
12462
"During Step 3, we loaded the ~
12463
uncertified ~#0~[book ~&0. This book ~
12464
was certified when we looked at ~
12465
it~/books ~&0. These books were ~
12466
certified when we looked at them~] in ~
12467
Step 2! The most likely explanation ~
12468
is that some concurrent job, possibly ~
12469
by another user of your file system, ~
12470
is currently recertifying ~#0~[this ~
12471
book~/these books~] (or subbooks of ~
12472
~#0~[it~/them~]). That hypothetical ~
12473
job might have deleted the ~
12474
certificate files of the books in ~
12475
question, rendering ~#0~[this ~
12476
one~/these~] uncertified. If this ~
12477
explanation seems likely, we ~
12478
recommend that you identify the other ~
12479
job and wait until it has ~
12480
successfully completed."
12484
"During Step 3, we loaded different ~
12485
books than were loaded by Step 2! ~
12486
Here are the tuples produced by Step ~
12487
3 of the form ~X04 whose CDDRs are ~
12488
not in the list of tuples produced by ~
12489
Step 2:~|~%~X14~|~%Perhaps some other ~
12490
user of your file system was editing ~
12491
the books during our Step 3? You ~
12492
might think that some other job is ~
12493
recertifying the books (or subbooks) ~
12494
and has deleted the certificate ~
12495
files, rendering uncertified some of ~
12496
the books needed here. But more has ~
12497
happened! Some file has changed (as ~
12498
indicated above)!~%~%DETAILS. Here ~
12499
is the include-book-alist as of the ~
12500
end of Step 2:~%~X24.~|~%And here is ~
12501
the alist as of the end of Step ~
12502
3:~%~X34.~|~%Frequently, the former ~
12503
has more entries than the latter ~
12504
because the former includes LOCAL ~
12505
books. So compare corresponding ~
12506
entries, focusing on those in the ~
12507
latter. Each entry is of the form ~
12508
(name1 name2 name3 alist . chk-sum). ~
12509
Name1 is the full name, name2 is the ~
12510
name as written in an include-book ~
12511
event, and name3 is the ``familiar'' ~
12512
name of the file. The alist indicates ~
12513
the presence or absence of ~
12514
problematic forms in the file, such ~
12515
as DEFAXIOM events. For example, ~
12516
(:AXIOMSP . T) means there were ~
12517
defaxiom events; (:AXIOMSP . NIL) -- ~
12518
which actually prints as (:AXIOMSP) ~
12519
-- means there were no defaxiom ~
12520
events. Finally, chk-sum is either an ~
12521
integer check sum based on the ~
12522
contents of the file at the time it ~
12523
was certified or else chk-sum is nil ~
12524
indicating that the file is not ~
12525
certified. Note that if the chk-sum ~
12526
is nil, the entry prints as (name1 ~
12527
name2 name3 alist). Go figure."
12532
. :chk-sum-for-events)
12533
(include-book-alist-subsetp-failure-witnesses
12535
(strip-cddrs post-alist1)
11572
(new-bad-fns all-bad-fns)
11573
(cond ((not (warning-disabled-p "Guards"))
11574
(mv (collect-ideals new-fns wrld2 nil)
11575
(collect-ideal-user-defuns wrld2)))
11577
(cond ((or new-bad-fns all-bad-fns)
11578
(let* ((new-bad-fns
11585
(set-difference-eq-sorted
11591
"~#1~[~/The book ~x0 defines the ~
11592
function~#2~[ ~&2, which has not ~
11593
had its~/s ~&2, which have not ~
11594
had their~] guards verified. ~
11595
~]~#3~[~/~#1~[For the book ~x0, ~
11596
its~/Moreover, this book's~] ~
11597
included sub-books ~#4~[~/and/or ~
11598
its certification world ~]define ~
11599
function~#5~[ ~&5, which has not ~
11600
had its~/s ~&5, which have not ~
11601
had their~] guards verified. ~
11602
~]See :DOC guards."
11604
(if new-bad-fns 1 0)
11606
(if extra-bad-fns 1 0)
11611
((not (include-book-alist-subsetp post-alist2
11613
(let ((files (spontaneous-decertificationp
11619
"During Step 3, we loaded the ~
11620
uncertified ~#0~[book ~&0. This ~
11621
book was certified when we looked ~
11622
at it~/books ~&0. These books were ~
11623
certified when we looked at them~] ~
11624
in Step 2! The most likely ~
11625
explanation is that some ~
11626
concurrent job, possibly by ~
11627
another user of your file system, ~
11628
is currently recertifying ~
11629
~#0~[this book~/these books~] (or ~
11630
subbooks of ~#0~[it~/them~]). ~
11631
That hypothetical job might have ~
11632
deleted the certificate files of ~
11633
the books in question, rendering ~
11634
~#0~[this one~/these~] ~
11635
uncertified. If this explanation ~
11636
seems likely, we recommend that ~
11637
you identify the other job and ~
11638
wait until it has successfully ~
11643
"During Step 3, we loaded different ~
11644
books than were loaded by Step 2! ~
11645
Here are the tuples produced by ~
11646
Step 3 of the form ~X04 whose ~
11647
CDDRs are not in the list of ~
11648
tuples produced by Step ~
11649
2:~|~%~X14~|~%Perhaps some other ~
11650
user of your file system was ~
11651
editing the books during our Step ~
11652
3? You might think that some other ~
11653
job is recertifying the books (or ~
11654
subbooks) and has deleted the ~
11655
certificate files, rendering ~
11656
uncertified some of the books ~
11657
needed here. But more has ~
11658
happened! Some file has changed ~
11659
(as indicated above)!~%~%DETAILS. ~
11660
Here is the include-book-alist as ~
11661
of the end of Step ~
11662
2:~%~X24.~|~%And here is the alist ~
11663
as of the end of Step ~
11664
3:~%~X34.~|~%Frequently, the ~
11665
former has more entries than the ~
11666
latter because the former includes ~
11667
LOCAL books. So compare ~
11668
corresponding entries, focusing on ~
11669
those in the latter. Each entry ~
11670
is of the form (name1 name2 name3 ~
11671
alist . chk-sum). Name1 is the ~
11672
full name, name2 is the name as ~
11673
written in an include-book event, ~
11674
and name3 is the ``familiar'' name ~
11675
of the file. The alist indicates ~
11676
the presence or absence of ~
11677
problematic forms in the file, ~
11678
such as DEFAXIOM events. For ~
11679
example, (:AXIOMSP . T) means ~
11680
there were defaxiom events; ~
11681
(:AXIOMSP . NIL) -- which actually ~
11682
prints as (:AXIOMSP) -- means ~
11683
there were no defaxiom events. ~
11684
Finally, chk-sum is either an ~
11685
integer check sum based on the ~
11686
contents of the file at the time ~
11687
it was certified or else chk-sum ~
11688
is nil indicating that the file is ~
11689
not certified. Note that if the ~
11690
chk-sum is nil, the entry prints ~
11691
as (name1 name2 name3 alist). Go ~
11697
. :chk-sum-for-events)
11698
(include-book-alist-subsetp-failure-witnesses
11700
(strip-cddrs post-alist1)
12542
(io? event nil state
12543
(post-alist1 full-book-name
12544
expansion-filename)
12545
(fms "* Step 4: Write the certificate ~
12546
for ~x0 in ~x1~@2. The final ~
12547
check sum alist is ~x3.~%"
12549
(cons #\0 full-book-name)
12552
(convert-book-name-to-cert-name
12556
(if expansion-filename
12557
(msg ", as well as the ~
12558
expansion file, ~@0"
12559
expansion-filename)
12561
(cons #\3 post-alist1))
12562
(proofs-co state) state nil))
12564
(if expansion-filename
12565
(write-expansion-file
12566
new-fns-exec expansion-filename
12567
expansion-alist ev-lst ctx state)
12569
(make-certificate-file
12572
(remove-duplicates-equal-from-end
12573
(append (car portcullis) new-defpkg-list)
11706
12585
(io? event nil state
11707
(post-alist1 full-book-name
11708
expansion-filename)
11709
(fms "* Step 4: Write the ~
11710
certificate for ~x0 in ~x1~@2. ~
11711
The final check sum alist is ~
11714
(cons #\0 full-book-name)
11717
(convert-book-name-to-cert-name
11721
(if expansion-filename
11722
(msg ", as well as the ~
11723
expansion file, ~@0"
11724
expansion-filename)
11726
(cons #\3 post-alist1))
12587
(fms "* Step 5: Compile the ~
12588
functions defined in ~x0.~%"
12589
(list (cons #\0 full-book-name))
11727
12590
(proofs-co state) state nil))
11729
(if expansion-filename
11730
(write-expansion-file
11731
new-fns-exec expansion-filename
11732
expansion-alist ev-lst ctx state)
11734
(make-certificate-file
11737
(remove-duplicates-equal-from-end
11738
(append (car portcullis) new-defpkg-list)
12592
(compile-certified-file
12595
full-book-name expansion-alist
12602
(delete-compiled-file
12603
(pathname-unix-to-os full-book-name
11750
(io? event nil state
11752
(fms "* Step 5: Compile the ~
11753
functions defined in ~
11755
(list (cons #\0 full-book-name))
11756
(proofs-co state) state nil))
11758
(compile-certified-file
11761
full-book-name expansion-alist
11768
(delete-compiled-file
11769
(pathname-unix-to-os full-book-name
11775
(when (and expansion-filename
11776
(not save-expansion))
11777
(delete-file expansion-filename)
11778
(io? event nil state
11779
(expansion-filename)
11780
(fms "Note: Deleting book ~
11781
expansion file,~%~s0.~|"
11785
expansion-filename))
11786
(proofs-co state) state
11790
full-book-name)))))))))))))))))))))))))))))
12609
(when (and expansion-filename
12610
(not save-expansion))
12611
(delete-file expansion-filename)
12612
(io? event nil state
12613
(expansion-filename)
12614
(fms "Note: Deleting book ~
12615
expansion file,~%~s0.~|"
12619
expansion-filename))
12620
(proofs-co state) state
12624
full-book-name))))))))))))))))))))))))))))))
11792
12626
#+acl2-loop-only
11793
12627
(defmacro certify-book (&whole event-form
14062
(defun defchoose-constraint-extra (fn bound-vars formals tbody ctx wrld state)
14064
; WARNING: If the following comment is removed, then eliminate the reference to
14065
; it in :doc defchoose.
14067
; Note that :doc conservativity-of-defchoose contains an argument showing that
14068
; we may assume that there is a definable enumeration, enum, of the universe.
14069
; Thus, for any definable property that is not always false, there is a "least"
14070
; witness, i.e., a least n for which (enum n) satisfies that property. Thus, a
14071
; function defined with defchoose is definable: pick the least witness if there
14072
; is one, else nil. From this definition it is clear that the following
14073
; formula holds, where formals2 is a copy of formals that is disjoint both from
14074
; formals and from bound-vars, and where tbody2 is the result of replacing
14075
; formals by formals2 in tbody, the translated body of the defchoose. (If
14076
; bound-vars is a list of length 1, then we use let rather than mv-let in this
14079
; (or (equal (fn . formals)
14081
; (mv-let (bound-vars (fn . formals))
14084
; (mv-let (bound-vars (fn . formals2))
14088
; We now outline an argument for the :non-standard-analysis case, which in fact
14089
; provides justification for both defchoose axioms. The idea is to assume that
14090
; there is a suitable well-ordering for the ground-zero theory and that the
14091
; ground-zero theory contains enough "invisible" functions so that this
14092
; property is preserved by extensions (as discussed in the JAR paper "Theory
14093
; Extensions in ACL2(r) by Gamboa and Cowles). Here is a little more detail,
14094
; but a nice challenge is to work this out completely.
14096
; The idea of the proof is first to start with what the above paper calls an
14097
; "r-complete" GZ: basically, a ground-zero theory satisfying induction and
14098
; transfer that contains a function symbol for each defun and defun-std. We
14099
; can preserve r-completeness as we add defun, defun-std, encapsulate, and
14100
; defchoose events (again, as in the above paper). The key idea for defchoose
14101
; is that GZ should also have a binary symbol, <|, that is axiomatized to be a
14102
; total order. That is, <| is a "definable well order", in the sense that
14103
; there are axioms that guarantee for each phi(x) that (exists x phi) implies
14104
; that (exists <|-least x phi). The trick is to add the well-ordering after
14105
; taking a nonstandard elementary extension of the standard reals MS, where
14106
; every function over the reals is represented in MS as the interpretation of a
14109
; Still as in the above paper, there is a definable fn for the above defchoose,
14110
; obtained by picking the least witness. Moreover, if body is classical then
14111
; we can first conjoin it with (standard-p bound-var), choose the <|-least
14112
; bound-var with a classical function using defun-std, and then show by
14113
; transfer that this function witnesses the original defchoose.
14115
(let* ((formals2 (generate-variable-lst formals (append bound-vars formals)
14116
nil (ens state) wrld))
14117
(equality (fcons-term* 'equal (cons fn formals) (cons fn formals2)))
14118
(tbody2 (subcor-var formals formals2 tbody))
14121
; It seems a pity to translate tbody, since it's already translated, but that
14122
; seems much simpler than the alternatives.
14125
((null (cdr bound-vars))
14126
`(or (let ((,(car bound-vars) (,fn ,@formals)))
14129
(let ((,(car bound-vars) (,fn ,@formals2)))
14133
`(or (mv-let ,bound-vars
14137
(mv-let ,bound-vars
14140
(not ,tbody))))))))
14141
(er-let* ((disjunct
14142
(translate raw-disjunct t t t ctx wrld state)))
14143
(value (disjoin2 equality disjunct)))))
14145
(defun defchoose-constraint (fn bound-vars formals tbody strengthen ctx wrld state)
14146
(er-let* ((basic (defchoose-constraint-basic fn bound-vars formals tbody ctx
14150
(er-let* ((extra (defchoose-constraint-extra fn bound-vars formals
14151
tbody ctx wrld state)))
14152
(value (conjoin2 basic extra))))
14153
(t (value basic)))))
13228
14155
(defun defchoose-fn (def state event-form)
14156
(declare (xargs :guard (true-listp def))) ; def comes from macro call
13231
14159
(with-ctx-summarized
13232
14160
(if (output-in-infixp state) event-form (cons 'defchoose (car def)))
13233
14161
(let* ((wrld (w state))
13234
14162
(event-form (or event-form (cons 'defchoose def)))
13235
(len (length def)))
14163
(raw-bound-vars (cadr def))
14164
(valid-keywords '(:doc :strengthen))
14165
(ka (nthcdr 4 def)) ; def is the argument list of a defchoose call
14166
(doc (cadr (assoc-keyword :doc ka)))
14167
(strengthen (cadr (assoc-keyword :strengthen def))))
13237
14169
(chk-all-but-new-name (car def) ctx 'constrained-function wrld state)
13239
((not (and (true-listp def)
13240
(member len '(4 5))))
14171
((not (and (keyword-value-listp ka)
14172
(null (strip-keyword-list valid-keywords ka))))
13242
14174
"Defchoose forms must have the form (defchoose fn bound-vars ~
13243
formals body), optionally with a doc-string before the body. ~
13244
However, ~x0 does not have this form."
13247
(not (doc-stringp (nth 3 def))))
13249
"When a DEFCHOOSE form has five arguments, the fourth must be a ~
13250
doc string. The form ~x0 is thus illegal. See :DOC doc-string."
13252
((redundant-defchoosep (car def) event-form len wrld)
14175
formals body), with optional keyword arguments ~&0. However, ~
14176
~x1 does not have this form. See :DOC defchoose."
14180
(not (doc-stringp doc)))
14182
"Illegal doc string has been supplied in ~x0. See :DOC ~
14185
((not (booleanp strengthen))
14187
"The :strengthen argument of a defchoose event must be t or nil. ~
14188
The event ~x0 is thus illegal."
14190
((redundant-defchoosep (car def) event-form wrld)
13253
14191
(stop-redundant-event state))
13255
14193
(enforce-redundancy
13256
14194
event-form ctx wrld
14196
((null raw-bound-vars)
13260
"The bound variables of a DEFCHOOSE form must be non-empty. ~
14198
"The bound variables of a defchoose form must be non-empty. ~
13261
14199
The form ~x0 is therefore illegal."
13264
14202
(let ((fn (car def))
13265
(bound-vars (if (atom (cadr def))
14203
(bound-vars (if (atom raw-bound-vars)
14204
(list raw-bound-vars)
13268
14206
(formals (caddr def))
13269
(doc (and (= len 5) (cadddr def)))
13270
(body (if (= len 5) (cadddr (cdr def)) (cadddr def))))
14207
(body (cadddr def)))
13272
14209
(chk-arglist-for-defchoose bound-vars t ctx state)
13273
14210
(chk-arglist-for-defchoose formals nil ctx state)
added
removed
other-events.lisp
