copilot
copilot copied to clipboard
`copilot-theorem`: `Copilot.Theorem.Prover.Z3` is dead code
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
| ^^^^^^^^^^^^^^^^^^^^^^^^^^