Here are a few potential ACL2 development tasks, separated by lines of
"<><>".  To see the one-line summaries:

grep '^{{.*}}[ ]*$' to-do.txt | sed 's/^{{//' | sed 's/}}[ ]*$//' > to-do-summary.txt

**WARNINGS**:

(1) This is for a small group of incipient ACL2 developers who have
undergone suitable training (see
http://www.cs.utexas.edu/users/moore/acl2/workshop-devel-2017/).  We
hope you will contribute!

(2) Matt and J need to approve any changes that go into any part of
the ACL2 system except for what is under books/.  So, you might want
to ask them to commit to looking at your changes before you spend time
working on them.

(3) The descriptions below are probably OK but not necessarily
polished.  Please discuss with your developer colleagues if you have
questions.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Improve error message for linear rule that is illegal because of evaluation.}}

Eric Smith's email just below raises that issue; some analysis is
below that.

..........

[acl2-devel] improving error message about :linear rules
Eric Smith <eric.smith@kestrel.edu>	Wed, May 20, 2020 at 1:07 AM
Reply-To: acl2-devel@utlists.utexas.edu
To: acl2-devel@utlists.utexas.edu

Here is a weird little example of something I ran into:

(defun two () 2)

;fails somewhat mysteriously
(defthm two-bound
  (< 1 (two))
  :rule-classes :linear)

(in-theory (disable (:e two)))

;same as before but succeeds!
(defthm two-bound
  (< 1 (two))
  :rule-classes :linear)

I presume that the first defthm fails because ACL2 evaluates the call of
TWO and perhaps also the < (:doc linear does mention evaluation of
ground subexpressions).  But the error message is just:

ACL2 Error in ( DEFTHM TWO-BOUND ...):  No :LINEAR rule can be generated
from TWO-BOUND.  See :DOC linear.

Perhaps it could be improved to show a bit more information, e.g., that
it is trying to make a linear rule from the constant T.

Thanks,
-Eric

..........

[acl2-devel] improving error message about :linear rules
Matt Kaufmann <kaufmann@cs.utexas.edu>	Wed, May 20, 2020 at 7:13 AM
Reply-To: acl2-devel@utlists.utexas.edu
To: acl2-devel@utlists.utexas.edu

Hi Eric,

Good suggestion.  I took a quick look, and it might take a bit of work
to pass the necessary information back.  The evaluation of ground
subexpressions takes place in the following call chain, from top to
bottom; the problem then is passing back the result of
eval-ground-subexpressions to chk-acceptable-linear-rule2, so that it
can print an extra message like "Note that the term was simplified to
<term> before attempting to construct a linear rule; see :DOC linear."

chk-acceptable-linear-rule2
  external-linearize
    linearize
      linearize1
        eval-ground-subexpressions

May I incorporate your email into a note to add to
books/system/to-do.txt?

Thanks,
Matt

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Possibly add function-symbolp to the guard of logicp.}}

Currently logicp returns t on a symbol that is not a function symbol, which is
slightly odd.  Adding function-symbolp to the guard of logicp would eliminate
this slight oddity, but would require discharging the ensuing guard verification
obligations.  Note also that some existing ACL2 code may rely on logicp
returning t on a non-function symbol, e.g., see the following line in the
definition of sublis-var!:

              (logicp (ffn-symb term) wrld) ; maybe fn is being admitted

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Perhaps split :doc hints into separate topics.}}

This item was added by Matt K. but is based on correspondence
initiated by Eric McCarthy.  Note that it could take some effort to do
well, since a lot of other stuff might point to :doc hints that would
then need to point somewhere else (e.g., in error messages).  Also,
it's pretty simple to search for a specific hint type within that
page, so this is perhaps not high priority [note from Matt: which is
why I'm adding this item here rather than doing it myself].  Eric
points out that with separate topics, "people can add more tips on
using hints and examples without making the page unmanageably large."

Perhaps a simple but adequate change would be for each kind of hint to
have HINTS as its parent.  Then error messages could still point to
:DOC hints, which would then show a clickable list of all hint types.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Improve argument names for set-guard-checking.}}

Alessandro Coglio had the following suggestions for renaming arguments
of set-guard-checking:

  :ignore instead of :none, since that mode ignores guards — nil and
  :none sound almost like synonyms

  :top instead of t, since that mode checks guards at the top-level —
  t is a bit nondescript, given that there’s also :all

Matt and J are happy with those new names, but want to keep the old
names too since they have been around for so long.  Also, the old
names are used throughout the code, and quite possibly in the books
too; it could be a substantial effort to be sure to touch all uses of
set-guard-checking and of state global 'guard-checking-on.

Instead, the idea is just to add aliases for set-guard-checking, but
continuing to use the old values of t and :none for state global
'guard-checking-on.  It will then also be important to change the
documentation, and also relevant output if any, to emphasize the
preferred names of :ignore and :top, while probably mentioning the old
names of :none and t as "aliases" or such (even though the aliasing is
actually the other way around).

I (Matt) suspect that this is a relatively simple development task,
and I expect whoever takes it on to deal not only with the
set-guard-checking implementation but also all relevant output and
documentation.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Perhaps avoid iteration for guessing type-prescriptions for non-rec functions.}}

Maybe don't look for a fixed point in type-prescription rule
generation if the function is non-recursive.  It's possible that the
code already does this, my guess is, probably not.

This one is probably not very important, but it might be a relatively
easy way to get familiar with the mechanism for generating
type-prescription rules for defuns.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Perhaps eliminate either directory-of-absolute-pathname or get-directory-of-file.}}

These two source functions seem to do roughly the same thing, though
one is more careful.  Perhaps they could be merged into a single
function, which might have a flag argument specifying whether or not
to check the filename argument and cause an error if the argument
isn't appropriate.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Strengthen state-p so that channel info has file-clocks that don't exceed file-clock.}}

[Note that duplicate-free open channel lists probably also needs to be
considered, as per Keshav.  See his email below the IRC thread,
below.]

Note that some books would probably need work to recertify if the
following is done.

Note from Keshav: the book std/io/open-channels contains several
examples of theorems which could be strengthened if this to-do list
item were implemented.

The predicate state-p is too weak for some purposes, because it
doesn't capture the invariant that the file-clock field of the state
is an upper bound for the file-clocks of the open channels (and
probably also of the read-files, though I haven't quite thought that
through).  If we strengthen it then presumably some proofs will need
to be redone.  Any thoughts on this?

<kini> mattjk`: Suppose I've come up with some invariant of the current ACL2
       state. There's no way for me to prove this invariant and make use of
       it, short of adding it to state-p1 in axioms.lisp, is there?  [08:01]
<kini> the actual example I have in mind is (and (no-duplicatesp (nth 0
       state)) (no-duplicatesp (nth 1 state)), which as far as I understand
       should always hold  [08:02]
<mattjk`> Could you just prove as a rewrite rule (implies (state-p state)
	  <property>)?  [08:04]
<mattjk`> Oh -- I guess you're saying that this isn't always true.
<mattjk`> In that case, I guess you could define (my-state-p state) = (and
	  (state-p state) <property>) and use that in your guards etc.  Any
	  reason that wouldn't work?  [08:05]
<kini> Hmm, I haven't tried that. But would it be possible to guard-verify
       such a thing?  [08:07]
<kini> I guess so, it would be self-contained...  [08:08]
<kini> hmm, but then would I be able to call such a function from the ACL2
       loop with the live state... guard-checking a guard on state seems like
       it might be hard since state contains some "fictional" things, doesn't
       it?  [08:09]
<mattjk`> OK, I see the problem.  I'm thinking on it....  [08:10]
<mattjk`> I think that the right solution might be to arrange that the
	  property indeed follows from state-p.  It almost does now, I think,
	  but we'd need the invariant that (file-clock state) is an upper
	  bound for all n such that, in the case of open-input-channels,
	  [exists file-name type . (list file-name typ n) is a key of
	  (readable-files state).  I don't know how disruptive that might be
	  to proving our way through axioms.lisp and to books that
								        [08:15]
<mattjk`> reason about state.
<mattjk`> Could be a fun task for you after the developer's workshop?  [08:16]
<kini> heheh, perhaps :)  [08:17]
<kini> but I don't quite follow
<kini> If we had the invariant you propose, how would that imply the one I
       gave about no-duplicatesp?  [08:18]
<kini> your invariant would be sufficient to prove that the built-in functions
       that modify (open-input-channels state) and (open-output-channels
       state) maintain my invariant, but not, I think, that arbitrary user
       functions that return state maintain my invariant  [08:19]
<kini> and such user functions could have been run at the ACL2 loop in the
       past
<mattjk`> First: I should have added that I came up with that by looking at
	  function open-input-channel in ACL2 source file axioms.lisp.  I
	  should also have added that a similar change would be needed for
	  open-output-channel.  [08:20]
<mattjk`> But maybe you already got that.  It seems to me that arbitrary user
	  functions would preserve the enhanced state-p, because they have no
	  way to mess directly with the file-clock.
<mattjk`> Do you want to have a short Skype about this now?  [08:21]
<kini> sorry, not at the moment -- I'm not at the office yet, which means my
       internet connection is only good for stuff like text chat, haha
<kini> perhaps later today if you have some time
<kini> maybe I need to understand better the stobj story for state  [08:23]
<mattjk`> Probably not today (things scheduled to keep me busy from 10:45
	  central time onward, maybe earlier even; maybe tonight).
<kini> OK.  Anyway there's no huge rush, it's just something that occurred to
       me
<kini> I don't need this invariant for anything at the moment
<mattjk`> I'll probably get J's thoughts on this on Friday.
<kini> I wrote some theorems about how open-input-channel-p1 of a channel is
       preserved under various orthogonal I/O operations, and one of the
       theorems was that if a channel is open and you close a different
       channel, the first channel remains open  [08:26]
<kini> so it occurred to me that it might be nice to have the sister theorem
       as well, that if a channel is open and you close the same channel, the
       channel then becomes closed
<kini> but the checkpoint I got when trying to prove this was basically asking
       me to prove that the list of input channels was no-duplicatesp
<kini> Sure, sounds good -- thanks!  [08:27]
ERC>

.....

[From Keshav via gmail, Sun, May 21, 2017 at 12:13 PM:]

  I'm still not sure that your condition about the file clock will be a
  sufficient strengthening of state-p1 to prove a theorem about a
  channel becoming closed after you attempt to close it, because it
  doesn't imply that there are no duplicates in the list of open
  channels.

  Your condition would allow me to prove that if there were currently no
  duplicate open channels in the state and I tried to open a channel,
  then there would continue to be no duplicates in the list of open
  channels.  But it doesn't seem to be strong enough to allow me to say
  that if (STATE-P STATE), then there are no duplicate open channels in
  STATE.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Fix handling of state result, in old-style signatures without state argument.}}

Below is the relevant email thread (with a typo from Matt fixed by
Matt).

From: Matt Kaufmann <kaufmann@cs.utexas.edu>
Subject: Re: Old-style signature with output state
Date: October 24, 2017 at 5:20:40 AM PDT
To: Alessandro Coglio <coglio@kestrel.edu>

Wow, weird!  I'll bet it's easy to fix.  May I add it to
books/system/to-do.txt and email acl2-devel about it?  Or, feel free
to do so (or even to forward this email if you like).

Thanks for letting me know --
-- Matt
Alessandro Coglio <coglio@kestrel.edu> writes:

Hi Matt,

[...]

I found that the following is accepted by ACL2, even though my reading of :doc
signature is that state may appear in the result of the signature only if it
appears in the formals:

(encapsulate
 ((f (x) state))
 (local (defun f (x) x)))

However, the stobjs-out property of f is (nil), indicating that the state output
variable has been treated like an ordinary variable.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Add two missing "Non-rec" warnings.}}

There are two cases where "Non-rec" warnings fail to be printed, but
should be:

1. Non-recursive functions in triggers of type-prescription rules
2. Non-recursive functions in hypotheses of linear rules

Below we explain each of these in turn.

-----

1. Non-recursive functions in triggers of type-prescription rules

There's no non-recursive function ("[Non-rec]") warning for the
:type-prescription rule consp-my-cons below, but there should be.  The
existing code (source function chk-acceptable-type-prescription-rule)
clearly doesn't even try to give a "[Non-rec]" warning for
:type-prescription rules except for non-recursive functions in their
hypotheses.

ACL2 !>(defun my-cons (x y) (cons x y))

Since MY-CONS is non-recursive, its admission is trivial.  We observe
that the type of MY-CONS is described by the theorem (CONSP (MY-CONS X Y)).
We used primitive type reasoning.

Summary
Form:  ( DEFUN MY-CONS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 MY-CONS
ACL2 !>(defthm consp-my-cons
	 (consp (my-cons x y))
	 :rule-classes :type-prescription)

ACL2 Observation in ( DEFTHM CONSP-MY-CONS ...):  Our heuristics choose
(MY-CONS X Y) as the :TYPED-TERM.

Q.E.D.

Summary
Form:  ( DEFTHM CONSP-MY-CONS ...)
Rules: ((:TYPE-PRESCRIPTION MY-CONS))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 CONSP-MY-CONS
ACL2 !>

-----

2. Non-recursive functions in hypotheses of linear rules

Here is one more case where we should create a "[Non-rec]" warning,
but we don't.  The log below illustrates that a rewrite rule can give
us a "[Non-rec]" in addition to the "[Free]" warning, but that's not
the case for a linear rule -- and it should be.  (Both of these are
designed to fail; of interest are the warnings.)

ACL2 !>(defthm test
         (implies (natp y) ; enabled non-rec fn
                  (< (* (car x) x) x))
         :rule-classes :rewrite)

ACL2 Warning [Free] in ( DEFTHM TEST ...):  A :REWRITE rule generated
from TEST contains the free variable Y.  This variable will be chosen
by searching for an instance of (NATP Y) in the context of the term
being rewritten.  This is generally a severe restriction on the applicability
of a :REWRITE rule.  See :DOC free-variables.


ACL2 Warning [Non-rec] in ( DEFTHM TEST ...):  As noted, we will instantiate
the free variable, Y, of a :REWRITE rule generated from TEST, by searching
for the hypothesis shown above.  However, this hypothesis mentions
the function symbol NATP, which is defun'd non-recursively.  Unless
disabled, this function symbol is unlikely to occur in the conjecture
being proved and hence the search for the required hypothesis will
likely fail.

[[.. non-warning output elided ..]]
******** FAILED ********
ACL2 !>(defthm test
         (implies (natp y) ; enabled non-rec fn
                  (< (* (car x) x) x))
         :rule-classes :linear)

ACL2 Warning [Free] in ( DEFTHM TEST ...):  A :LINEAR rule generated
from TEST will be triggered by the term (BINARY-* (CAR X) X).  When
TEST is triggered by (BINARY-* (CAR X) X) the variable Y will be chosen
by searching for an instance of (NATP Y) among the hypotheses of the
conjecture being rewritten.  This is generally a severe restriction
on the applicability of the :LINEAR rule.

[[.. non-warning output elided ..]]
******** FAILED ********
ACL2 !>

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Consider an alias or name change: VALUE-EVENT for VALUE-TRIPLE.}}

The name "VALUE-EVENT" seems more descriptive than "VALUE-TRIPLE".
Such a change might well not be sufficiently important to be worth
carrying out -- it should only be done so by someone who personally
feels that this is important, and will deal with all details that
arise from such a change.

This change is trivial at some level, but it could affect a lot of
books beyond just the community books.  So it seems important to query
the community before changing VALUE-TRIPLE to VALUE-EVENT, or more
likely, define one of them to be a macro for the other.

Before anyone embarks on this, they should read the email thread
below.

From: Alessandro Coglio <coglio@kestrel.edu>
Subject: Re: Value-triple => value-event ?
Date: Sat, 29 Sep 2018 13:22:02 -0700
To: Kaufmann Matt <kaufmann@cs.utexas.edu>
In-Reply-To: <t4dy3bk8nma.fsf@ginger.cs.utexas.edu>

Hi Matt, I understand. Adding it to the developer to-do list seems like a good idea to me. Thanks.



> On Sep 29, 2018, at 6:00 AM, Matt Kaufmann <kaufmann@cs.utexas.edu> wrote:
>
> Hi, Alessandro --
>
> Yes, I think the "triple" in "value-triple" is intended to emphasize
> that error triples are involved.  But I agree that "value-event" is a
> more descriptive [hence, better] name.  What I'm not sure of is
> whether it's sufficiently better to bother with the change.
>
> It might be very easy to make the change, by making value-event a
> macro:
>
> (defmacro value-event (&rest args)
>  `(value-triple ,@args))
>
> However, the :doc and, perhaps, error messages, would then still say
> "value-triple", so that wouldn't help much.  Things could be the other
> way around: all occurrences in the sources of value-triple could be
> changed to value-event, and then:
>
> (defmacro value-triple (&rest args)
>  `(value-event ,@args))
>
> I don't know if books changes would be needed.
>
> But even though I like your suggested "value-event" better than
> "value-triple", I don't know that it's sufficiently better to warrant
> the time spent on the changes, as there could easily be issues that
> haven't occurred to me.  I suppose that I could put this email thread
> into books/system/to-do.txt as a developer task, in case anyone wants
> to take it on.  What do you think?
>
> Thanks --
> -- Matt
> Alessandro Coglio <coglio@kestrel.edu> writes:
>
>> Hi Matt,
>>
>> Please feel free to ignore this idea, but I was wondering if 'value-event' may be a more descriptive name for what is currently called 'value-triple'. In a sense, this function “lifts” an arbitrary value to an event. I’m sure there’s a reason for the ‘triple’ of ‘value-triple’, but it’s not immediately evident to me; I looked at value-triple-fn and I see that it uses the value function to return error triples, so maybe that’s the rationale?
>>
>> Thanks.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Retain the guard of a defun-sk with :constrain t.}}

Currently a defun-sk with :constrain t has its guard set to t, regardless of
whether a different guard is specified in the defun-sk; if specified, the guard
is silently ignored. This is not a bug, because :doc defun-sk documents this
behavior, but it is undesirable.


> On May 24, 2019, at 7:57 PM, Matt Kaufmann <kaufmann@cs.utexas.edu> wrote:

> (defun-sk f (x)
>  (declare (xargs :guard (consp x)))
>  (exists y (equal (cons y y) x))
> ; Either include the following or not:
>  :constrain t)

> Then the command

> :args f

> shows that the guard is t if we use :constrain t, but the guard is
> (consp x) if we don't.  That disparity seems goofy.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Name the free variables of each rule in the output of :pr.}}

A user may need to know the free variables for a given rule in cases
where this information is not lexically visible, for instance, when
the event generating the rule has let-bindings. Currently, :pr
writes out the LHS (for :rewrite rules)/typed term
(for :type-prescription rules)/trigger terms (for
:forward-chaining/:linear rules) without syntactic sugar; it may be
desirable for :pr to also list the free variables. Note, free
variables may arise in rule classes other than the ones mentioned above.

A developer taking on this task may find Matt Kaufmann's example,
below, helpful.

ACL2 !>(let ((rule (car (find-rules-of-rune
			 '(:rewrite symbol-<-transitive)
			 (w state)))))
	 (set-difference-eq
	  (union-eq (all-vars (access rewrite-rule rule :rhs))
		    (all-vars1-lst (access rewrite-rule rule :hyps) nil))
	  (all-vars (access rewrite-rule rule :lhs))))
(Y)
ACL2 !>

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Enable the generation of extra-info hypothesis for each functional instantiation constraint}}

A couple of reasons for this: a) knowing where constraints are coming
from is useful for debugging. and, perhaps more importantly, b) the
proofs of different constraints can have radically different
strategies.  Generating extra-info hyps would allow a user to write
robust computed hints that could employ strategies appropriate for
each constraint.

There could be a table to enable this feature.  A good model for that
is the inhibit-warnings-table, where the macro set-inhibit-warnings is
a local table event using that table:

(defmacro set-inhibit-warnings (&rest lst)
  `(local (set-inhibit-warnings! ,@lst)))

Or it could be yet another acl2-defaults-table key, which would
automatically make it local to books and encapsulate events.  That's
probably best in general, but the former approach is good if one wants
a way to make the setting global in one's session, including all books
that one is certifying in that session.

Note: extra-info hypotheses are already available for guard and
termination proofs.

Note: A cursory look into how constraints are computed reveals that
some constraints (ie: from encapsulations) are associated with
function symbols at the time of their admission:

ACL2 !>(trace$ putprop-constraints)
ACL2 !>(encapsulate
    (
     ((fn *) => *)
     )
  (local (defun fn (x) x))
  (defthm integerp-fn
    (implies
     (integerp x)
     (integerp (fn x))))
  )

1> (PUTPROP-CONSTRAINTS FN NIL
                        ((IMPLIES (INTEGERP X)
                                  (INTEGERP (FN X))))
                        NIL
                        ((FN SIBLINGS FN)
                         . |current-acl2-world|))
<1 (PUTPROP-CONSTRAINTS ((FN CONSTRAINT-LST
                             (IMPLIES (INTEGERP X)
                                      (INTEGERP (FN X))))
                         (FN SIBLINGS FN)
                         . |current-acl2-world|))

In other words, enabling the event:

:hints (("Goal" :use (:functional-instance lemma
                                           (fn zed))))

to generate an attributed constraint, such as:

(implies
 (and
  (extra-info '(:functional-instantiation) '(:constraint integerp-fn))
  (integerp x))
 (integerp (zed x)))

will require us to generate constraint attribution at the time of
function admission.

[[
Matt's reply: Or will it?  It seems to me that at the time the
:functional-instance hint is processed, we have this chain of calls:

translate-lmi
calls
translate-lmi/functional-instance
calls
relevant-constraints
calls
relevant-constraints1
calls
constraint-info

If a suitable flag were passed, then constraint-info could return
extra-info.  For example, after the encapsulate above, try this:

(defthm lemma (equal (fn x) (fn x)) :rule-classes nil)
(trace$ constraint-info)
(thm t :hints (("Goal" :use (:functional-instance lemma (fn ifix)))))

Then you'll see this:

1> (CONSTRAINT-INFO FN |current-acl2-world|)
<1 (CONSTRAINT-INFO FN
                    ((IMPLIES (INTEGERP X)
                              (INTEGERP (FN X)))))

But actually, I think it would make a lot more sense to modify
relevant-constraints1 to take a flag instead of constraint-info.
... end of Matt's reply]]

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Improve :pl output when a free variable of the rule occurs in the argument of :pl.}}

Eric Smith sent this example:

(defthm <-trans
  (implies (and (< x y) ; y is a free var
                (< y z))
           (< x z)))

and then do:

:pl (< y z)

The current output is confusing, since sometimes "Y" refers to the
free variable in the hypotheses of <-trans, and other times "Y" refers
to the variable in the input term, (< y z)::

(:REWRITE <-TRANS)
  New term: T
  Hypotheses: ((< Y Y) (< Y Z))
  Equiv: EQUAL
  Substitution: ((Z Z) (X Y))
  Free variable: Y

On the acl2-devel list we seemed to agree on the following as desired
output for this example.

(:REWRITE <-TRANS)
 New term: T
 Hypotheses: ((< Y Y{FREE}) (< Y{FREE} Z))
 Equiv: EQUAL
 Substitution: ((Z Z) (X Y) (Y Y{FREE}))
 Free variable bindings: ((Y Y{FREE}))

Of course, if Y{FREE} should be suitably "fresh"; if it weren't then
we could search for the first "fresh" variable of the form Y{FREE}1,
Y{FREE}2, etc.

The same issue arises in the proof-builder: you can see it with
(verify (< y z)) followed by sr.

This issue also applies to :linear rules and perhaps others; whoever
takes this item on should figure out which rule classes are relevant
and fix them all.  Perhaps :pl2 or :pr should also be considered (not
sure).  Here's an example involving a :linear rule.

(defthm <-trans
  (implies (and (< x y) ; y is a free var
                (< y z))
           (< (identity x) (identity z)))
  :rule-classes :linear)

:pl (identity y) currently gives this output.

(:LINEAR <-TRANS)
  Conclusion: (< (IDENTITY Y) (IDENTITY Z))
  Hypotheses: ((< Y Y) (< Y Z))
  Substitution: ((X Y))
  Free variables: Y and Z

Again, an analogous issue arises in the proof-builder: you can see it
with (verify (< (identity y) (identity z))) followed by (dv 1) and
show-linears.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Move computation of defrec names from books/build/cert_features.lsp to ACL2 build.}}

By moving that compuatation (see constant *defrecs* and function
write-defrec-certdeps in books/build/cert_features.lsp) to the build,
we can compute the set of defrec names without affecting regression
times, just build time.  The computation.  Sol S. and Matt
K. discussed this and it was OK with both of them.

There are lots of examples in the ACL2 sources of defining a constant
and then checking their accuracy at the end of the build.  See
function check-built-in-constants in interface-raw.lisp.

<><><><><><><><><><><><><><><><><><><><><><><><><>

{{Fix arguments of subseq-list.}}

Simplest, and perhaps sufficient, might be to fix the start argument
of (subseq-list lst start end) to a natural number using MBE.  But
perhaps more fixing would be useful, so that the entire guard holds.

Quite a few rules about subseq-list and subseq will become more
concise and have fewer case-splits when we replace start with (nfix
start). A quick look suggests that this will, however, require some
work to get "make devel-check" (see :doc
verify-guards-for-system-functions) to pass and to get the community
books to certify afterwards.

Note that others seem to independently have noted the desirability
of doing this in :doc subseq-list.

<><><><><><><><><><><><><><><><><><><><><><><><><>