search

impermeable / coq-waterproof

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
https://impermeable.github.io/
GNU Lesser General Public License v3.0
29 stars 9 forks source link

Problem installing using opam #40

Closed jnarboux closed 8 months ago

jnarboux commented 10 months ago

I did: opam install coq.8.17.0

git clone https://github.com/impermeable/coq-waterproof.git && cd coq-waterproof opam install .

I get: coq-waterproof is now pinned to git+file:///adhome/n/na/narboux/coq-waterproof#main (version 2.1.0+8.17)

Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting

jim-portegies commented 10 months ago

What is the version of the OCaml compiler?

jim-portegies commented 10 months ago

What might also work is to, instead of performing opam install ., install by

dune build -p coq-waterproof
dune install -p coq-waterproof
jnarboux commented 9 months ago

I am on (university server), Debian 11, ocaml 4.11.1., opam 2.0.8 I tried compiling using dune and it fails (see below). I tried compiling using opam changing the constraint on ocaml version, dune compilation fails with similar errors. You really need ocaml 4.14.1 ?

Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -rectypes -w -27 -g -I src/.waterproof.objs/byte -I src/.waterproof.objs/native -I /adhome/n/na/narboux/.opam/default/lib/coq-core/boot -I /adhome/n/na/narboux/.opam/default/lib/coq-core/clib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/config -I /adhome/n/na/narboux/.opam/default/lib/coq-core/coqworkmgrapi -I /adhome/n/na/narboux/.opam/default/lib/coq-core/engine -I /adhome/n/na/narboux/.opam/default/lib/coq-core/gramlib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/interp -I /adhome/n/na/narboux/.opam/default/lib/coq-core/kernel -I /adhome/n/na/narboux/.opam/default/lib/coq-core/lib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/library -I /adhome/n/na/narboux/.opam/default/lib/coq-core/parsing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq-core/pretyping -I /adhome/n/na/narboux/.opam/default/lib/coq-core/printing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/proofs -I /adhome/n/na/narboux/.opam/default/lib/coq-core/stm -I /adhome/n/na/narboux/.opam/default/lib/coq-core/sysinit -I /adhome/n/na/narboux/.opam/default/lib/coq-core/tactics -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vernac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vm -I /adhome/n/na/narboux/.opam/default/lib/findlib -I /adhome/n/na/narboux/.opam/default/lib/zarith -I /usr/lib/ocaml/threads -intf-suffix .ml -no-alias-deps -open Waterproof -o src/.waterproof.objs/native/waterproofProofutils.cmx -c -impl src/proofutils.ml) File "src/proofutils.ml", line 1: Error: The implementation src/proofutils.ml does not match the interface src/.waterproof.objs/byte/waterproofProofutils.cmi: ... In module StringMap: The value to_rev_seq' is required but not provided File "src/proofutils.mli", line 91, characters 2-43: Expected declaration (cd _build/default && /usr/bin/ocamlc.opt -w -40 -rectypes -w -27 -g -bin-annot -I src/.waterproof.objs/byte -I /adhome/n/na/narboux/.opam/default/lib/coq-core/boot -I /adhome/n/na/narboux/.opam/default/lib/coq-core/clib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/config -I /adhome/n/na/narboux/.opam/default/lib/coq-core/coqworkmgrapi -I /adhome/n/na/narboux/.opam/default/lib/coq-core/engine -I /adhome/n/na/narboux/.opam/default/lib/coq-core/gramlib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/interp -I /adhome/n/na/narboux/.opam/default/lib/coq-core/kernel -I /adhome/n/na/narboux/.opam/default/lib/coq-core/lib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/library -I /adhome/n/na/narboux/.opam/default/lib/coq-core/parsing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq-core/pretyping -I /adhome/n/na/narboux/.opam/default/lib/coq-core/printing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/proofs -I /adhome/n/na/narboux/.opam/default/lib/coq-core/stm -I /adhome/n/na/narboux/.opam/default/lib/coq-core/sysinit -I /adhome/n/na/narboux/.opam/default/lib/coq-core/tactics -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vernac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vm -I /adhome/n/na/narboux/.opam/default/lib/findlib -I /adhome/n/na/narboux/.opam/default/lib/zarith -I /usr/lib/ocaml/threads -intf-suffix .ml -no-alias-deps -open Waterproof -o src/.waterproof.objs/byte/waterproof__Proofutils.cmo -c -impl src/proofutils.ml) File "src/proofutils.ml", line 1: Error: The implementation src/proofutils.ml does not match the interface src/.waterproof.objs/byte/waterproof__Proofutils.cmi: ... In module StringMap: The valueto_rev_seq' is required but not provided File "src/proofutils.mli", line 91, characters 2-43: Expected declaration (cd _build/default/tests && /adhome/n/na/narboux/.opam/default/bin/coqdep -I /adhome/n/na/narboux/.opam/default/lib/coq-core/boot -I /adhome/n/na/narboux/.opam/default/lib/coq-core/clib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/config -I /adhome/n/na/narboux/.opam/default/lib/coq-core/coqworkmgrapi -I /adhome/n/na/narboux/.opam/default/lib/coq-core/engine -I /adhome/n/na/narboux/.opam/default/lib/coq-core/gramlib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/interp -I /adhome/n/na/narboux/.opam/default/lib/coq-core/kernel -I /adhome/n/na/narboux/.opam/default/lib/coq-core/lib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/library -I /adhome/n/na/narboux/.opam/default/lib/coq-core/parsing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq-core/pretyping -I /adhome/n/na/narboux/.opam/default/lib/coq-core/printing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/proofs -I /adhome/n/na/narboux/.opam/default/lib/coq-core/stm -I /adhome/n/na/narboux/.opam/default/lib/coq-core/sysinit -I /adhome/n/na/narboux/.opam/default/lib/coq-core/tactics -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vernac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vm -I /adhome/n/na/narboux/.opam/default/lib/findlib -I /adhome/n/na/narboux/.opam/default/lib/zarith -I /usr/lib/ocaml -I /usr/lib/ocaml/threads -I ../src -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/btauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/cc -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/derive -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/extraction -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/firstorder -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/funind -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/micromega -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/nsatz -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/number_string_notation -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ring -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/rtauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ssreflect -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ssrmatching -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p0 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p1 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p2 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p3 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/zify -R /adhome/n/na/narboux/.opam/default/lib/coq/theories Coq -Q ../theories Waterproof -R . __WaterproofTests -dyndep opt -vos util/MessagesToUser.v tactics/Unfold.v tactics/ToShow.v tactics/TakeSuchThat.v tactics/Take.v tactics/Obtain.v tactics/ItSuffices.v tactics/ItHolds.v tactics/Induction.v tactics/Either.v tactics/Define.v tactics/Contradiction.v tactics/Conclusion.v tactics/Claims.v tactics/Choose.v tactics/BothStatements.v tactics/BothDirections.v tactics/Because.v tactics/Assume.v libs/Analysis/StrongInductionIndexSequence.v libs/Negation.v chains/Manipulation.v chains/Inequalities.v automation/databases/RealsAndIntegers.v automation/databases/Integers.v automation/databases/Empty.v automation/databases/Decidability.v automation/databases/Core.v automation/Shield.v automation/Chains.v) > _build/default/tests/.__WaterproofTests.theory.d *** Warning: ltac_plugin.cmxs already found in /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac (discarding /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac/ltac_plugin.cmxs)

*** Warning: ltac2_plugin.cmxs already found in /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 (discarding /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac2/ltac2_plugin.cmxs)

(cd _build/default/theories && /adhome/n/na/narboux/.opam/default/bin/coqdep -I /adhome/n/na/narboux/.opam/default/lib/coq-core/boot -I /adhome/n/na/narboux/.opam/default/lib/coq-core/clib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/config -I /adhome/n/na/narboux/.opam/default/lib/coq-core/coqworkmgrapi -I /adhome/n/na/narboux/.opam/default/lib/coq-core/engine -I /adhome/n/na/narboux/.opam/default/lib/coq-core/gramlib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/interp -I /adhome/n/na/narboux/.opam/default/lib/coq-core/kernel -I /adhome/n/na/narboux/.opam/default/lib/coq-core/lib -I /adhome/n/na/narboux/.opam/default/lib/coq-core/library -I /adhome/n/na/narboux/.opam/default/lib/coq-core/parsing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq-core/pretyping -I /adhome/n/na/narboux/.opam/default/lib/coq-core/printing -I /adhome/n/na/narboux/.opam/default/lib/coq-core/proofs -I /adhome/n/na/narboux/.opam/default/lib/coq-core/stm -I /adhome/n/na/narboux/.opam/default/lib/coq-core/sysinit -I /adhome/n/na/narboux/.opam/default/lib/coq-core/tactics -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vernac -I /adhome/n/na/narboux/.opam/default/lib/coq-core/vm -I /adhome/n/na/narboux/.opam/default/lib/findlib -I /adhome/n/na/narboux/.opam/default/lib/zarith -I /usr/lib/ocaml -I /usr/lib/ocaml/threads -I ../src -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/btauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/cc -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/derive -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/extraction -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/firstorder -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/funind -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac2 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/micromega -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/nsatz -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/number_string_notation -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ring -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/rtauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ssreflect -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ssrmatching -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tauto -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p0 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p1 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p2 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/tutorial/p3 -I /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/zify -R /adhome/n/na/narboux/.opam/default/lib/coq/theories Coq -R . Waterproof -dyndep opt -vos Util/Since.v Util/MessagesToUser.v Util/Init.v Util/Hypothesis.v Util/Goals.v Util/Constr.v Util/Assertions.v Tactics/Unfold.v Tactics/ToShow.v Tactics/Take.v Tactics/Obtain.v Tactics/ItSuffices.v Tactics/ItHolds.v Tactics/Induction.v Tactics/Help.v Tactics/Either.v Tactics/Define.v Tactics/Contradiction.v Tactics/Conclusion.v Tactics/Claims.v Tactics/Choose.v Tactics/BothStatements.v Tactics/BothDirections.v Tactics/Because.v Tactics/Assume.v Notations/Sets.v Notations/Reals.v Notations/Common.v Libs/Logic/InformativeEpsilon.v Libs/Logic/ConstructiveLogic.v Libs/Analysis/SupAndInf.v Libs/Analysis/SubsequencesMetric.v Libs/Analysis/Subsequences.v Libs/Analysis/StrongInductionIndexSequence.v Libs/Analysis/Series.v Libs/Analysis/SequentialAccumulationPoints.v Libs/Analysis/SequencesMetric.v Libs/Analysis/Sequences.v Libs/Analysis/OpenAndClosed.v Libs/Analysis/MetricSpaces.v Libs/Analysis/LimsupLiminfBolzano.v Libs/Analysis/ContinuityDomainR.v Libs/Analysis/ContinuityDomainNat.v Libs/Reals.v Libs/Negation.v Libs/Analysis.v Chains/Manipulation.v Chains/Inequalities.v Automation/Hints.v Automation/Framework.v Waterprove.v Waterproof.v Version.v Tactics.v Notations.v Chains.v Automation.v) > _build/default/theories/.Waterproof.theory.d *** Warning: ltac_plugin.cmxs already found in /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac (discarding /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac/ltac_plugin.cmxs)

*** Warning: ltac2_plugin.cmxs already found in /adhome/n/na/narboux/.opam/default/lib/coq-core/plugins/ltac2 (discarding /adhome/n/na/narboux/.opam/default/lib/coq/../coq-core/plugins/ltac2/ltac2_plugin.cmxs)

jim-portegies commented 8 months ago

With PR #45 , installation should now be possible with Ocaml compilers >= 4.09.1. This is incorporated in versions 2.1.1+8.17 and 2.1.1+8.18