Installing ACL2s on NixOS

This repository contains instructions for building acl2s on NixOS.

1. Clone this repository. Make sure that you have nix flakes enabled. Execute all the following shell blocks from the root of this repository.
2. Clone the following repositories

   git clone https://gitlab.com/acl2s/external-tool-support/scripts ./scripts
   git clone https://github.com/acl2/acl2 ./acl2
   git clone https://gitlab.com/acl2s/proof-checking/hand-proof-checker ./hand-proof-checker
       

3. In nix develop, run to build acl2 and acl2s

   ./scripts/clean-gen-acl2-acl2s.sh
       

4. Make sure symlinks in ./bin fire. If not,

   cd bin
   ln -s ../acl2/saved_acl2 acl2
   ln -s ../acl2s acl2s
   ln -s ../hand-proof-checker/check-file.sh check-proof
   ln -s ../acl2/books/build/cert.pl cert.pl
       

5. In nix develop, build the hand proof checker CLI (requires docker and dockerd to be running)

   cd hand-proof-checker/
   make proof-checker-cli # makes the docker image
   make # builds it locally