Stream: Coq devs & plugin devs

Topic: Installing coq-stdlib with opam


view this post on Zulip Ali Caglayan (Apr 03 2023 at 00:49):

Are people able to install coq-stdlib with opam? I am getting the following:

[ERROR] The compilation of coq-stdlib.8.17.0 failed at "make dunestrap COQ_DUNE_EXTRA_OPT=-split".

#=== ERROR while compiling coq-stdlib.8.17.0 ==================================#
# context     2.1.4 | linux/x86_64 | coq-core.8.17.0 | https://opam.ocaml.org#256625cb
# path        ~/.opam/coq-core.8.17.0/.opam-switch/build/coq-stdlib.8.17.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_DUNE_EXTRA_OPT=-split
# exit-code   2
# env-file    ~/.opam/log/coq-stdlib-672455-587bbe.env
# output-file ~/.opam/log/coq-stdlib-672455-587bbe.out
### output ###
# [...]
# 41 |   (source_tree theories)
# 42 |   (source_tree plugins))
# 43 |  (action
# 44 |   (with-stdout-to %{targets}
# 45 |    (run tools/dune_rule_gen/gen_rules.exe Coq theories %{env:COQ_DUNE_EXTRA_OPT=}))))
# [gen_rules] Fatal error: Invalid_argument("failed to locate Coq plugins in split build mode: coq-
core.plugins.number_string_notation")
# Raised at Coq_dune__Coq_rules.FlagUtil.findlib_plugin_flags in file "tools/dune_rule_gen/coq_rule
s.ml", line 56, characters 6-89
# Called from Coq_dune__Coq_rules.Context.make in file "tools/dune_rule_gen/coq_rules.ml", line 171
, characters 25-63
# Called from Dune__exe__Gen_rules.main in file "tools/dune_rule_gen/gen_rules.ml", line 72, charac
ters 13-109
# Called from Dune__exe__Gen_rules in file "tools/dune_rule_gen/gen_rules.ml", line 107, characters
 6-13
#
# make: *** [Makefile:124: .dune-stamp] Error 1

view this post on Zulip Ali Caglayan (Apr 03 2023 at 00:53):

I still kind of think it was premature to split the opam package in the opam repository since the split opam files in the repo always had issues.

view this post on Zulip Ali Caglayan (Apr 03 2023 at 00:53):

But I would love to be proven wrong, maybe my setup is broken.

view this post on Zulip Karl Palmskog (Apr 03 2023 at 09:51):

installation of coq-stdlib has worked fine for me across many versions of OCaml and both 8.17+rc1 and 8.17.0. I get Dune 3.7.0 by default, might be connected to some Dune version?

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 11:55):

Even if Ali were doing something wrong, if a Coq core dev must ask for help to install Coq, it's relatively strong evidence the packaging is immature. (we're testing the split packaging with dune 3.7 without issues yet, but of course successful tests don't prove absence of bugs)

view this post on Zulip Karl Palmskog (Apr 03 2023 at 11:59):

if it's a Dune version issue, we can fix it by adjusting opam version reqs. So a replication in a fresh opam switch would be helpful

view this post on Zulip Karl Palmskog (Apr 03 2023 at 12:01):

we also went through opam-repository's picky CI for that package, they even test package version downgrades

view this post on Zulip Karl Palmskog (Apr 03 2023 at 12:02):

I'm speculating, but could there be an issue with some environment variable?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 13:36):

The problem is due to ocamlfind not being aware of coq-core being installed

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 13:36):

So that seems indeed like a problem very specific to Ali's setup

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 13:39):

Ali Caglayan said:

But I would love to be proven wrong, maybe my setup is broken.

There is a very high chances that your setup is broken.

What issues do split opam files in the repo have? There are some todos, but there are no issues that would be problematic AFAICT

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 13:39):

The split setup has been in place for quite a signficant time

view this post on Zulip Karl Palmskog (Apr 03 2023 at 14:51):

I'm not aware of any issues with the split opam files per se. The crux is that now, coqc can be available without Stdlib, meaning coqc will not be useful for many purposes. This requires some downstream tools to change their approach to using Coq as an optional dependency

view this post on Zulip Karl Palmskog (Apr 03 2023 at 14:52):

I think this is a good thing in general, people will make it clear they don't depend just on Coq. In the future, we may have projects that only depend on coqc + mathcomp-ssreflect

view this post on Zulip Karl Palmskog (Apr 03 2023 at 14:56):

I think that for now though, we are not asking people to be explicit about depending on coq-core/stdlib in their opam packages (that could come in 8.18?)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 15:02):

I guess only developments not using the stdlib should update their opam deps to coq-core

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 15:02):

so that's indeed a kind of "niche" use case

view this post on Zulip Karl Palmskog (Apr 03 2023 at 15:09):

I think we need more use cases there for sure, if nothing else to demonstrate how it can be done with current tools

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2023 at 16:08):

I think HoTT and tactician work with coq-core, all you need to do is to pass -boot , but indeed we need more use cases

view this post on Zulip Ali Caglayan (Apr 03 2023 at 20:12):

By the way this was a completely fresh switch that I was trying to create.

view this post on Zulip Ali Caglayan (Apr 03 2023 at 20:13):

It is entirely possible there are some problematic enviornment variables around. For example, OCAMLFIND_DESTDIR always messes up the install of Zarith so I have to manually unset it.

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 20:58):

If your environment is entirely managed by opam things should be expected to work

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 20:59):

The "relevant" environment, that is

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 20:59):

If you're settings such env. vars by hand, OTOH, you're possibly on your own


Last updated: Jun 18 2024 at 00:02 UTC