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: Oct 13 2024 at 01:02 UTC