Before 8.16 is released, I wanted to experiment with it in an opam switch. For this I use
opam pin add -k git coq-core.8.16 "https://github.com/coq/coq.git#v8.16" opam pin add -k git coq-stdlib.8.16 "https://github.com/coq/coq.git#v8.16"
The first pin installs correctly and I get
> coqc --version The Coq Proof Assistant, version 8.16.0 compiled with OCaml 4.14.0
However, the second gives me
[ERROR] The compilation of coq-stdlib.8.16 failed at "dune build -p coq-stdlib -j 15 @install". #=== ERROR while compiling coq-stdlib.8.16 ====================================# # context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 | pinned(git+https://github.com/coq/coq.git#v8.16#628f33ed) # path ~/.opam/8.16/.opam-switch/build/coq-stdlib.8.16 # command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-stdlib -j 15 @install # exit-code 1 # env-file ~/.opam/log/coq-stdlib-895-86729b.env # output-file ~/.opam/log/coq-stdlib-895-86729b.out ### output ### # [...] # (cd _build/default/theories && /home/user/.opam/8.16/bin/coqdep -boot -R . Coq -I /home/user/.opam/8.16/lib/coq-core/boot -I /home/user/.opam/8.16/lib/coq-core/clib -I /home/user/.opam/8.16/lib/coq-core/config -I /home/user/.opam/8.16/lib/coq-core/engine -I /home/user/.opam/8.16/lib/coq-core/gramlib -I /home/user/.opam/8.16/lib/coq-core/interp -I /home/user/.opam/8.16/lib/coq-core/kernel -I /[...] # *** Warning: in file ssrmatching/ssrmatching.v, declared ML module ./plugins/ssrmatching/ssrmatching_plugin has not been found! # File "user-contrib/Ltac2/dune", line 1, characters 0-167: # 1 | (coq.theory # 2 | (name Ltac2) # 3 | (package coq-stdlib) # 4 | (synopsis "Ltac2 tactic language") # 5 | (flags -w -deprecated-native-compiler-option) # 6 | (libraries coq-core.plugins.ltac2)) # (cd _build/default && /home/user/.opam/8.16/bin/coqc -w -deprecated-native-compiler-option -boot -R theories Coq -I /home/user/.opam/8.16/lib/coq-core/boot -I /home/user/.opam/8.16/lib/coq-core/clib -I /home/user/.opam/8.16/lib/coq-core/config -I /home/user/.opam/8.16/lib/coq-core/engine -I /home/user/.opam/8.16/lib/coq-core/gramlib -I /home/user/.opam/8.16/lib/coq-core/interp -I /home/user/.[...] # Error: Can't find file number_string_notation_plugin.cmxs on loadpath.
ocamlfind is up to date:
> opam list # Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq-core 8.16 pinned to version 8.16 at git+https://github.com/coq/coq.git#v8.16 dune 3.4.1 Fast, portable, and opinionated build system ocaml 4.14.0 The OCaml compiler (virtual package) ocaml-config 2 OCaml Switch Configuration ocaml-option-flambda 1 Set OCaml to be compiled with flambda activated ocaml-variants 4.14.0+options Official release of OCaml 4.14.0 ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
I highly recommend using the
core-dev opam repo and this package instead: https://github.com/coq/opam-coq-archive/blob/master/core-dev/packages/coq/coq.8.16.dev/opam
pinning directly from the repo has never been guaranteed to work, to my knowledge. Although it might work now on
master with the recent changes to the Coq build system (fully Dune-based)
Thanks for the quick reply. I'll use core-dev then.
Actually this was working (except for native) but there is a bug in Dune 3.4 which broke it.
So indeed you are seeing that bug, you can either use Dune 3.3, or indeed will have to wait
Last updated: Jun 09 2023 at 08:01 UTC