acl2/acl2

ACL2 System and Books as Maintained by the Community

acl2's Issues

Improve homepage

From [email protected] on December 06, 2007 13:43:49

We should improve the "Project Home" page description of this project,
perhaps linking to overview documentation in the wiki, giving instructions
on how to join, etc.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=8

[ACL2(p)] waterfall-parallelism for centaur directory, single-threaded clause-processors

From [email protected] on February 19, 2013 09:53:17

I currently see two obstacles to making the centaur directory compatible with waterfall-parallelism:

(1) Shared hash-tables
(2) Single-threaded clause-processors

This feature request focuses on (2).

I think that when a user tries to use ACL2(hp) with waterfall-parallelism enabled to certify the centaur directory, that they can receive errors about single-threaded clause-processors. For each error, fixing this involves one of two things:

-- Going through the files and adding .acl2 files that disable waterfall parallelism for the symptomatic files, or

-- Modifying the clause-processor so that it doesn't return state.

I think that the GL books actually need state, so we'll probably need to take the first approach for those.

Upon further investigation, it may turn out that I've already done this, but I don't think I have, so I'm filing this feature request (probably against myself).

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=37

[cutil::defprimitive] Create it

From [email protected] on March 06, 2013 14:47:36

Something like the following but more general. The idea is to tie this into defaggregate default values.

(in-package "ACL2")
(include-book "xdoc/top" :dir :system)

(defmacro defprimitive (name args body &key default)
(b* ((xdoc::mksym-package-symbol name))
`(progn
(defun ,name ,args
,body)
(defun ,(xdoc::mksym 'make- name) ()
,default)))))

(defprimitive foo (x)
(and (integerp x)
(> x 4))
:default 7)

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=45

Document :require field of defaggregate (std)

From [email protected] on February 07, 2013 12:12:13

The new defaggregate syntax is great, thanks Jared!!!

However, based on my current understanding of defaggregate (which could be wrong!), it feels a bit clunky to implement dependent types. E.g., is there a way to get rid of the two integerp tests in the definition of two-integers-correctly-related? We could just use the "<" inline with the declaration of my-int-r, but there's no notion of using the declared type information to satisfy the guards on "<".

(defun two-integers-correctly-related (q r)
(and (integerp q)
(integerp r)
(< q r)))

(cutil::defaggregate dependent-foo
((my-int-q integerp)
(my-int-r (and (integerp my-int-q)
(two-integers-correctly-related my-int-q my-int-r))))
:tag :dependent-foo)

A work around that makes a little bit of sense is to use the :require option from a readability perspective, like follows:

(cutil::defaggregate dependent-foo
((my-int-q integerp)
(my-int-r integerp))

:require
((dependent-type-lemma-1
(and (integerp my-int-q)
(integerp my-int-r)
(< my-int-q my-int-r))))
:tag :dependent-foo)

But what if we had the following:

(cutil::defaggregate dependent-foo
((my-int-q integerp)
(my-int-r integerp))
:dependent-requirements
((< my-int-q my-int-r))

:tag :dependent-foo)

And defaggregate could be modified to use the type information from the declarations of the variables as forced hyps for the dependent-requirements lemmas.

Obviously, in some sense, this is just "more work." But, the idea seems like it could be nice, so I thought I'd throw it out there.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=34

Documentation of deflist

From [email protected] on December 05, 2012 08:36:41

Modify xdoc for deflist to mention mutual-recursion as a potential application under the :already-defined-p flag (so that the flag comes up when searching for "mutual")

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=20

Move books/system/io.lisp to books/io/base.lisp

From [email protected] on January 10, 2013 13:48:01

This is a books organization change. I started to make the change myself, and I was going to place a wrapper for io/base.lisp inside the system directory as part of the transition strategy. However, this wrapper introduces a circular Make dependency (the file that needs to move depends on system/f-put-global.lisp), so it's infeasible to leave this wrapper behind.

I could make the change anyway, because there's nothing in the regression suite that depends on system/io.lisp. However, I suspect it will break Centaur's books, and then force them to update their includes. Rather than break their build, I leave this relatively simple task for them to do.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=27

Automatic default values for defaggregate

From [email protected] on March 06, 2013 14:24:19

Suppose we have an aggregate pair:

(cutil::defaggregate pair
((first integerp :default 0)
(second integerp :default 0)))

Now suppose we have a bar that includes a pair:

(cutil::defaggregate bar
((x pair-p)
(y pair-p)))

It would be useful to have the default for x and y to automatically be calls of (make-pair), instead of just nil. This could be possible, because I think we can detect that bar-p is an aggregate.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=44

Move books/unicode/read-file-characters to books/io/read-file-characters

From [email protected] on January 10, 2013 15:24:25

What is the organizational change? Move books/unicode/read-file-characters to books/io/read-file-characters Will this change likely break books outside the repository? If it is known who will have to fix these books, cc them in this report. Yes.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=28

Developing some book conventions

From [email protected] on December 06, 2007 13:40:02

Can we agree on some style principles, e.g.,

• Don't use non-local in-theory events
• Use Eric-style names, e.g., foo-of-bar-when-baz
• Use -cheap when introducing backchain-limited rules
• Be arithmetic-agnostic

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=4

Remove older rtl books

From [email protected] on December 06, 2007 13:41:42

Can we get rid of rtl/rel5 and so on?

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=6

Arithmetic books are incompatible

From [email protected] on December 06, 2007 13:41:01

This has been a problem forever.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=5

Convert #+acl2-par occurrences in .acl2 files to a make-event

From [email protected] on February 19, 2013 12:07:43

In order to better support multiple Lisps, we could consider changing each #+acl2-par (e.g., in books/models/jvm/m5/apprentice.acl2) to a make-event that inspects the ACL2 state and only calls the set-waterfall-parallelism* primitive if par/hons/some-combo-thereof is/are enabled.

Supposedly this is only an issue to those who use multiple lisps. Thus, so long as Kaufmann is happy, we don't actually plan on fixing this. However, we file the idea for later in case we need it.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=39

Provisional certification

From [email protected] on December 08, 2007 10:18:34

I think this is an idea Jared's been using in his project as a sort of
unofficial certification mechanism in order to enable him to hog 64 cores
with a single parallel build. I think it would also almost eliminate the
need for project-specific makefiles, since anyone who wanted to certify a
library could do all the books in any order.

When a book is being certified, currently any other book that it includes
must have an up to date certificate (with correct checksum) or the
certification will fail. What if we allowed books to be certified even
when their dependencies were uncertified? Include-book always checks
recursively that all dependencies are correctly certified and (by default
outside of certify-book) issues a warning if not. This wouldn't change --
one could certify a book and subsequently receive a warning when including
it, if its dependencies weren't certified. Obviously including a
provisionally-certified book would be unsound in general; only when no such
warnings were issued would we expect soundness.

This idea would need to be more fully fleshed out in order to be
universally applicable. There are, I think, four or so main areas in which
unforeseen (by me) problems could prevent this from working well:

• portcullis events: are include-book's current portcullis checks enough?
  should certify-book somehow warn about missing portcullis events from
  included uncertified books?
• make-event: is the full expansion of all events included in the
  checksum? other problems?
• local: seems okay to me, but who knows
• ttags: ditto; certainly there shouldn't be a way (modulo forging a
  certificate) to sneak a ttag into a dependency of a book certified without
  ttags.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=11

Add appropriate package inclusion so books/security/des.lisp can use GL

From [email protected] on December 12, 2012 17:34:50

For this checkin: https://code.google.com/p/acl2-books/source/detail?r=1374 In books/security/des/des.lisp, Soumava and I would like to use GL to prove a theorem. However, we couldn't figure out a decent way to define the GL package so that the call of def-gl-thm would work when calling certify-book.

So, we commented out the calls to the GL package and submitted the books as is. Someone who knows how packages work in ACL2 (and even more so if they know how to include the GL defpkg) should be able to fix this up pretty easily.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=25

Axioms.lisp has theorems in it

From [email protected] on December 06, 2007 13:36:20

There are defthms (and defaxioms) in axioms.lisp which are enabled. We
can't change these in the repository easily, even if we want to. Maybe we
want to consider ways of moving them into books, or maybe it isn't a big
deal since we can just email Matt a change if we want to make one.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=2

Extend define to support documented test cases

From [email protected] on March 25, 2013 11:38:18

Add tests to define's definition and automatically incorporate those tests into the generated xdoc.

Just an idea -- it might be good, because it would automatically increase the documentation, but it might be bad, because, presumably, we don't want cutil::define to be too much like the kitchen sink. Plus, including tests automatically might keep us from feeling like we need to invest the time in making nice and descriptive English sentences.

We can note that the tests have not been added as documentation, but that it would be useful to have the tests as part of the documentation in revision 1621 of regex-ui.lisp

(define do-regex-match
((str stringp "String to test")
(pat stringp "String representing the pattern to find")
(opts parse-opts-p "Options for test.

                   BOZO: state and explain the possible options.  Possible
                   options might include
                   <tt>:b</tt>/<tt>:e</tt>/<tt>:f</tt> for
                   basic/extended/fixed, <tt>:i</tt> for case-insensitive,
                   <tt>:full</tt> for something, etc."))

:short "Test whether a given string matches a given regular expression"
:long "Intended for use in the dynamically compiled case"
:parents (regex)
:returns (mv (error-msg (or (stringp error-msg)
(not error-msg))
"Error message"
:rule-classes :type-prescription)
(whole (or (stringp whole)
(not whole))
"The portion of str that matches the pattern
provided by pat. Nil if there is not
a match."
:rule-classes :type-prescription)
(substrs true-listp
"List of substrings that match parenthesized
subexpressions of the pattern (when applicable).
Nil if there is not a match."
:rule-classes :type-prescription))
(b* ((str (mbe :logic (if (stringp str) str "") :exec str))
(pat (mbe :logic (if (stringp pat) pat "") :exec pat))
(pat (if (parse-options-case-insensitive opts)
(str::downcase-string pat)
pat))
(regex (regex-do-parse pat opts))
((when (stringp regex))
(mv regex nil nil))
((mv whole substrs)
(do-regex-match-precomp str regex opts)))
(mv nil whole substrs)))

; examples
(local (assert! (mv-let (error-msg whole substrs)
(do-regex-match "cdeAbfdEfDeghIj"
"ab([def]*)\1([gh])"
(parse-options 'ere ; type
nil ; not strict-paren
nil ; not strict-brace
nil ; not strict-repeat
t ; case-insensitive
))
(and (not error-msg)
(equal whole "AbfdEfDeg")
(equal substrs '("fdE" "g"))))))

(local (assert! (mv-let (error-msg whole substrs)
(do-regex-match "cdeAbfdEfDeghIj"
"ab([def]*)\1([gh])"
(parse-options 'fixed ; type
nil ; not strict-paren
nil ; not strict-brace
nil ; not strict-repeat
t ; case-insensitive
))
(and (not error-msg)
(not whole)
(not substrs)))))

(local (assert! (mv-let (error-msg whole substrs)
(do-regex-match "cdeAbfdEfDeghIj"
"cdeabfdefdeghij"
(parse-options 'fixed ; type
nil ; not strict-paren
nil ; not strict-brace
nil ; not strict-repeat
t ; case-insensitive
))
(and (not error-msg)
(equal whole "cdeAbfdEfDeghIj")
(not substrs)))))

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=50

Remove ttag requirement from cutil::define

From [email protected] on January 10, 2013 15:26:04

What is the idea? Remove ttag requirement from cutil::define Which book(s) and/or directories would be affected by this request? Anything that uses define. How many people will be affected by this feature? 2

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=29

[critpath.pl] Add option to see deeper directory structure

From [email protected] on February 12, 2013 13:55:21

The danger in telling others about one's work is that they'll use it! Critpath.pl is definitely great, thanks for contributing such a nice tool to the community!

I could use an improvement to critpath.pl to disambiguate the y86/x86 books. There are three branches for books that are basically the same in https://code.google.com/p/acl2-books/source/browse/#svn&#37;2Ftrunk&#37;2Fmodels&#37;2Fy86 The branches are fine imho, but it'd be nice to know which branch I'm in when looking at the individual file timing that critpath reports.

I'm not saying that anyone should spend their time on this -- maybe I'll do it if I want it badly enough.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=35

Document regex library

From [email protected] on March 19, 2013 16:47:22

It seems that making the regex binder available requires including books/regex/regex-ui, but it would be nice if its existence was somehow discoverable via a search engine. E.g., I'd like searching on Google for "site:fv.centtech.com/acl2/ regex" to return something meaningful.

It's questionable where the right place to put this documentation is. The easiest thing is to manually update topic "B*-binders".

Another option would be to create a new top-level regex topic, and to link to it (or one of its children) from b*-binders.

Another much more time-consuming option would be to automatically include all uses of def-b_-binder that occur within the repository inside the "B_-binders" xdoc topic, in a second section that is automatically generated. Haha - no one has the time and motivation to do this one, but it's still a neat idea.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=47

data-structures/alist-defthms and coi/alists/ are incompatible

From [email protected] on May 10, 2011 18:49:40

In data-structures/alist-defthms:
(defthm assoc->assoc-equal
(equal (assoc x a)
(assoc-equal x a)))

In coi/alists/equiv.lisp:
(defthm assoc-equal-reduction
(equal (assoc-equal x y)
(assoc x y)))

Plus, all the useful theorems in data-structures/ are defined only for assoc-equal, and all the useful theorems in coi/alists/ are defined only for assoc.

It would be nice to pick one convention or the other. (I like the coi/alists convention, just because "assoc" is shorter than "assoc-equal".)

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=14

Add calls of with-waterfall-parallelism to some of the slower books that benefit from waterfall parallelism

From [email protected] on January 11, 2013 06:45:34

What is the idea? Speedup the time it takes to make some of the more time consuming books when using ACL2(p) Which book(s) and/or directories would be affected by this request? All that are reported to be time consuming in Rager's dissertation. How many people will be affected by this feature? Anyone who build workshop books.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=30

Create deprecated-include-book macro

From [email protected] on January 14, 2013 12:09:31

I should create a deprecated-include-book macro for use in these stubs and change the stub books in the repository to use it.

The objection ya'll might have is that it makes searching for (for example) "(include-book "misc/take")" harder, but it's basically the same thing to search for "include-book "misc/take")".

Any protests?

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=33

[books-cleanup] Libraries need documentation

From [email protected] on December 06, 2007 13:42:40

Erik suggeted an "index.html" file in each directory, possibly
automatically generated by doc strings, possibly hand-written. It would be
good to add documentation for the existing libraries and an index
describing the functionality they provide.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=7

Already-defined-p for defaggregate

From [email protected] on December 05, 2012 08:37:31

Add already-defined-p flag to defaggregate and document it as a possible solution to the mutual-recursion problem.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=21

Defstructure accepts malformed structures without complaining

From [email protected] on November 08, 2009 14:42:48

Defstructure will accept malformed (according to its BNF specification for
input as given by http://www.cs.utexas.edu/users/moore/publications/others/defstructure-brock.ps )
structures without any form of complaint:

Example:

(include-book "data-structures/structures" :dir :system)

(defstructure good
(afield (:assert (natp afield) :rewrite))
(bfield (:assert (consp bfield) :rewrite)))

(defstructure bad
(afield (:assert (natp afield)) :rewrite)
(bfield (:assert (consp bfield) :rewrite)))

No error is produced when "bad" is accepted, however defs-bad-assertions
will not have an assertion corresponding to the first field as good does:

ACL2 !>:pe defs-good-assertions
d 2 (DEFSTRUCTURE GOOD (AFIELD #) ...)
\

        (DEFTHM
            DEFS-GOOD-ASSERTIONS
            (IMPLIES (GOOD-P GOOD)
                     (AND (WEAK-GOOD-P GOOD)
                          (NATP (GOOD-AFIELD GOOD))
                          (CONSP (GOOD-BFIELD GOOD))
                          T))
            :RULE-CLASSES
            ((:REWRITE :COROLLARY (IMPLIES (GOOD-P GOOD)
                                           (NATP (GOOD-AFIELD GOOD))))
             (:REWRITE :COROLLARY (IMPLIES (GOOD-P GOOD)
                                           (CONSP (GOOD-BFIELD GOOD))))))

ACL2 !>:pe defs-bad-assertions
d 3:x(DEFSTRUCTURE BAD (AFIELD # :REWRITE)
...)
\

        (DEFTHM
              DEFS-BAD-ASSERTIONS
              (IMPLIES (BAD-P BAD)
                       (AND (WEAK-BAD-P BAD)
                            (NATP (BAD-AFIELD BAD))
                            (CONSP (BAD-BFIELD BAD))
                            T))
              :RULE-CLASSES
              ((:REWRITE :COROLLARY (IMPLIES (BAD-P BAD)
                                             (CONSP (BAD-BFIELD BAD))))))

Including >= 2 fields makes this error particularly annoying -
defs-bad-assertions will still exist, it just will be missing an assertion.
With more fields an error of this form becomes difficult to detect.

I thought I would report this so it is known, but I may try to fix this
myself. At minimum it would probably be good to note somewhere that
although defstructure does have a rigorously defined BNF spec for its input
it does not fully check for adherence to this spec.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=12

Document :red, :blue, and :gold mode (ihs)

From [email protected] on March 08, 2013 11:54:27

IHS seems like a nice library.

It would be nice either to have documentation that either explains these modes, or if they're already explained elsewhere, to have a pointer to such an explanation, in this xdoc topic: http://fv.centtech.com/acl2/latest/doc/centaur/html/ACL2____IHS-DEFINITIONS.html

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=46

Uniform build system

From [email protected] on December 06, 2007 13:47:18

Can Makefile-generic be simplified or do we want to switch to something
crazy like omake.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=10

[cutil::define] using :returns with :hyp :fgaurd does not error

From [email protected] on February 27, 2013 15:37:29

We should probably cause an error when fguard is mispelled (it was fgaurd in the case I encountered).

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=40

B* integration with defaggregate

From [email protected] on March 04, 2013 16:33:56

This might end up being a will-not-fix feature request, but I wanted to document it. Regardless, it's pretty low priority.

It strikes me as odd, in the following example, that I can make reference to better-but-not-good-enough-bar.first but not to better-but-not-good-enough-bar. I'm guessing there's an implementation reason for this, but from a user perspective (really, my perspective), it's a bit odd. Look for the call of change-bar (sorry about the long example).

(cutil::defaggregate foo
((left integerp)
(right integerp)))

(cutil::defaggregate bar
((first foo-p)
(second foo-p)))

(cutil::define raise-the-bar
((the-bar bar-p))
(b* (((bar better-but-not-good-enough-bar) the-bar))
(change-bar the-bar ; works
:first
(change-foo better-but-not-good-enough-bar.first
:left 4))))

(cutil::define raise-the-bar
((the-bar bar-p))
(b* (((bar better-but-not-good-enough-bar) the-bar))
(change-bar better-but-not-good-enough-bar ; doesn't work
:first
(change-foo better-but-not-good-enough-bar.first
:left 4))))

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=41

Document two-nats for measures

From [email protected] on December 05, 2012 22:22:37

Document unicode/two-nats-measure

Also make an example that uses it in demos/making-an-ordinal-measure-from-two-nats.lisp

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=22

Document cert.pl in xdoc?

From [email protected] on March 22, 2013 16:17:42

Seems like cert.pl should include this in its help message. Or, at least point to an xdoc topic that explains that it's available.

I'm guessing part of why it's not yet documented is that we're still working out some of the Make/cert.pl building issues. https://code.google.com/p/acl2-books/source/detail?r=1545&spec=svn1580

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=49

Better recognizer debugging for aggregates

From [email protected] on October 15, 2012 21:58:54

Suppose we define a new data structure, called a foo, by calling defaggregate. Now suppose that we use the foo-p predicate in the guards of functions. Now suppose that we have concrete executions of these functions with non-verified guards (so we could also be calling these functions from the top-level). Finally, suppose we call one of these functions with an argument that is supposed to be a foo-p but actually isn't. We will receive an error that indicates we have a guard failure.

One option is to use ACL2 function/macro print-gv to debug our failure. That works okay, but what I'd like instead is to have the predicate comment-window print the offending member of the foo with a nice error message. Of course, we won't always want this printing on, so the printing should probably be enabled/disabled with a table event (for example) or with the call of defaggregate that defines foo-p.

The demand for this is probably fairly low, but Rager might just do it at some point. The problem of "what's causing this guard failure?" has plagued users for a long time, and while print-gv (introduce in ver ~4.0) is a nice improvement, we can obtain more debugging information by modifying and using defaggregate.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=17

Automatic build server

From [email protected] on December 06, 2007 13:45:36

It would be nice to have a server that builds this stuff every day with all
the lisps. Careful of security issues. (Chroot jail?)

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=9

Convention for relocating books

From [email protected] on January 14, 2013 11:13:25

One way to keep book relocations from breaking things (especially outside the repository) is to replace the original book with a stub file that just includes the book in its new location. I think this is advisable in general, so as not to suddenly break things.

An additional convention I'd propose we adopt is the inclusion of a line marking the replacement book as a stub, i.e.:

(in-package "ACL2")
;; The following line marks this book as a relocation stub:
;; cert_param: (reloc_stub)
(include-book "new/location/of/this/book" :dir :system)

This extra line will allow the cert.pl build system to mark this book as a stub and perhaps (not yet implemented) print a warning whenever a book includes the stub, so that eventually these books may be updated with the new file locations and the stub can be removed.

This extra line also can allow these books to be excluded from the Makefile-generic build system, which might be desirable in order to avoid directory-level dependency loops (?). E.g., the directory's Makefile might contain:

include ../Makefile-generic

The following line excludes books that contain the stub marker

BOOKS := $(patsubst %.lisp, %, $(shell fgrep -L 'cert_param: (reloc_stub)' *.lisp))
-include Makefile-deps

Any objections to adopting this convention?

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=32

[cutil::define] Add table event to define so user can query for signature of a function

From [email protected] on December 12, 2012 17:59:09

We could save the guard and return value obligations in a table event so that a user could query for the signature of the defined function without having to go find the definition in their source code.

For example:

(define foo ((a integerp)
(b string-listp))
:returns (ans consp :hyp :fguard)
(cons a b))

(signature 'foo)
==>
Foo takes as arguments
A, of type integerp
B, of type string-listp

Foo returns
Ans, of type consp

OR

(signature 'foo)
==>
((a integerp) (b string-listp)) => (ans consp)

Whether signature writes a narrative or just returns the original formals declarations is subjective. I probably prefer the latter.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=26

Integrate defenum with xdoc

From [email protected] on February 19, 2013 11:10:18

For example:

(cutil::defenum my-enum-p
((:one "the doc for one")
(:two "the doc for two")))

Admittedly, the parens are a annoyingly a bit more verbose than

(cutil::defenum my-enum-p
(:one ; the doc for one
:two ; the doc for two
))

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=38

Books documentation and topics with the same names

From [email protected] on December 10, 2012 13:04:17

I note that close-output-channel has two documentation topics: the one defined in the ACL2 source code and the one defined in books/system/io.lisp.

Both topics seem to show up in the index for the latest version of the xdoc manual that includes the centaur books. However, both links result in showing the built-in ACL2 :doc topic. Shouldn't one of them (specifically, the first of the two links) point to the xdoc created by the :defsection inside books/system/io.lisp?

This is on Google Chrome/Chromium.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=24

[regex] Add xdoc to regular expression library

From [email protected] on March 19, 2013 16:49:56

Seems like the regex library could have some users. It'd be nice to document it so these users and future users could figure out how to get started using it.

As a start, some of the functions in regex-ui look like they'd be a natural fit for using cutil::define, which would auto-build some of the documentation for us. That being said, we still should have a nice top-level topic that introduces the best-practices for using the library.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=48

Document the limitations of defaggregate when using macro recognizers

From [email protected] on October 08, 2012 13:06:13

The defaggregate documentation could describe why using macros as recognizers results in :rewrite rules that aren't acceptable to ACL2. Minimally, it could state that not being able to use macros is a known-issue.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=16

Add Readme.lsp to the new std directory

From [email protected] on January 11, 2013 06:52:27

The new std directory (soon to be committed) needs to be documented. I'm going to save writing that documentation until after getting some feedback from the community (basically depending upon how much complaint there is about things breaking).

Also, I plan on continuing to move some things into std, so refraining from writing Readme.lsp early on will mean less short-term editing for me.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=31

Create a way to efficiently search books to answer the question "what books contain useful theorems about function ___"

From [email protected] on December 08, 2012 22:20:20

Create a way to efficiently search books to answer the question "what books contain useful theorems about function ___"

For example, right now I need a lemma about append that says

(implies (and (string-listp x)
(string-listp y))
(string-listp (append x y)))

A book that contained this lemma could contain other useful lemmas. Actually there is one hit in a VL book. But, can that really be all?

Example of searching code base for "(string-listp (append" https://code.google.com/p/acl2-books/source/search?q=&#37;22&#37;28string-listp+&#37;28append&#37;22&origq=&#37;22&#37;28string-listp+&#37;28append&#37;22&btnG=Search+Trunk

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=23

Verify guards of system functions

From [email protected] on April 04, 2012 10:22:09

This could be a nice place to list some system functions whose guards we'd like to verify. Possible motivations include:

-- Proof exercise for those learning ACL2 or just wanting to do some proofs

-- If Rager recalls correctly, it would make those system functions more attachable (via defattach)

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=15

[ACL2(p)] waterfall-parallelism for centaur directory, shared hash-tables

From [email protected] on February 19, 2013 09:53:02

I currently see two obstacles to making the centaur directory compatible with waterfall-parallelism:

(1) Shared hash-tables
(2) Single-threaded clause-processors

This feature request focuses on (1).

Currently when a user tries to use ACL2(hp) with waterfall-parallelism enabled to certify the centaur directory, they receive a lot of errors that look like:

---

.************ ABORTING from raw Lisp ***********
Error: .Not owner of hash table .#<.HASH-TABLE .:TEST .EQL size 1/62 #x30200C652DAD>

---

This could be fixed in one of two ways:

-- Going through the directory and adding .acl2 files that disable waterfall parallelism for the symptomatic files, or

-- Modifying ACL2(h[p]) so that the hash table reporting a violation is :shared (perhaps only :shared in #+acl2-par... but we would probably need to test to see whether that causes an issue... I don't know what it means for performance to load a :shared hash-table into an image from which you've explicitly exluded parallelism (ACL2(h)).

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=36

[cutil::defaggregate] Allow user to specify default values

From [email protected] on November 27, 2012 22:09:00

Add a way to specify default values for the members of an aggregate. Also consider using the syntax about to used in an upcoming macro to infer requirements on the members.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=19

What should we do with the workshop books

From [email protected] on December 06, 2007 13:37:28

I haven't bothered to upload them yet. Maybe we want them, or just some of
them. Shrug.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=3

[books-cleanup] Create advise/trace mechanism for asserting that return values of functions satisfy predicates provided by defaggregate

From [email protected] on March 05, 2013 15:27:57

Create advise/trace mechanism for asserting that return values of functions satisfy predicates provided by cutil::define.

Might require adding to the data that is stored in tables during a cutil::define. And then writing a book in cutil that takes advantage of that stored data.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=43

Create a 4.0 branch

From [email protected] on July 08, 2010 13:49:29

We have one for 3.6. Seems like we should add this to our todo list. Or we can just wait until someone wants it. I don't need it myself.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=13

Procedure for moderating commits

From [email protected] on December 06, 2007 13:31:07

We probably eventually want to develop some kind of process in case there
are disputes about whether a certain change should be accepted.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=1

Update cutil::defalist doc

From [email protected] on October 26, 2012 11:51:33

Update cutil::defalist documentation to suggest some alternatives to assoc and maybe acons (of course both of these are easy to write... I'd just rather see a standard evolve). It seems like they should exist in the ACL2 books somewhere since a non-nil-terminated alist would be useless without a lookup function.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=18

Define could automatically bind defaggregates

From [email protected] on March 05, 2013 11:45:35

Use the declared types of arguments to cutil::define to automatically bind field names.

Suppose one has a pair aggregate:

(cutil::defaggregate pair
((first integerp)
(second integerp)))

Then one defines function my-f to use that pair:

(cutil::define my-f ((x pair-p))
(+ x.first x.second))

This would expands to the following (among other things):

(defun my-f (x)
(declare (xargs :guard (pair-p x)))
(let* ((x.first (pair->first x)))
(x.second (pair->second x))))
(+ x.first x.second)))

Implementation desire and hazard:

It would also be good for this to work for nested aggregates. By this, I mean suppose a Pair-p contained two Foo-p's. And Foo-p's have fields Left and Right. Should cutil::define automatically bind pair.first.left, pair.first.right, pair.second.left, and pair.second.right?

Either (1) define has to scan the body to find out what's used, or (2) we can declare everything and make them ignorable. If we choose (1), what if the user rebinds pair.first.right in their function's body and the original value is never used? Do we even care? Probably not. The syntax is already strange enough and would be documented in define's xdoc, that if a user "happens upon it", I wouldn't feel too badly. I'm actually currently in favor of (2), because it has the simplest story to tell.

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=42