don't depend on coq stdlib

[Alizter]

We use the .opam.template feature of dune to get these weird dependency constrains in #2284.

This will probably have breakages in Contrib which I will fix by disabling what we don't really need.

[jdchristensen]

I'm curious why the dependency information will be listed in two files (coq-hott.opam and coq-hott.opam.template) and is slightly different in the two places, with dune omitted in the former.

[jdchristensen]

Also, is this related to #2290?

[Alizter]

@jdchristensen Yes, I am attempting to get this to build with 9.1.

The coq-hott.opam file is generated by dune using information found in dune-project and additionally any fields that appear in coq-hott.opam.template. Dune cannot (does not want to) express disjunctive package dependencies as was suggested in #2284, so this is the way to get the constraint to work.

We are in a bit of a blind spot when it comes to Rocq development. We are one of the very few users of dune and of -noinit and both of these things are broken on recent versions of Rocq for separate reasons. I am not fully certain if I can fix all of the issues appearing.

[jdchristensen]

The coq-hott.opam file is generated by dune using information found in dune-project and additionally any fields that appear in coq-hott.opam.template.

The depends field in the .template file contains a dune dependency, but that doesn't appear in the .opam file. How does that fit with what you wrote above?

[Alizter]

@jdchristensen I forgot to do dune build coq-hott.opam before committing.

[jdchristensen]

@jdchristensen I forgot to do dune build coq-hott.opam before committing.

Does it make sense to commit a generated file? I guess it means that others don't need to run the generate script, but it also means that one has to remember to generate before committing.

[Alizter]

@jdchristensen We've been generating this file for a while with no problems. The only difference is the .template file which lets us manually specify some opam fields.

[jdchristensen]

@Alizter What's the status of this and #2284? Now that the CI works with recent Rocq, should we rebase this on master and see if it works? Or is none of this needed now that the dune build works (#2312)?

[Alizter]

If everything is working as it should, then yes it is not needed any longer.

[jdchristensen]

Ok, I'll close this then.

[jdchristensen]

It seems like this is still useful. Can we just merge it as is? I'll reopen.

[jdchristensen]

The format of this is different from what is was before, with extra square brackets. The | is also not parenthesized as it is in #2284. Is the semantics here the same as in #2284? If so, can we just merge this PR?

[jdchristensen]

@Alizter @proux01 I tested a variant of this, and was not able to build Coq-HoTT using coq-core 9.0. As Ali had mentioned, there is an error involving coqc --config. I used

depends: [
  "dune" {>= "3.13"}
  ("coq-core" {>= "9.0"} | "coq" {>= "8.19.0" & < "9~"})
  "odoc" {with-doc}
]

in the coq-hott.opam file, which I found to be the most readable option, and which has the desired effect. The full set of steps I used and the error messages are below.

So unless there is an easy workaround, I think we'll have to use something like

  ("coq-core" {>= "9.1"} | "coq" {>= "8.19.0" & < "9.1~"})

(untested).

Click to show

$ opam switch create test-opam --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-variants" {= "4.14.1+options"} "ocaml-option-flambda"]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved ocaml-config.2  (cached)
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-option-flambda.1
⬇ retrieved ocaml-variants.4.14.1+options  (cached)
∗ installed ocaml-variants.4.14.1+options
∗ installed ocaml-config.2
∗ installed ocaml.4.14.1
Done.
# Run eval $(opam env --switch=test-opam) to update the current shell environment
$ eval $(opam env --switch=test-opam)
$ time opam install .
Package coq-hott does not exist, create as a NEW package? [Y/n] y
coq-hott is now pinned to git+file:///home/jdc/scratchy/math/me/homotopy-type-theory/HoTT-master#master (version ~dev)
The following actions will be performed:
  ∗ install conf-linux-libc-dev 0      [required by rocq-runtime]
  ∗ install conf-pkg-config     4      [required by zarith]
  ∗ install ocamlfind           1.9.8  [required by rocq-runtime]
  ∗ install conf-gmp            5      [required by zarith]
  ∗ install dune                3.20.2 [required by coq-hott]
  ∗ install zarith              1.14   [required by rocq-runtime]
  ∗ install rocq-runtime        9.0.0  [required by coq-core]
  ∗ install coq-core            9.0.0  [required by coq-hott]
  ∗ install coq-hott            ~dev*
===== ∗ 9 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved conf-gmp.5  (cached)
⬇ retrieved coq-core.9.0.0  (cached)
⬇ retrieved dune.3.20.2  (cached)
∗ installed conf-gmp.5
∗ installed conf-pkg-config.4
⬇ retrieved ocamlfind.1.9.8  (cached)
⬇ retrieved rocq-runtime.9.0.0  (cached)
∗ installed conf-linux-libc-dev.0
⬇ retrieved zarith.1.14  (cached)
∗ installed ocamlfind.1.9.8
⬇ retrieved coq-hott.~dev  (git+file:///home/jdc/scratchy/math/me/homotopy-type-theory/HoTT-master#master)
∗ installed zarith.1.14
∗ installed dune.3.20.2
∗ installed rocq-runtime.9.0.0
∗ installed coq-core.9.0.0
[ERROR] The compilation of coq-hott.~dev failed at "dune build -p coq-hott -j 7 @install".

#=== ERROR while compiling coq-hott.~dev ======================================#
# context     2.1.5 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.14.1+options | pinned(git+file:///home/jdc/scratchy/math/me/homotopy-type-theory/HoTT-master#master#228f8f3896f3957d0f5844b5d875acda56e5b41b)
# path        ~/scratchy/.opam/test-opam/.opam-switch/build/coq-hott.~dev
# command     ~/scratchy/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-hott -j 7 @install
# exit-code   1
# env-file    ~/scratchy/.opam/log/coq-hott-47947-4e5160.env
# output-file ~/scratchy/.opam/log/coq-hott-47947-4e5160.out
### output ###
# Warning: Skipping installed theories due to 'coqc --config' failure:
# - /home/jdc/scratchy/.opam/test-opam/bin/coqc --config failed with exit code 1.
# Hint: Try running 'coqc --config' manually to see the error.
# Couldn't find Coq standard library, and theory is not using (stdlib no)
# -> required by _build/default/theories/Basics.glob
# -> required by _build/install/default/lib/coq/user-contrib/HoTT/Basics.glob
# -> required by _build/default/coq-hott.install
# -> required by alias install



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-hott ~dev
└─ 
┌─ The following changes have been performed
│ ∗ install conf-gmp            5
│ ∗ install conf-linux-libc-dev 0
│ ∗ install conf-pkg-config     4
│ ∗ install coq-core            9.0.0
│ ∗ install dune                3.20.2
│ ∗ install ocamlfind           1.9.8
│ ∗ install rocq-runtime        9.0.0
│ ∗ install zarith              1.14
└─ 

<><> coq-core.9.0.0 installed successfully ><><><><><><><><><><><><><><><><><><>
=> Coq has been renamed to The Rocq Prover, see
   https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details. 
     This package provides compatibility binaries to ease the transition to the new rocq binary.

The former state can be restored with:
    /usr/bin/opam switch import
"/home/jdc/scratchy/.opam/test-opam/.opam-switch/backup/state-20251001203722.export"

real	3m54.370s
user	9m21.053s
sys	1m2.561s
$ coqc --config
cannot guess a path for Rocq libraries; please use -coqlib option or ensure you have installed the package containing Rocq's prelude (rocq-core in OPAM) If you intend to use Rocq without prelude, the -boot -noinit options must be used.

[jdchristensen]

@proux01 Thanks for the tip in #2284. I just pushed a version that builds for me with Rocq 9.0, without using the standard library.

I also verified that contrib/SetoidRewrite.v works from within this opam switch.

@Alizter , does this look good to you?

[Alizter]

That looks fine to me. Thanks for taking this on.

[jdchristensen]

@Alizter Do you know what's going on with the CI / install job that is taking more than an hour? It's sitting there printing out sha hashes.

[jdchristensen]

@Alizter Also, should we update rocq-prover/opam#3522 to avoid depending on the Coq stdlib? Or will that not matter for the context in which that .opam file is used?

[jdchristensen]

I've cancelled the CI job since it's just wasting CPU time. And I've restarted all jobs to see if the issue was just a temporary glitch.

[jdchristensen]

That CI glitch went away, so I'm merging. The only question that remains is the one about updating rocq-prover/opam#3522

[jdchristensen]

@Alizter Oh, another question I just remembered: this version of the PR dropped the "odoc" dependency. Is that correct? I don't know what it is or whether we should be depending on it.

[Alizter]

@jdchristensen That's a default from dune for ocaml projects nothing to worry about.

[proux01]

@Alizter Also, should we update rocq-prover/opam#3522 to avoid depending on the Coq stdlib? Or will that not matter for the context in which that .opam file is used?

I think it's wort updating it in any case, the least unused dependencies the better.

[jdchristensen]

@proux01 That makes sense to me. Can you or @Alizter do this?

[proux01]

Done: rocq-prover/opam#3525

[jdchristensen]

Thanks, @proux01 !