All Questions
25
questions
0
votes
1
answer
29
views
What is the tag for menhir for coq 8.12 when installing it with opam install -y?
I want to install opam menhir but make the install explicit for coq 8.12 to make my script explicit + robust to installation.
But when I ask it to show me it show the dev tag, which I assume might ...
- 5,961
0
votes
3
answers
307
views
How does one pin/freeze a version of the dependencies of an opam project/package and then install the project with such specified dependencies?
How do we freeze an entire dependency tree/chain from an already working opam install?
I have a bunch of coq projects installed via opam right now. I'd like to figure out what commit they are using ...
- 5,961
1
vote
1
answer
240
views
How do I install ocamlfind first properly before other opam packages without root permissions?
I was trying to install some coq packages with opam but have this hack:
# coq-equations seems to rely on ocamlfind for it's build, but doesn't
# list it as a dependency, so opam sometimes tries to ...
- 5,961
0
votes
1
answer
44
views
How does one make sure that coq project installed correctly when it doesn't seem to appear on opam list?
I tried installing lin-alg-8.10 using the instructions I was told from proverbot's repo using coq 8.10:
# - Create the 8.10 switch
opam switch
opam switch create coq-8.10 4.07.1
eval $(opam env --...
- 5,961
0
votes
1
answer
105
views
How to install the coq 8.14 (or 8.15) package with opam pin when it says it can't find it?
I am on ubuntu. I'm trying to install coq 8.14. I'm sure it must exist. Why doesn't it let me install it? Commands and error msg:
(iit_synthesis) brando9~/proverbot9001 $ opam switch create coq-8.14 4....
- 5,961
0
votes
1
answer
168
views
How does one install a opam coq package that has been successfully install previously?
I know this has been installed before becuase the proverbot9001 project has used it before. So how do I go about finding what exactly is the issue in my set up that doesn't let me install it? Any ...
- 5,961
6
votes
0
answers
160
views
How does one automatically make a `COQ_PROJ.opam` install script automatically from a Coq Project/Package?
I have a very long list of coq projects I want to automatically install with opam pin/install. I'd like to install them with opam because I am using this python tool (PyCoq) that uses opam pin/install....
- 5,961
2
votes
1
answer
494
views
redundant eval $(opam env) needed in Dockerfile [duplicate]
I successfully installed coqc with Dockerfile. Why do I need to run eval $(opam env) again when I execute the docker?
##############
# #
# image name #
# #
##############
FROM ...
- 6,760
2
votes
1
answer
406
views
Adding an old version of Ocaml to Opam
I am trying to install Coq version 8.10.2 using Opam and from this output, I assume Coq 8.10.2 needs an ocaml compiler with version < 4.10
Missing dependency:
- (invariant) -> coq = 8.10.2 -&...
2
votes
1
answer
601
views
Configure OPAM switch for installation of Coq packages
Since OPAM 2.0, after installation one is required to create/select a "switch" before installing packages. If all I'm using OPAM for is Coq packages, what should I use as my switch?
- 6,498
0
votes
0
answers
279
views
Installing library for Coq via Opam on Windows
I'm know nothing in programming. During the installation via Opam library Math Classes in Coq i received an ERROR. I don't know what to do, no idea. The same ERROR occurs when i try to install Bignums ...
- 1
4
votes
1
answer
817
views
How to change Coq Version in Proof General?
I have some code that only compiles coq code in Coq 8.09.0 . The version that I normally use is the most up-to-date version now which is Coq 8.11.0. I was able to create a new environment using opam ...
- 473
2
votes
1
answer
267
views
coq 8.11.0 incompatible with ocaml 4.10?
I am installing coq with opam as per these instructions and have gotten the error message
`No solution for coq: The following dependencies couldn't be met:
- coq → ocaml < 4.10
...
- 437
2
votes
2
answers
99
views
QuickChick "Error: Could not compile mli file"
I successfully installed coq 8.9.1 and coq-quickchick 1.1.0 with opam 2.0.4 and I'm programming on emacs 26.1.
However, when running a QuickChick command I received the following error:
Error: ...
0
votes
2
answers
3k
views
How to upgrade Ocaml to the latest version to support QuickChick in Coq?
When I installed QuickChick from opam, I obtained:
The following dependencies couldn't be met:
coq-quickchick → ocaml >= 4.04.0
base of this switch (use --unlock-base to force)
How should I ...
- 1,969