Improve integration of SULFA into the community books

[kini]

Right now, SULFA seems like kind of a standalone thing. It requires one of two particular SAT solvers, minisat or zchaff, neither of which has been actively developed in the last decade. Plus, the SAT solver needs to be installed into a particular, but platform-dependent, location in the ACL2 repository; just being in the user's $PATH is not good enough. So leeroy's regression runs always skip building SULFA, and I suspect most other people's regression runs do as well.

It would be nice if SULFA could be updated to at least be able to use minisat or zchaff from $PATH, to make it easier to build during the regression (i.e. some Linux distros have easy-to-install packages for minisat).

Even better would be if SULFA could be updated to use the satlink library somehow, since plenty of other community books now use that framework for calling SAT solvers in a pluggable fashion. I imagine that unless SULFA is using some idiosyncratic C API of minisat/zchaff, it should be compatible with other SAT solvers such as glucose via the standard DIMACS format.

[ragerdl]

Agreed that it'd be nice to clean this up. 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, so I guess it's fine. It's not in a top-level books directory, so that's good.

FWIW, I doubt I'll ever add minisat/zchaff to leeroy2 just for the sake of building the sulfa books.

I kind of wish there was an archive directory. workshops is definitely an archive directory. projects is kind of an archive directory, but stuff that's still being maintained and could be useful is in there (e.g., Julian and Team's avr-isa model could be useful). Knowing almost nothing about SULFA, my guess is that SULFA helped lay the groundwork for Sol's work, and at this point, Sol's work supersedes it. So, either moving it to an archive or rming it could be appropriate.

If I were being centered around my perspective, I'd think data-structures should also go in archive, since std has what I consider to be better approaches. However, I'm guessing some folks still use data-structures, and it's important to preserve their functionality. My concern is that if a new user looks at the books directory to try to figure out what to use, data-structures is going to seem more appealing when instead they need to look in std. Also, it's just clutter (again, from my perspective). OTOH :doc data-structures has a nice intro to std, and maybe that's all that matters.

[MattKaufmann]

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, so I guess
it's fine.

I'm very happy to have the community books as support for
testing ACL2 (and I think J is too), including books that
aren't used elsewhere. As for the SULFA books, I test those
regularly, in fact as recently as this past Thursday --
twice that day, in fact (once with ACL2(p) on SBCL, and once
with ACL2 on CCL).

So I request that community books not be removed from the
GitHub repository (with obvious exception, e.g., books that
nobody will certify, books removed by their authors, books
that are superseded or are obsolete stubs, etc.). I don't
mind moving some to a books/archive/ directory if someone
wants to do that reorganization while preserving
certifiability of existing books (could be a lot of work),
though I think a better way to help new users would be to
write and maintain a suitable :doc topic (I'm not
volunteering though).

[MattKaufmann]

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 though that I think that's it's worth anyone's trouble. ;)

[kini]

As for the SULFA books, I test those
regularly, in fact as recently as this past Thursday --
twice that day, in fact (once with ACL2(p) on SBCL, and once
with ACL2 on CCL).

Thanks Matt, it's good to know that someone is testing SULFA, at least :) I guess I should have realized that based on the fact that there are @useless-runes.lsp files for those books in the repository.

[acoglio]

@kini Do you think that this Issue can be closed now?

[kini]

I don't think anything has changed regarding SULFA since I opened the ticket, has it? If that's the case, then I'd say this issue should remain open.

[MattKaufmann]

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 that people like @acoglio don't waste time looking through such issues for ones that can be closed?

[kini]

I've now added a couple labels ("wishlist" and "help wanted") which I guess are intended for that purpose.

[acoglio]

@MattKaufmann Yes, one can define labels, such as the ones added by @kini, including priority labels.

It's no bother for me to look through these issues, and takes me little time. It's really the first time I look through most of them, and even if we can close or clarify a few of them, I think it's worth it.