Building books with ABC and Ipasir - acl2/acl2 GitHub Wiki

Adapted from a thread on the acl2-help mailing list.

Alessandro wrote:

I’d like to certify all the ACL2 community books when I run regression tests — for “plain” ACL2, in particular not ACL2(r) at this moment.

My current make output shows

ACL2_HAS_HONS     := 1
ACL2_HAS_ANSI     := 1
ACL2_HAS_PARALLEL := 
ACL2_HAS_REALS    := 
ACL2_COMP_EXT     := dx64fsl
ACL2_HOST_LISP    := CCL
OS_HAS_ABC        := 
OS_HAS_GLUCOSE    := 1
OS_HAS_IPASIR     := 
OS_HAS_SMTLINK    := 1
USE_QUICKLISP     := 1

which suggests that I should install ABC and IPASIR, which I’m not familiar with.

Is ABC at https://github.com/berkeley-abc/abc? Is there any special advice about installing it, other than following the instructions on that site? (I’m thinking of things like the fact that only the older version of Glucose works with the ACL2 books.) I searched a bit in the ACL2 manual but did not see anything.

The ACL2 manual points to https://github.com/biotomas/ipasir for IPASIR. Again, any special advice about installing it?

Finally, is this all that’s needed to certify all (plain) ACL2 community books, or is there anything not shown by the output above?

Sol wrote:

For ABC, yes, the berkeley-abc github page is where to start. I don't know of any problems with the build, and the standard executable is what you need with ACL2 (just put it in your path).

For ipasir, there's a little more to do. First, there are a number of choices for a SAT library that implements the interface. You can get a few of them from the SAT competition website, https://baldur.iti.kit.edu/sat-competition-2017/solvers/incremental/ -- but I basically just use glucose. There are others you could try, but some others have restrictive licenses and I also recall finding that at least one didn't implement the whole interface, but just enough to compete in the SAT competition -- but maybe the situation has improved since then. The other part is that you need to change the build a bit to build a shared library instead of a static library, so that you can dynamically load it into your Lisp. I've only done this on Linux. I've attached a patch to apply to the makefile for this. Probably it's about the same on a Mac modulo the filename extensions; I don't know about Windows. I think you also need a relatively recent gcc version, maybe 6.0+ or so. Once you have the library built you just need to set the environment variable IPASIR_SHARED_LIBRARY to the path to that file.

Rob wrote:

In addition to Sol's advice, I just wanted to add that it is a little different on Mac for shared libraries (in case anyone wants to use ipasir on mac and has run into issues). I added the following line to the makefile and pointed IPASIR_SHARED_LIBRARY to the pointed to file and everything has worked for me:

libipasir$(SIG).dylib: libipasir$(SIG).a ipasir$(NAME)glue.o
	$(CXX) $(LDFLAGS) -o libipasir$(SIG).dylib -dynamiclib -current_version 4.0 -compatibility_version 4.0 ipasir$(NAME)glue.o $(DIR)/build/release/lib/lib$(NAME).a

The "-dynamiclib" is needed to tell LD to build a shared library in the right format for dylib and the version crud is (I think) required to get dylib to accept the loading of the library on Mac OS.

The patch from Sol is below:

26c26,27
< TARGET=libipasir$(SIG).a
---
> TARGET=libipasir$(SIG).so
> TARGET_A=libipasir$(SIG).a
32c33,34
< CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3
---
> CXXFLAGS=-std=c++11 -Wall -DNDEBUG -O3 -fPIC
> export CXXFLAGS
41c43
< 	rm -f *.o *.a
---
> 	rm -f *.o *.a *.so; cd glucose-4; make clean
62,63c64,68
< 	cp $(DIR)/build/release/lib/lib$(NAME).a $(TARGET)
< 	ar r $(TARGET) ipasir$(NAME)glue.o
---
> 	cp $(DIR)/build/release/lib/lib$(NAME).a $(TARGET_A)
> 	ar r $(TARGET_A) ipasir$(NAME)glue.o
> 
> libipasir$(SIG).so: libipasir$(SIG).a ipasir$(NAME)glue.o
> 	$(CXX) $(LDFLAGS) -o libipasir$(SIG).so -shared -Wl,-soname,libipasir$(SIG).so ipasir$(NAME)glue.o $(DIR)/build/release/lib/lib$(NAME).a
70c75
< 	$(CXX) -g  -std=c++11 $(CXXLAGS) \
---
> 	$(CXX) -std=c++11 $(CXXFLAGS) \