Ali Caglayan (Apr 03 2023 at 00:49): 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
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.
Ali Caglayan (Apr 03 2023 at 00:53):But I would love to be proven wrong, maybe my setup is broken.
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?
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)
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
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
Karl Palmskog (Apr 03 2023 at 12:02):I'm speculating, but could there be an issue with some environment variable?
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
Emilio Jesús Gallego Arias (Apr 03 2023 at 13:36):So that seems indeed like a problem very specific to Ali's setup
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
Emilio Jesús Gallego Arias (Apr 03 2023 at 13:39):The split setup has been in place for quite a signficant time
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
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
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?)
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
Emilio Jesús Gallego Arias (Apr 03 2023 at 15:02):so that's indeed a kind of "niche" use case
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
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
Ali Caglayan (Apr 03 2023 at 20:12):By the way this was a completely fresh switch that I was trying to create.
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.
Paolo Giarrusso (Apr 03 2023 at 20:58):If your environment is entirely managed by opam things should be expected to work
Paolo Giarrusso (Apr 03 2023 at 20:59):The "relevant" environment, that is
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: Nov 29 2023 at 22:01 UTC