Skip to content

Commit

Permalink
Improved #., both its error message and by clearing input. Fixed erro…
Browse files Browse the repository at this point in the history 
…r message for :definition rule with empty clique. Fixed handling of xdoc <stv> tags in text-based display. Fixed error message for bad argument of set-iprint. Improved :doc irrelevant-formals.

Quoting :doc note-7-3:

  We improved ACL2's implementation of the #. read macro so that it no
  longer prints additional errors after the first. Also, the error
  message now mentions :DOC [sharp-dot-reader], pointing in
  particular to a relevant remark when the failure occurs during book
  certification.

  For a proposed [definition] rule with a missing (or empty) :CLIQUE
  but a non-empty :CONTROLLER-ALIST, the error message was
  ill-formed. This has been fixed.

Also quoting :doc note-7-3, where this is a new item under the item,
"The text-based display of [documentation] has been improved...."

    * Text within ``<stv> ... </stv>'' is now replaced by the text ``{STV
      display}''. A general mechanism is in place for extending this
      behavior to other tags (see xdoc-tag-elide-alist in
      [community-books] file 'books/xdoc/display.lisp').

Fixed an error message in the case that the first argument of
set-iprint was not one of the supported values.  (This bug was
introduced after Version 7.2.)

Improved :doc irrelevant-formals.  (This is independent of the
possible change of "irrelevant" to "irrelevant-ok" in declare forms,
perhaps coming soon.)
  • Loading branch information
Matt Kaufmann authored and Matt Kaufmann committed Sep 26, 2016
1 parent 6ed1e29 commit 03477ed
Show file tree
Hide file tree
Showing 7 changed files with 287 additions and 167 deletions.
14 changes: 11 additions & 3 deletions acl2-fns.lisp
View file
Expand Up @@ -1274,14 +1274,22 @@ notation causes an error and (b) the use of ,. is not permitted."
(consp (cdr val))
(null (cddr val)))
(cadr val))
(t (error "(Implementation error) Found non-quotep 'const ~%~
(t (clear-input stream)
(error "(Implementation error) Found non-quotep 'const ~%~
property for ~s."
sym))))
(sym
(clear-input stream)
(error "ACL2 supports #. syntax only for #.*a*, where *a* has been ~%~
defined by ~s. Thus the form #.~s is illegal."
'defconst sym))
defined by ~s. Thus the form #.~s is illegal. See :DOC ~%~
sharp-dot-reader~a."
'defconst
sym
(cond ((eval '(f-get-global 'certify-book-info *the-live-state*))
(format nil ", in particular Remark (2)"))
(t ""))))
(t ; surprising case
(clear-input stream)
(error "ACL2 supports #. syntax only for #.*a*, where *a* has been ~%~
defined by ~s."
'defconst)))))
Expand Down
81 changes: 60 additions & 21 deletions books/system/doc/acl2-doc.lisp
View file
Expand Up @@ -43087,8 +43087,8 @@ tables in the current Hons Space."
and the value of @('(fn a1...ai...an)') is independent of @('ai').</p>

<p>The easiest way to define a function with an irrelevant formal is simply
not to use the formal in the body of the function. Such formals are said to
be ``ignored'' by Common Lisp and a special declaration is provided to allow
not to use the formal anywhere in its definition. Such formals are said to be
``ignored'' by Common Lisp and a special declaration is provided to allow
ignored formals. ACL2 makes a distinction between ignored and irrelevant
formals. Note however that if a variable is @(tsee declare)d @('ignore')d or
@('ignorable'), then it will not be reported as irrelevant.</p>
Expand All @@ -43104,22 +43104,34 @@ tables in the current Hons Space."

<p>Observe that @('x') is only used in recursive calls of @('fact'); it never
``gets out'' into the result. ACL2 can detect some irrelevant formals by a
closure analysis on how the formals are used. For example, if the @('i')th
formal is only used in the @('i')th argument position of recursive calls, then
it is irrelevant. This is how @('x') is used above.</p>
closure analysis on how the formals are used; let us call these the ``clearly
irrelevant formals.'' For example, if the @('i')th formal is only used in the
@('i')th argument position of recursive calls, then it is clearly irrelevant.
This is how @('x') is used above.</p>

<p>It is possible for a formal to appear only in recursive calls but not be
clearly irrelevant, or even irrelevant at all. For example, @('x') is
<b>not</b> irrelevant below, even though it only appears in the recursive
call.</p>

@({
(defun fn (i x y)
(if (zp i) y (fn (1- i) y x)))
})

<p>It is possible for a formal to appear only in recursive calls but still be
relevant. For example, @('x') is <b>not</b> irrelevant below, even though it
only appears in the recursive call.</p>
<p>The following examples show the relevance of @('x').</p>

@({
(defun fn (i x) (if (zp i) 0 (fn x (1- i))))
ACL2 !>(fn 1 3 0)
3
ACL2 !>(fn 1 4 0)
4
ACL2 !>
})

<p>The key observation above is that while @('x') only appears in a recursive
call, it appears in an argument position, namely @('i')'s, that is relevant.
(The function above can be admitted with a @(':measure') of @('(+ (nfix i)
(nfix x))').)</p>
<p>The key observation for the definition of @('fn') is that while @('x') only
appears in a recursive call, it appears in the argument position for a formal
that is not clearly irrelevant, namely @('y')'s.</p>

<p>Establishing that a formal is irrelevant, in the sense defined above, can
be an arbitrarily hard problem because it requires theorem proving. For
Expand All @@ -43131,8 +43143,8 @@ tables in the current Hons Space."

<p>Note that the value of @('(test i j k x)') is independent of @('x') &mdash;
thus making @('x') irrelevant &mdash; precisely if @('(p i j k)') is a
theorem. ACL2's syntactic analysis of a definition does not guarantee to
notice all irrelevant formals.</p>
theorem. ACL2's syntactic analysis of a definition to determine the ``clearly
irrelevant'' formals does not guarantee to notice all irrelevant formals.</p>

<p>We regard the presence of irrelevant formals as an indication that
something is wrong with the definition. By default, ACL2 causes an error on
Expand All @@ -43154,9 +43166,10 @@ tables in the current Hons Space."
<p>To turn off the checking of irrelevant formals globally (though we do not
recommend avoiding those checks), see @(see set-irrelevant-formals-ok). In
that case ACL2 will ignore every @('irrelevant') declaration. But otherwise,
and by default, if you provide an @('irrelevant') declaration, then it must
specify exactly the irrelevant formals: any extra formal that is not
irrelevant will cause an error.</p>")
and by default, if you provide an @('irrelevant') declaration (see @(see
declare)), then it must specify exactly the formals that ACL2 determines to be
irrelevant, what we call the ``clearly irrelevant'' formals above: any formal
declared irrelevant that is not clearly irrelevant will cause an error.</p>")

(defxdoc keep
:parents (books-tour)
Expand Down Expand Up @@ -74607,6 +74620,10 @@ it."
cause the wrong constraints to be generated in the case of more than one
function argument.</p>

<p>For a proposed @(see definition) rule with a missing (or empty)
@(':CLIQUE') but a non-empty @(':CONTROLLER-ALIST'), the error message was
ill-formed. This has been fixed.</p>

<h3>Changes at the System Level</h3>

<p>It was possible for a backtrace to be printed to the terminal by SBCL and
Expand Down Expand Up @@ -74666,6 +74683,11 @@ it."
@('books/centaur/vl2014/server/server.lisp'). Thanks to Jared Davis for a tip
that helped us to debug that issue (ACL2 GitHub Issue #634).</p>

<p>We improved ACL2's implementation of the @('#.') read macro so that it no
longer prints additional errors after the first. Also, the error message now
mentions :DOC @(see sharp-dot-reader), pointing in particular to a relevant
remark when the failure occurs during book certification.</p>

<h3>EMACS Support</h3>

<p>The text-based display of @(see documentation) has been improved, that is,
Expand All @@ -74689,6 +74711,11 @@ it."
<li>Certain ``raw'' topics, such as DEFXDOC-RAW, are now included that
formerly were only included in the web-based manual.</li>

<li>Text within ``@('<stv> ... </stv>')'' is now replaced by the text
``@('{STV display}')''. A general mechanism is in place for extending this
behavior to other tags (see @('xdoc-tag-elide-alist') in @(see
community-books) file 'books/xdoc/display.lisp').</li>

</ul>

<h3>Experimental Versions</h3>
Expand Down Expand Up @@ -92054,7 +92081,10 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")
(set-irrelevant-formals-ok flg)
})

<p>where @('flg') is either @('t'), @('nil'), or @(':warn').</p>")
<p>where @('flg') is either @('t'), @('nil'), or @(':warn').</p>

<p>For a way to permit irrelevant formals in a specific definition, see @(see
declare).</p>")

(defxdoc set-let*-abstractionp
:parents (prover-output)
Expand Down Expand Up @@ -93064,7 +93094,9 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")

(defxdoc set-serialize-character-system
:parents (serialize)
:short "<p>This function can be used to turn off (or on) the @(see
:short "Avoid some special @(see serialize) writing, including for @('.cert')
files"
:long "<p>This function can be used to turn off (or on) the @(see
serialize-write) capability, which is on by default, for writing certain files
during book certification, including @(see certificate) files. To use this
function during a session:</p>
Expand All @@ -93084,7 +93116,10 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")
cd books ; \\
make basic \\
ACL2_CUSTOMIZATION=`pwd`/../acl2-customization-files/no-serialize.lisp
})")
})

<p>To control the use of @(see serialize) for writes controlled by the user
rather than by the system, see @(see with-serialize-character).</p>")

(defxdoc set-skip-meta-termp-checks
:parents (meta clause-processor)
Expand Down Expand Up @@ -110904,6 +110939,10 @@ for the execution of @('form')."
routines, contributed by Jared Davis for saving ACL2 objects in files for
later loading.</p>

<p>NOTE: To control the use of the serialize writer by the system, rather than
by the user (as discussed below), see @(see
set-serialize-character-system).</p>

<p>The expression @('(with-serialize-character char form)') evaluates to the
value of @('form'), but with the serialize-character of the @(tsee state)
assigned to @('char'), which should be one of @('nil'), @('#\\Y'), or
Expand Down
6 changes: 4 additions & 2 deletions books/system/doc/render-doc-base.lisp
View file
Expand Up @@ -204,8 +204,10 @@
(mv (er hard 'render-topic
"Unexpected implementation error!")
state))
(merged-tokens (reverse (merge-text tokens nil 0 nil
topic-to-rendered-table)))
(merged-tokens
(reverse (merge-text tokens nil 0 nil
topic-to-rendered-table
(f-get-global 'xdoc-tag-elide-alist state))))
(acc (tokens-to-terminal merged-tokens 70 nil nil nil))
(terminal (str::trim (str::rchars-to-string acc))))

Expand Down
88 changes: 67 additions & 21 deletions books/xdoc/display.lisp
View file
Expand Up @@ -166,7 +166,27 @@
(car match)
"]")))))

(defun merge-text (x acc codes href topic-to-rendered-table)
; This variable can be modified here or by the user. It is an alist so that
; for every tag TAG for which <TAG>...</TAG> is to be replaced by text TEXT,
; the alist contains the entry (TAG . TEXT).
(make-event (pprogn (f-put-global 'xdoc-tag-elide-alist
'(("stv" . "{STV display}"))
state)
(value '(value-triple t)))
:check-expansion t)

(defun skip-to-close (tag x)
(cond ((atom x)
x)
(t (b* ((tok1 (car x))
(name (and (closetok-p tok1)
(closetok-name tok1))))
(cond ((equal name tag)
(cdr x))
(t (skip-to-close tag (cdr x))))))))

(defun merge-text (x acc codes href topic-to-rendered-table
xdoc-tag-elide-alist)
;; CODES is number of open <code> tags -- we don't normalize whitespace
;; within them, but entities still get converted.
(b* (((when (atom x))
Expand All @@ -181,18 +201,22 @@
(cond ((equal name "img")
(b* ((tok (list :TEXT "{IMAGE}")))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
((equal name "icon")
(b* ((tok (list :TEXT "{ICON}")))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
((member-equal name *throwaway-tags*)
(merge-text rest acc codes nil topic-to-rendered-table))
(merge-text rest acc codes nil topic-to-rendered-table
xdoc-tag-elide-alist))
((equal name "a")
(b* ((href (cdr (assoc-equal "href" (opentok-atts tok1))))
(tok (list :TEXT (str::cat "{"))))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
((equal name "see")
(b* ((href (or
; It's probably rare or impossible to have a <see> within an <a href...>, but
Expand All @@ -204,21 +228,32 @@
(opentok-atts tok1)))))
(tok (list :TEXT "[")))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
((equal name "srclink")
(b* ((tok (list :TEXT "<")))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
(t
(merge-text rest (cons tok1 acc) codes href
topic-to-rendered-table)))))
(let ((pair (assoc-equal name xdoc-tag-elide-alist)))
(cond
(pair (b* ((tok (list :TEXT (cdr pair))))
(merge-text (cons tok (skip-to-close name x))
acc codes href
topic-to-rendered-table
xdoc-tag-elide-alist)))
(t (merge-text rest (cons tok1 acc) codes href
topic-to-rendered-table
xdoc-tag-elide-alist))))))))
((when (closetok-p tok1))
(b* ((name (closetok-name tok1))
(codes (if (equal name "code")
(- 1 codes)
codes)))
(cond ((member-equal name *throwaway-tags*)
(merge-text rest acc codes href topic-to-rendered-table))
(merge-text rest acc codes href topic-to-rendered-table
xdoc-tag-elide-alist))
((member-equal name '("see"))
(b* ((text (texttok-text (car acc)))
(bracket-posn (search "[" text :from-end t))
Expand All @@ -234,24 +269,29 @@
((eq match t)
(let ((tok (list :TEXT "]")))
(merge-text (cons tok rest) acc codes nil
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
(t (merge-text
rest
(cons (list :text
(fix-close-see text bracket-posn match))
(cdr acc))
codes nil topic-to-rendered-table)))))
codes nil topic-to-rendered-table
xdoc-tag-elide-alist)))))
((member-equal name '("a"))
(let ((tok (list :TEXT (str::cat " | " (or href "") "}"))))
(merge-text (cons tok rest) acc codes nil
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
((equal name "srclink")
(let ((tok (list :TEXT ">")))
(merge-text (cons tok rest) acc codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))
(t
(merge-text rest (cons tok1 acc) codes href
topic-to-rendered-table)))))
topic-to-rendered-table
xdoc-tag-elide-alist)))))
(tok1
;; Goofy. Convert any entities into ordinary text. Normalize
;; whitespace for any non-code tokens.
Expand All @@ -264,12 +304,14 @@
;; Inside a <code> block, so don't touch ws.
tok1)))
((unless (texttok-p (car acc)))
(merge-text rest (cons tok1 acc) codes href topic-to-rendered-table))
(merge-text rest (cons tok1 acc) codes href topic-to-rendered-table
xdoc-tag-elide-alist))

(merged-tok (list :TEXT (str::cat (texttok-text (car acc))
(texttok-text tok1)))))
(merge-text rest (cons merged-tok (cdr acc)) codes href
topic-to-rendered-table)))
topic-to-rendered-table
xdoc-tag-elide-alist)))

(defun has-tag-above (tag open-tags)
(if (atom open-tags)
Expand Down Expand Up @@ -597,8 +639,10 @@
((when err)
(mv (str::cat "Error displaying xdoc topic: " *nls* *nls* err *nls* *nls*)
state))
(merged-tokens (reverse (merge-text tokens nil 0 nil
topic-to-rendered-table)))
(merged-tokens
(reverse (merge-text tokens nil 0 nil
topic-to-rendered-table
(f-get-global 'xdoc-tag-elide-alist state))))
; (- (cw "Merged tokens are ~x0.~%" merged-tokens))
(terminal (str::rchars-to-string
(tokens-to-terminal merged-tokens 70 nil nil nil)))
Expand Down Expand Up @@ -695,8 +739,10 @@
(state (newline *standard-co* state))
(state (newline *standard-co* state)))
state))
(merged-tokens (reverse (merge-text tokens nil 0 nil
topic-to-rendered-table)))
(merged-tokens
(reverse (merge-text tokens nil 0 nil
topic-to-rendered-table
(f-get-global 'xdoc-tag-elide-alist state))))
; (- (cw "Merged tokens are ~x0.~%" merged-tokens))
(terminal (str::rchars-to-string (tokens-to-terminal merged-tokens 70 nil nil nil)))
(state (princ$ " " *standard-co* state))
Expand Down
5 changes: 3 additions & 2 deletions defthm.lisp
View file
Expand Up @@ -8345,9 +8345,10 @@
that maps each function symbol in the :CLIQUE to a list of ~
t's and nil's whose length is equal to the arity of the ~
function symbol. ~x0 is an inappropriate controller alist ~
for the :CLIQUE consisting of ~&1. See :DOC definition."
for the ~@1. See :DOC definition."
controller-alist
clique)))))))
(cond ((null clique) "empty clique")
(t (msg ":CLIQUE consisting of ~&0" clique))))))))))
((eq token :INDUCTION)
(cond ((not (assoc-eq :PATTERN seen))
(er soft ctx
Expand Down

0 comments on commit 03477ed

Please sign in to comment.