`copilot-libraries`: Introduce testing infrastructure

[ivanperez-keera]

Description

As part of the requirements for Class D (NPR7150.2C), we need unit tests for all of copilot.

A natural next step is to introduce the testing infrastructure for copilot-libraries.

Type

• Management: conformance with new requirement.

Additional context

None.

Requester

• Ivan Perez

Method to check presence of bug

Not applicable (not a bug).

Expected result

The library copilot-libraries includes tests for some of the existing modules. Introducing (some classes of) errors in the implementation of copilot-libraries makes the tests detect those errors.

Desired result

The library copilot-libraries includes tests for some of the existing modules. Introducing (some classes of) errors in the implementation of copilot-libraries makes the tests detect those errors.

Proposed solution

Add tests for copilot-libraries that tests basic properties of some of the existing modules.

Further notes

Due to the magnitude of this change, we decide to simplify the issue by merely introducing the infrastructure. We leave it to a future issue to have a more comprehensive list of properties that covers all modules.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 3.18.

Fix assigned to: @ivanperez-keera .

[ivanperez-keera]

Implementor: Solution 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/268024914

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

    
    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-libraries && \ cabal test copilot-libraries:unit-tests && \ echo Success

  Command (adjust repo as necessary):

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

• [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.

[ivanperez-keera]

Change Manager: Implementation ready to be merged.