Stream: Coq devs & plugin devs

Topic: Can't find file on loadpath (opam)


view this post on Zulip Andrej Dudenhefner (Sep 06 2022 at 09:08):

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

view this post on Zulip Karl Palmskog (Sep 06 2022 at 09:09):

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

view this post on Zulip Karl Palmskog (Sep 06 2022 at 09:10):

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)

view this post on Zulip Andrej Dudenhefner (Sep 06 2022 at 09:14):

Thanks for the quick reply. I'll use core-dev then.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2022 at 17:09):

Actually this was working (except for native) but there is a bug in Dune 3.4 which broke it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2022 at 17:09):

So indeed you are seeing that bug, you can either use Dune 3.3, or indeed will have to wait


Last updated: Feb 06 2023 at 00:03 UTC