copilot icon indicating copy to clipboard operation
copilot copied to clipboard

`copilot-theorem`: `Copilot.Theorem.Prover.Z3` is dead code

Open RyanGlScott opened this issue 6 months ago • 0 comments

The Copilot.Theorem.Prover.Z3 module has not included in the copilot-theorem.cabal file ever since https://github.com/Copilot-Language/copilot/commit/6a67d89ee42ffa0718e844e03a4e7f34d2a88801, and as such, it is dead code. Moreover, the code has bitrotted since then, as trying to compile it with a modern version of copilot-theorem fails:

src/Copilot/Theorem/Prover/Z3.hs:27:1: error:
    Could not find module ‘Data.Unit’
    Perhaps you meant
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
      Data.Bit (needs flag -package-id bitvec-1.1.5.0)
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
27 | import Data.Unit (Unit(..))
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:37:1: error:
    Could not find module ‘Language.SMTLib2’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
37 | import Language.SMTLib2
   | ^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:38:1: error:
    Could not find module ‘Language.SMTLib2.Pipe’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
38 | import Language.SMTLib2.Pipe
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:39:1: error:
    Could not find module ‘Language.SMTLib2.Connection’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
39 | import Language.SMTLib2.Connection
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:40:1: error:
    Could not find module ‘Language.SMTLib2.Strategy’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
40 | import Language.SMTLib2.Strategy
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:42:1: error:
    Could not find module ‘Language.SMTLib2.Internals’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
42 | import Language.SMTLib2.Internals hiding (Var)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Copilot/Theorem/Prover/Z3.hs:44:1: error:
    Could not load module ‘System.Console.ANSI’
    It is a member of the hidden package ‘ansi-terminal-1.1.2’.
    Perhaps you need to add ‘ansi-terminal’ to the build-depends in your .cabal file.
    It is a member of the hidden package ‘ansi-terminal-1.0.2’.
    Perhaps you need to add ‘ansi-terminal’ to the build-depends in your .cabal file.
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
44 | import System.Console.ANSI
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^

RyanGlScott avatar Jun 27 '25 10:06 RyanGlScott