Installation instructions
=========================

CUT is currently developed and maintained only for Linux. We recommend to install
and use it with Docker, as detailed below, but you also can try a manual
installation. Both methods share the following first steps:

1. If it is not done yet, download the most recent version cut.XXX.zip or cut.XXX.tar.gz of CUT at 
   [http://members.femto-st.fr/alain-giorgetti/en/coq-unit-testing](http://members.femto-st.fr/alain-giorgetti/en/coq-unit-testing)
   and extract the archive:

        unzip cut*.zip

   or

        tar xvf cut*.tar.gz

2. Move to the extracted folder:

        cd cut

CUT with Docker
---------------

3. If Docker is not installed, follow the instructions at
   [https://docs.docker.com/install/linux/docker-ce/ubuntu/](https://docs.docker.com/install/linux/docker-ce/ubuntu/)
   and 
   [https://docs.docker.com/engine/installation/linux/linux-postinstall/](https://docs.docker.com/engine/installation/linux/linux-postinstall/)
   to install Docker and run Docker commands without using sudo.

4. Build the Docker image (all Docker commands are encapsulated in Makefile entries):

        make build

   The Docker image will contain compatible releases of all the tools required
   for CUT.

   Warnings: The Docker image is a large file, its construction can be very long.
   A network connection is required. If you already have a Docker image with this
   name, either remove it or change the image name in Makefile.

5. Create the container:

        make ctr

   Warning: If you already have a Docker container with the same name, either
   remove it or change the container name in Makefile.

6. Start an interactive session in the container and move to the cut folder in it:

        make start
        cd cut

7. See the entries in the Makefile in the folders examples/, prolog/, why3/ and 
   OCaml/. They encapsulate various possible testing and proving actions that you
   can experiment. For instance, check the Coq proofs of the first case study as follows:

        cd examples/coq
        make compile

   or run the second case study as follows:

         cd examples/isomorphisms
         make

   or run or replay Why3 proofs as follows:

        cd why3/enum
        make prove

   Warning: Some of these folders (examples/, why3/, etc.) are mounted in the container.
   So, any change in them in the container is actually done in their local version.

8. Finally, quit the container:

        exit

Successfully tested in October 2020 under Linux Ubuntu 18.04, with Docker 19.03.12.

Manual installation
-------------------

If you already have installed most of the tools among Why3, Alt-Ergo, CVC3, CVC4,
Z3 and Coq, under Linux, you can try to install CUT manually, but we do provide
help for manual installations.

3. Complete your installation by running commands similar to the commands in Dockerfile.

4. In the folder cut/, run the command

        cd examples; make config; cd ..

   It displays something like:
      
        echo "-I /usr/lib/ocaml/zarith -I /usr/local/lib/ocaml/4.02.3/why3"
        \-I /usr/lib/ocaml/zarith -I /usr/local/lib/ocaml/4.02.3/why3

5. The tool relies on an extension of QuickChick for Coq 8.10.2 stored in the folder
   QuickChick-master/. It has to be adapted and compiled for your system as follows:

   - Edit the file QuickChick-master/src/quickChick.ml4.

   - Search for the lines

         let ocamlopt3 = "ocamlopt -I /home/opam/opam-coq.8.10.2/ocaml-base-compiler.4.08.1/lib/zarith -I /home/opam/opam-coq.8.10.2/ocaml-base-compiler.4.08.1/lib/why3 zarith.cmxa why3.cmxa"
         let ocamlc3 = "ocamlc -I /home/opam/opam-coq.8.10.2/ocaml-base-compiler.4.08.1/lib/zarith -I /home/opam/opam-coq.8.10.2/ocaml-base-compiler.4.08.1/lib/why3"

   - Replace in both lines the substring 

         "-I .. -I .."

   with the substring echoed at step 4.

   - Then move to the folder QuickChick-master/ and run the following commands:

        make clean
        make
        make install (possibly, as sudoer)
        make tests (optional)

   Our extension of QuickChick is now installed on your system.

6. If your installation succeeds, follow step 7 of 'CUT with Docker' to play with
   the tool.
