Stream: Coq devs & plugin devs

Topic: external libraries and upstream Coq


view this post on Zulip Pierre Rousselin (Sep 12 2023 at 10:14):

(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?

view this post on Zulip 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).

view this post on Zulip Pierre Rousselin (Sep 12 2023 at 10:24):

Thank you very much, I will try this out.

view this post on Zulip 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

view this post on Zulip Pierre Rousselin (Sep 12 2023 at 10:38):

wow, that looks powerful!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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"

view this post on Zulip 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

My version of OCaml is 4.14.1.

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 23:06):

are you sure you're on coq master?

view this post on Zulip Pierre Rousselin (Sep 14 2023 at 04:56):

Hmm... no, I did it on my branch. Isn't it the purpose though?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Pierre Rousselin (Sep 14 2023 at 05:45):

This is solved by rebasing (and recompiling).


Last updated: Jun 13 2024 at 05:01 UTC