MattKaufmann
MattKaufmann
Apparent incompleteness for books/build/universal-dependency.certdep I seem to have found a case where books/build/universal-dependency.certdep didn't do the job that I think was intended, i.e., to force recertification of all books. In...
Here is how I was able to get ACL2(p) to hang with waterfall-parallelism on, both in Linux and on a Mac. I've seen this in lots of books when trying...
I think this has cdoame up before, but I can't remember what was said and I think this deserves to be a GitHub Issue. Recently an ACL2 user asked me...
I've explained the problem here: https://www.cs.utexas.edu/users/kaufmann/quicklisp-lw/
Consider changing warnings "found topics with non-existent parents" into errors, just as we already treat broken links as errors. A simple fix might be to replace the following code in...
I've run into an ACL2(p) issue with defoption that I'm having difficulty solving, so I've punted by turning off waterfall-parallelism in some places, with commit fb11bed6972bf31e8d1315cfe257d8d33269cfc2. See the long comment...
This is pretty minor, but I'm making it an Issue at Sol's suggestion. In a bash shell, where $ACL2 is defined, I successfully did (changing names here) the following: ```...
As pointed out to me by Alessandro Coglio, when attempting to build the manual in books/ with ``` make -j 4 manual USE_QUICKLISP=1 ``` the book centaur/sv/tutorial/boothpipe.lisp can fail to...
It appears that include-raw is not sensitive to having run (set-compiler-enabled nil state). That is, it's apparently not sensitive to the value of state global 'compiler-enabled. The following partial log...
An attempt to evaluate (ld "base.lisp") in directory books/quicklisp/ fails with the following message. ``` HARD ACL2 ERROR in INCLUDE-RAW: Load of "base-raw.lsp" failed with the following message: Error in...