`copilot-theorem`: Introduce testing infrastructure about copilot HOT 6 CLOSED

Change Manager: Confirmed that the issue exists.

from copilot.

Technical Lead: Confirmed that the issue should be addressed.

from copilot.

Technical Lead: Issue scheduled for fixing in Copilot 3.18.

Fix assigned to: @ivanperez-keera .

from copilot.

Implementor: Solution implemented, review requested.

from copilot.

Change Manager: Verified that:

• Solution is implemented:

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

  • 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
    

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

from copilot.

Change Manager: Implementation ready to be merged.

from copilot.