copilot-theorem: Examples do not compile

Description

Some example programs in the copilot-theorem/example subdirectory have bitrotted, as they depend on a Copilot.Theorem.Prover.Z3 module that is no longer included in copilot-theorem.cabal (as of 6a67d89). Attempting to build any of these examples results in compilation failures.

Type

Bug: Example programs fail to compile.

Additional context

Copilot.Theorem.Prover.Z3 was an early, SMT solver–based approach for proving properties about Copilot specifications. The copilot-theorem library has largely replaced Copilot.Theorem.Prover.Z3 will different APIs, such as those offered by Copilot.Theorem.Prover.SMT and Copilot.Theorem.What4. Of the latter two, the API in Copilot.Theorem.Prover.SMT is closest to what Copilot.Theorem.Prover.Z3 offered.

Requester

Ryan Scott (Galois)

Method to check presence of bug

First, build the copilot libraries, using a method such as the following:

$ cabal build copilot --write-ghc-environment-files=always

Then invoke ghc on one of the files in the copilot-theorem/examples subdirectory that import Copilot.Theorem.Prover.Z3. The bug manifests as a GHC compilation error, such as in the following example:

$ ghc copilot-theorem/examples/BoyerMoore.hs
Loaded package environment from /Users/rscott/Documents/Hacking/Haskell/copilot/.ghc.environment.aarch64-darwin-9.4.8
[1 of 1] Compiling BoyerMoore       ( copilot-theorem/examples/BoyerMoore.hs, copilot-theorem/examples/BoyerMoore.o )

copilot-theorem/examples/BoyerMoore.hs:8:1: error:
    Could not find module ‘Copilot.Theorem.Prover.Z3’
    Perhaps you meant
      Copilot.Theorem.Prover.SMT (from copilot-theorem-4.6)
      Copilot.Theorem.Prover.SMT (needs flag -package-id copilot-theorem-4.3)
      Copilot.Theorem.Prover.SMT (needs flag -package-id copilot-theorem-4.3)
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
  |
8 | import Copilot.Theorem.Prover.Z3
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expected result

Invoking ghc on any of the examples in the copilot-theorem/examples subdirectory should succeed.

Desired result

Invoking ghc on any of the examples in the copilot-theorem/examples subdirectory should succeed.

Proposed solution

Modify the code in each of the examples in copilot-theorem/examples to import from Copilot.Theorem.Prover.SMT instead of Copilot.Theorem.Prover.Z3, making adjustments as needed to adapt to the slightly different API in Copilot.Theorem.Prover.SMT.

Further notes

None.

I could do this if you want to assign it to me.

Change Manager: modified description to qualify which examples fail, and the nature of the changes proposed.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@chathhorn-galois

Technical Lead: Issue scheduled for fixing in Copilot 4.7.1.

Fix assigned to: @chathhorn-galois .

Implementor: Solution implemented, review requested.

copilot-theorem: Update examples to compile with copilot-theorem >= 3…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

copilot-theorem: Update examples to compile with copilot-theorem >= 3…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

copilot-theorem: Update examples to compile with copilot-theorem >= 3…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

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/278077300

The solution proposed produces the expected result. Details:
The following Dockerfile checks that all the examples that used the removed module Z3 can now be compiled, after which it prints the message "Success":

FROM ubuntu:jammy

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

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -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 ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/BoyerMoore.hs \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/Grey.hs \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/Incr.hs \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/SerialBoyerMoore.hs \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/SphericalWCV.hs \
  && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/WCV.hs \
  && echo "Success"

Command (substitute variables based on new path after merge):

$ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=579b124a56146f563e620ca9df5d9b1c70640a84 copilot-verify-692

Implementation is documented. Details:
No updates needed; the changes are minimal maintenance updates to examples.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
The change is to the examples.
Required version bumps are evaluated. Details:
Bump not required; change affects examples only.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-fix-theorem-examples-z3'. Close Copilot-Languag…

Navigation Menu

Repository navigation

`copilot-theorem`: Examples do not compile #692

7 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Examples do not compile #692

Description

Activity

chathhorn-galois commented on Nov 20, 2025

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Mar 10, 2026

7 remaining items

chathhorn-galois commented on Mar 31, 2026

ivanperez-keera commented on May 7, 2026

ivanperez-keera commented on May 7, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: Examples do not compile #692