Ocaml 5.3.0 install rocq 9.0.0 failed ("failed to locate Coq kernel package in split build mode")

[RuifengFu]

Description of the problem

[ERROR] The compilation of rocq-core.9.0.0 failed at "make dunestrap COQ_SPLIT=1 DUNESTRAPOPT=-p rocq-core".
∗ installed coq-core.9.0.0
∗ installed coqide-server.9.0.0

#=== ERROR while compiling rocq-core.9.0.0 ====================================#
# context     2.3.0 | linux/x86_64 | ocaml.5.3.0 | https://opam.ocaml.org#999bff3ed88d26f76ff7eaddbfa7af49ed4737dc
# path        ~/.opam/default/.opam-switch/build/rocq-core.9.0.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_SPLIT=1 DUNESTRAPOPT=-p rocq-core
# exit-code   2
# env-file    ~/.opam/log/rocq-core-108432-2ac678.env
# output-file ~/.opam/log/rocq-core-108432-2ac678.out
### output ###
# [...]
# 67 |   (source_tree plugins)
# 68 |   (source_tree theories)
# 69 |   (source_tree user-contrib))
# 70 |  (action
# 71 |   (with-stdout-to %{targets}
# 72 |    (run tools/dune_rule_gen/gen_rules.exe Corelib theories -split %{env:COQ_DUNE_EXTRA_OPT=}))))
# (cd _build/default && tools/dune_rule_gen/gen_rules.exe Corelib theories -split '') > _build/default/theories_dune_split
# [gen_rules] Fatal error:
# Anomaly
# "Uncaught exception Invalid_argument("failed to locate Coq kernel package in split build mode: rocq-runtime.kernel")."
#   Please report at http://coq.inria.fr/bugs/.
# make: *** [Makefile:136: .dune-stamp] Error 1

Small Rocq / Coq file to reproduce the bug

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

Did rocq-runtime install properly?
Do you have a non-opam ocaml installed (typically from your package manager)?

[RuifengFu]

Thanks for your comment.
Sorry, but I'm a newbie in Ocaml.
I installed rocq-runtime (it shows up in the list), and I don't have a non - opam ocaml installed (can't use commands like coqc/rocqc or coqtop/rocqtop).

This is the full output.

opam pin add rocq-prover 9.0.0
[NOTE] Pinning unchanged
rocq-prover is now pinned to version 9.0.0

The following actions will be performed:
=== install 3 packages
  ∗ rocq-core   9.0.0          [required by rocq-prover]
  ∗ rocq-prover 9.0.0 (pinned)
  ∗ rocq-stdlib 9.0.0          [required by rocq-prover]

Proceed with ∗ 3 installations? [y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved rocq-stdlib.9.0.0  (cached)
⬇ retrieved rocq-core.9.0.0  (cached)
[ERROR] The compilation of rocq-core.9.0.0 failed at "make dunestrap COQ_SPLIT=1 DUNESTRAPOPT=-p rocq-core".

#=== ERROR while compiling rocq-core.9.0.0 ====================================#
# context     2.3.0 | linux/x86_64 | ocaml.5.3.0 | https://opam.ocaml.org#999bff3ed88d26f76ff7eaddbfa7af49ed4737dc
# path        ~/.opam/default/.opam-switch/build/rocq-core.9.0.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_SPLIT=1 DUNESTRAPOPT=-p rocq-core
# exit-code   2
# env-file    ~/.opam/log/rocq-core-120211-f684d6.env
# output-file ~/.opam/log/rocq-core-120211-f684d6.out
### output ###
# [...]
# 77 |   (source_tree plugins)
# 78 |   (source_tree theories)
# 79 |   (source_tree user-contrib))
# 80 |  (action
# 81 |   (with-stdout-to %{targets}
# 82 |    (run tools/dune_rule_gen/gen_rules.exe Ltac2 user-contrib/Ltac2 -split %{env:COQ_DUNE_EXTRA_OPT=}))))
# (cd _build/default && tools/dune_rule_gen/gen_rules.exe Ltac2 user-contrib/Ltac2 -split '') > _build/default/ltac2_dune_split
# [gen_rules] Fatal error:
# Anomaly
# "Uncaught exception Invalid_argument("failed to locate Coq kernel package in split build mode: rocq-runtime.kernel")."
#   Please report at http://coq.inria.fr/bugs/.
# make: *** [Makefile:136: .dune-stamp] Error 1

Here's the list of opam installed packages.

opam list -i
# Packages matching: installed
# Name                  # Installed # Synopsis
base                    v0.17.1     Full standard library replacement for OCaml
base-bigarray           base
base-domains            base
base-effects            base
base-nnp                base        Naked pointers prohibited in the OCaml heap
base-threads            base
base-unix               base
conf-gmp                5           Virtual package relying on a GMP lib system installation
conf-linux-libc-dev     0           Virtual package relying on the installation of the Linux kernel headers files
conf-pkg-config         4           Check if pkg-config is installed and create an opam switch local pkgconfig folder
cppo                    1.8.0       Code preprocessor like cpp for OCaml
csexp                   1.5.2       Parsing and printing of S-expressions in Canonical form
dune                    3.18.1      Fast, portable, and opinionated build system
dune-configurator       3.18.1      Helper library for gathering system configuration
jane-street-headers     v0.17.0     Jane Street C header files
jsonrpc                 1.22.0      Jsonrpc protocol implemenation
jst-config              v0.17.0     Compile-time configuration for Jane Street libraries
lsp                     1.22.0      LSP protocol implementation in OCaml
num                     1.5-1       The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                   5.3.0       The OCaml compiler (virtual package)
ocaml-compiler-libs     v0.17.0     OCaml compiler libraries repackaged
ocaml-config            3           OCaml Switch Configuration
ocaml-system            5.3.0       The OCaml compiler (system version, from outside of opam)
ocaml_intrinsics_kernel v0.17.1     Intrinsics
ocamlbuild              0.16.1      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind               1.9.8       A library manager for OCaml
octavius                1.2.2       Ocamldoc comment syntax parser
parsexp                 v0.17.0     S-expression parsing library
ppx_assert              v0.17.0     Assert-like extension nodes that raise useful errors on failure
ppx_base                v0.17.0     Base set of ppx rewriters
ppx_cold                v0.17.0     Expands [@cold] into [@inline never][@specialise never][@local never]
ppx_compare             v0.17.0     Generation of comparison functions from types
ppx_derivers            1.2.1       Shared [@@deriving] plugin registry
ppx_deriving            6.0.3       Type-driven code generation for OCaml
ppx_enumerate           v0.17.0     Generate a list containing all values of a finite type
ppx_globalize           v0.17.0     A ppx rewriter that generates functions to copy local values to the global heap
ppx_hash                v0.17.0     A ppx rewriter that generates hash functions from type expressions and definitions
ppx_here                v0.17.0     Expands [%here] into its location
ppx_import              1.11.0      A syntax extension for importing declarations from interface files
ppx_inline_test         v0.17.0     Syntax extension for writing in-line tests in ocaml code
ppx_js_style            v0.17.0     Code style checker for Jane Street Packages
ppx_optcomp             v0.17.0     Optional compilation for OCaml
ppx_sexp_conv           v0.17.0     [@@deriving] plugin to generate S-expression conversion functions
ppx_yojson_conv         v0.17.0     [@@deriving] plugin to generate Yojson conversion functions
ppx_yojson_conv_lib     v0.17.0     Runtime lib for ppx_yojson_conv
ppxlib                  0.35.0      Standard infrastructure for ppx rewriters
ppxlib_jane             v0.17.2     Utilities for working with Jane Street AST constructs
result                  1.5         Compatibility Result module
rocq-runtime            9.0.0       The Rocq Prover -- Core Binaries and Tools
sel                     0.6.0       Simple Event Library
seq                     base        Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib                 v0.17.0     Library for serializing OCaml values to and from S-expressions
sexplib0                v0.17.0     Library containing the definition of S-expressions and some base converters
stdio                   v0.17.0     Standard IO library for OCaml
stdlib-shims            0.3.0       Backport some of the new stdlib features to older compiler
time_now                v0.17.0     Reports the current time
topkg                   1.0.8       The transitory OCaml software packager
uutf                    1.0.4       Non-blocking streaming Unicode codec for OCaml
yojson                  2.2.2       Yojson is an optimized parsing and printing library for the JSON format
zarith                  1.14        Implements arithmetic and logical operations over arbitrary-precision integers

[SkySkimmer]

can't use commands like coqc/rocqc or coqtop/rocqtop

coq is not part of ocaml, it's a user of ocaml

[SkySkimmer]

What does ocamlfind query rocq-runtime.kernel say? Is opam exec -- ocamlfind query rocq-runtime.kernel different?
What do command -v ocamlopt and command -v ocamlfind say?

[RuifengFu]

❯ ocamlfind query rocq-runtime.kernel
/home/xxx/.opam/default/lib/rocq-runtime/kernel
❯ opam exec -- ocamlfind query rocq-runtime.kernel
/home/xxx/.opam/default/lib/rocq-runtime/kernel
❯ command -v ocamlopt
/usr/bin/ocamlopt
❯ command -v ocamlfind
/home/xxx/.opam/default/bin/ocamlfind

[SkySkimmer]

/usr/bin/ocamlopt

That means you have a non-opam ocaml installed.
What does opam exec -- sh -c 'command -v ocamlc' say?

[RuifengFu]

/usr/bin/ocamlc

[SkySkimmer]

Do you have a file /usr/bin/ocamlfind?

[RuifengFu]

yes

[SkySkimmer]

ocaml/ocamlfind#107

opam install ocaml-compiler may work, otherwise you will need to create a switch with a non-system compiler https://rocq-prover.org/docs/managing-versions#switches
Ocaml 4.14.2 is recommended for rocq, ocaml 5+ is slower and does not support https://rocq-prover.org/doc/master/refman/proofs/writing-proofs/equality.html#coq:tacn.native_compute