MattKaufmann

A new trace$ printing option may be possible. In the meantime, the following from :DOC trace$ may be helpful, to overcome ACL2's hijacking of trace and untrace. If you need...

@bendyarm In principle, using option :evisc-tuple :print does what you want; see :DOC trace$. It doesn't quite do what I'd expect though; I plan to fix that tomorrow.

@bendyarm I've improved trace$ option `:evisc-tuple :print` as per the following from :DOC note-8-6. ``` The [trace$] option :evisc-tuple :print, which continues to use raw Lisp printing, has undergone the...

Regarding: > Right now it's effectively just dead code. OTOH, we > already have a bunch of "dead code" that's mostly only > included for the sake of preserving artifacts,...

P.S. To clarify, by "I don't mind moving some [books]", I meant that I don't mind if someone ELSE wants to do that (again, preserving all certifiability). I shouldn't pretend...

I don't mind leaving this issue open, but I suspect that nobody will ever deal with it. Is there a way to mark such issues as "dormant" or such, so...

Ugh -- too much to remember! Anyhow, I'll try to avoid further discussion on this issue, but it's very important to me to be able to build the manual easily....

Hi, David -- I seem to remember several months ago that after I noted that SBCL seems faster than CCL in the regression (also in some other tests I've un),...

David, did you try my suggestion of something like this in your saved_acl2? --dynamic-space-size 240000 --control-stack-size 640 Or, if you can tell me how to reproduce the problem, I could...

Hi, David -- Ah -- OK, right, my suggestion probably wouldn't help. (I'm not 100% sure of that, though -- for all I know SBCL got into a weird stack-overflow...