A journey with the preprocessor and defprod

How many fields does it take to break defprod?  Hint: you already know the answer.  42!

Why is this?  Suppose you have the following forms:

(include-book "centaur/fty/deftypes" :dir :system)
(fty::defprod slow-it-down
 ((a booleanp) (b booleanp) (c booleanp) (d booleanp) (e booleanp)
 (f booleanp) (g booleanp) (h booleanp) (i booleanp) (j booleanp)
 (k booleanp) (l booleanp) (m booleanp) (n booleanp) (o booleanp)
 (p booleanp) (q booleanp) (r booleanp) (s booleanp) (tt booleanp)
 (u booleanp) (v booleanp) (w booleanp) (xx booleanp) (y booleanp)
 (z booleanp) (aa booleanp) (ab booleanp) (ac booleanp) (ad booleanp)
 (ae booleanp) (af booleanp) (ag booleanp) (ah booleanp) (ai booleanp)
 (aj booleanp) (ak booleanp) (al booleanp) (am booleanp) (an booleanp)
 (ao booleanp) (ap booleanp)
 (aq booleanp) ;; the offending threshold
 ))

As of May 16, 2016, you’ll get a nice error that says the preprocessor’s rewrite stack has reached its limit and quit:

HARD ACL2 ERROR in PREPROCESS: The call depth limit of 1000 has been
exceeded in the ACL2 preprocessor (a sort of rewriter). There is probably
a loop caused by some set of enabled simple rules.

But there are no such looping rules (that I found).  This is evident by the error going away (and an analogous proof completes over a weekend in 130,000 seconds — hah!).

You might think it clever to disable the preprocessor.  That _might_ work, but there are three difficulties with that:

  1. There isn’t any published way to disable the preprocessor at the top-level (there may not be any), and we’re deep inside defprod
  2. Modifying defprod not to call the preprocessor in just the right place could break  other uses of defprod
  3. The subgoal generated when you do disable the preprocessor looks a lot like something a preprocessor could be good at (though, I suspect that in ACL2 we need generalization):
    (IMPLIES
     (AND
      (ALISTP X)
      (CONSP X)
      (CONSP (CDR X))
      (CONSP (CDDR X))
      (CONSP (CDDDR X))
      (CONSP (CDDDDR X))
      (CONSP (CDR (CDDDDR X)))
      (CONSP (CDDR (CDDDDR X)))
      (CONSP (CDDDR (CDDDDR X)))
      (CONSP (CDDDDR (CDDDDR X)))
      ...)
     (EQUAL (LIST (CONS 'B (<booleanp-fix> (CDR (CAR X))))
                  (CONS 'C (<booleanp-fix> (CDR (CADR X)))))
            X))

With what solution did I end up?

Change the format of the defprod from the default of being represented as an alist to being represented as a tree.

It’s still slow, and I’ll probably clean it up some more, but now it finishes in 666.04 seconds instead of 130,000.

Migrated Leeroy from home to Google Compute Engine

Leeroy (our community Jenkins server) is more or less migrated to Google Compute Engine.  When it’s up, it can be viewed at the same old URL, leeroy.defthm.com.

DSC04820 - cropped

Leeroy has been running in GCE for awhile now, but it took a bit of time to set it up the way I wanted.  Specifically, I wanted to make it a preemptible instance that was automatically restarted once resources became available again.  This costs about a quarter of what it would cost to have the instance up all the time.  Since our community is a humble community, it’s probably fine for the server to have some downtime.  Having it up most of the time will make committing to the “testing” branch more meaningful, as Leeroy automatically merges in changes that pass “testing” into “master.”

This frees up my home machine(s) but leaves me wondering… what am I going to do with all of this RAM @ home?

Leeroy is back!

The continuous integration server is back online.  Phew!  Turns out that either new subnets get assigned the “public” windows 7 firewall setting by default, or I selected “public” at some point without realizing it.

While updating my DHCP leases, I was really pleased to see that Synology web interface automatically redirected me to its new IP address, without requiring me to type it in.  Way to think of a border case and address it elegantly Synology!

http://leeroy.defthm.com

Also, I’ve decided to make leeroy’s read-only access public.

Leeroy under construction

I picked up a new Buffalo router that runs DD-WRT.  It seems there’s a bug with port forwarding in this router (although I get an IP assigned in a different IP block than with the old router), so leeroy should be considered under construction until I sort that out.

Leeroy

A continuous integration server for the ACL2 community is now hosted at http://leeroy.defthm.com.  To make my life easier (and not have to worry as much about security), you need an account to read the build status.  But, I’m happy to provide such an account upon request!

Beyond just informing us as to the status of the build, another nice perk of having a CI server is that the “acl2” build target functions as a gatekeeper for automatically pushing commits that are still able to build the manual from a “beta” branch to a “master” branch.  This lowers the amount of paranoia that I must maintain when committing changes.

.leeroy

The service is currently sponsored exclusively by Defthm Consulting, but we’re looking for financial sponsors who can help us scale up from 3 cores and 16GB of RAM to using hardware available via cloud services like Google Compute Engine and Amazon Web Services.  This would allow the community to determine the status of various ACL2 builds based upon building more than just arithmetic-2 (the current “acl2-multi” build target).  The estimated cost for this better service is somewhere around $5000 per annum.

A screenshot of the “acl2-multi” build status:

leeroy-acl2-multi

Greetings

Defthm Consulting LLC came into being in 2013 and exists as a mechanism for funding projects of interest to the ACL2 community.  Please contact David Rager (ragerdl@defthm.com) with any questions you may have.

Switched ACL2 from googlecode to github

We have completed the conversion from using svn on googlecode.com to using git on github.com.  The new repository is stored at https://github.com/acl2/acl2.  You can check it out using the following command:

git clone https://github.com/acl2/acl2

We invite you to contribute to the repository by following (and improving) the guidance at
http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual/?topic=ACL2____GIT-QUICK-START

We will be moving the wikis and issue tracker to github over the next couple weeks.  Feel free to contribute to those on googlecode until we say that we’re about to move them (due to needing to be able to edit the wikis, committing to the googlecode repositories is still possible, but we do not recommend it).

You may notice that we have merged the Community Books (formerly acl2-books) and ACL2 System (formerly acl2-devel) repositories into one.  Nevertheless, changes should be made only to the books/ subdirectory unless you are Matt or J, since everything outside books/ is part of the ACL2 system.  (If you have suggestions for system changes, they should be sent to Matt or J, as has been done in the past.)

As always, feel free to ask questions via an ACL2 help email alias or the IRC channel #acl2.  We expect some questions on the best-practices for our community and how to use git and github.

If anyone is curious how this repository was created (it wasn’t trivial), and what tests were performed to ascertain its quality, you can view the scripts, supporting files, and logs at https://github.com/ragerdl/svn-to-git.  I provide a summary below the
signature.  Thanks to David Rager for performing most of the work.
Also thanks to Jared Davis, Matt Kaufmann, and Keshav Kini for
help with many issues.

Creation Process:
— Dump both subversion repositories using svnsync and svnadmin
— Create a new svn repository with the books repo mounted in a books subdirectory
— Remove all branches and tags from the svn repository (but leaving their history)
— Convert the svn repo to git, canonicalizing emails to match github account email addresses
— Remove all references to branches and tags in the history using “bfg”
— “Rewrite” the git history to accommodate the move from uvnaimor-3 many years ago, the moving of the ACL2 system trunk up to root, and the moving of the books up a level
— Create a new repo and “cherry-pick” the 4000+ commits in order of timestamp to create a nicely ordered history
— Pushed the resulting repo to github

QA Process
— For each extension found in the svn repository, ensure that the number of files in the svn repository matches the number of files in the git repository.
— Did a diff to ascertain that everything that is in both repositories is the same (requires previous step for validity)
— Ran books “everything” target a couple times and also “manual” once.  I only did this using CCL and Hons.  I had a couple quicklisp issues, but they’re unrelated.
— Jared and I looked at the gitk output.
— David, Matt, and Jared performed diffs between the svn version and the git version and ascertained that the differences were reasonable.

(post shared after the fact and backdated)