`copilot-theorem`: Introduce testing infrastructure for `Copilot.Theorem.What4`. Refs #474.

[ivanperez-keera]

Introduce minimal testing infrastructure for copilot-theorem, focusing only on Copilot.Theorem.What4, Z3, and a few sample properties, as prescribed in the solution proposed for #474.

[ivanperez-keera]

Change Manager: Changes requested:

• Rebase on top of the current master (changes have been merged since this was filed).
• Change the order of commits to make the changes to the change logs last.
• The text "update GHC version in both as needed." in the CI script should say "keep GHC version numbers in both places in sync".

[ivanperez-keera]

Implementor: Changes implemented. Review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • [X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/267963797

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile checks that copilot-theorem's tests can be executed, in which case it prints the message Success:

    
    --- Dockerfile-verify-474
    FROM ubuntu:focal

  RUN apt-get update

  RUN apt-get install --yes libz-dev RUN apt-get install --yes git

  RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

  RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ RUN apt-get install --yes curl RUN apt-get install --yes gcc make libgmp3-dev g++

  SHELL ["/bin/bash", "-c"]

  RUN ghcup install ghc 9.4.7 RUN ghcup install cabal 3.8 RUN ghcup set ghc 9.4.7 RUN cabal update

  RUN apt-get install --yes z3

  CMD git clone $REPO && \ cd $NAME && \ git checkout $COMMIT && \ cd copilot-theorem && \ cabal test copilot-theorem:unit-tests && \ echo Success

  Command (adjust repo as necessary):

  $ docker run -e "REPO=https://github.com/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=e717ae2620bfd7cf8e2339addb74eb2c7e1f64ea" -it copilot-verify-474

• [X] Implementation is documented. Details: Change to tests. No changes to the public documentation are needed. Comments are added to all new modules and functions.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump not needed. This is a change to the tests.