external libraries and upstream Coq · Coq devs & plugin devs

(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 <coq_local_repo>/_build/install/default/bin.
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?

Pierre Roux (Sep 12 2023 at 10:21):

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, make, make install).

Pierre Rousselin (Sep 12 2023 at 10:24):

Gaëtan Gilbert (Sep 12 2023 at 10:26):

if you 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

Pierre Rousselin (Sep 12 2023 at 10:38):

Pierre Rousselin (Sep 12 2023 at 10:41):

As we're at it, any advice on the opam switch for dev? Should I pin ocaml to some version?

Gaëtan Gilbert (Sep 12 2023 at 10:45):

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

Pierre Rousselin (Sep 12 2023 at 10:50):

It allows to specify a version for a package if I'm not mistaken (can't say I know much about opam too).

Pierre Rousselin (Sep 12 2023 at 10:51):

but then... I have probably said something stupid because the opam switch is already attached to some version of ocaml?

Paolo Giarrusso (Sep 12 2023 at 10:59):

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)

Emilio Jesús Gallego Arias (Sep 12 2023 at 18:08):

Most comfortable setup is to have a composed dune build of Coq with coq-bignums , in this case, everything works "out of the box"

Pierre Rousselin (Sep 13 2023 at 22:09):

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

Gaëtan Gilbert (Sep 13 2023 at 23:06):

Pierre Rousselin (Sep 14 2023 at 04:56):

Guillaume Melquiond (Sep 14 2023 at 05:02):

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.

Pierre Rousselin (Sep 14 2023 at 05:06):

I will try to rebase it without notifying the whole world this time then. Sorry for the noise and thank you for your answers

Guillaume Melquiond (Sep 14 2023 at 05:21):

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., origin).

Stream: Coq devs & plugin devs

Topic: external libraries and upstream Coq

Pierre Rousselin (Sep 12 2023 at 10:14):