(Sorry, this is probably a very naive question...)
I need to build the coqprime library against a development branch of coq. This library itself relies on coq-bignums.
I usually just rely on the
COQBIN environment variable, set as
What would be an easy way to install
coq-bignums and tell
coqprime that the stdlib is to be found in the repo while coq-bignums is somewhere else?
A solution (maybe not the easiest) is to use OPAM, create a specific switch (I usually call it
coqdev), install your Coq branch in that switch (for instance following the instructions in coq-core.opam and coq-stdlib.opam), make OPAM believe Coq is installed with
opam install --fake coq.dev (requires the OPAM repo coq-core-dev), then you can
opam install coq-bignums (requires the coq-extra-dev repo). You can also skip the last two OPAM steps and manually instal bignums (
git clone https://github.com/coq/bignums,
Thank you very much, I will try this out.
make install in bignums it should go in the user-contrib of <coq_local_repo>/_build/install so no need to do anything more
you can also
make ci-coqprime from <coq_local_repo>, it will build bignums then coqprime in <coq_local_repo>/_build_ci
wow, that looks powerful!
As we're at it, any advice on the opam switch for dev? Should I pin ocaml to some version?
I use 4.14 for dev (except when bisecting over older versions which don't support it, then I have a few other switches with older ocamls)
I don't know much opam so I don't know what you mean by pinning ocaml
It allows to specify a version for a package if I'm not mistaken (can't say I know much about opam too).
but then... I have probably said something stupid because the opam switch is already attached to some version of ocaml?
The ocaml compiler is indeed pinned in the switch... (ignoring the ocaml-system compiler, which can be updated externally if you want more compiler excitement)
Most comfortable setup is to have a composed dune build of Coq with coq-bignums , in this case, everything works "out of the box"
Following @Gaëtan Gilbert's advice, I tried to
make ci-equations but this time it fails with :
File "src/subterm.ml", line 186, characters 54-79: 186 | (Hints.HintsResolveEntry (List.concat constrhints)) in ^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type ('a Typeclasses.hint_info_gen * bool * Hints.hint_term) list but an expression was expected of type (Typeclasses.hint_info * Hints.hnf * Hints.hints_path_atom * Hints.hint_term) list Type 'a Typeclasses.hint_info_gen * bool * Hints.hint_term is not compatible with type Typeclasses.hint_info * Hints.hnf * Hints.hints_path_atom * Hints.hint_term
My version of OCaml is 4.14.1.
are you sure you're on coq master?
Hmm... no, I did it on my branch. Isn't it the purpose though?
Yes, but you should rebase your branch on top of master from time to time, as other pull requests (including overlays for external libraries) might have been merged in the meantime.
I will try to rebase it without notifying the whole world this time then. Sorry for the noise and thank you for your answers
It should just be a matter of doing
git fetch upstream ; git rebase upstream/master (replace
upstream by whatever the name of the upstream remote is, e.g.,
This is solved by rebasing (and recompiling).
Last updated: Dec 05 2023 at 12:01 UTC