Dear all,

I have been suggested to use dune to build GeoCoq to manage several interdependent package more easily. I now have something that seems to work using commands like `dune build my_pack.install`

but not using `dune build -p my_pack`

which produces the following error.

```
Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
3.8 and will be removed in an upcoming Dune version.
Hint: To disable this warning, add the following to your dune-project file:
(warnings (deprecated_coq_lang_lt_08 disabled))
File "theories/Utils/dune", line 4, characters 11-17:
4 | (theories GeoCoq))
^^^^^^
Theory "GeoCoq" has not been found.
-> required by theory GeoCoq.Utils in theories/Utils/dune:2
-> required by _build/default/theories/Utils/all_equiv.vo
-> required by
_build/install/default/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.vo
-> required by _build/default/coq-geocoq-coinc.install
-> required by alias install
File "theories/Tactics/Coinc/dune", line 4, characters 11-17:
4 | (theories GeoCoq))
^^^^^^
Theory "GeoCoq" has not been found.
-> required by theory GeoCoq.Tactics.Coinc in theories/Tactics/Coinc/dune:2
-> required by _build/default/theories/Tactics/Coinc/CoincR.vo
-> required by
_build/install/default/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.vo
-> required by _build/default/coq-geocoq-coinc.install
-> required by alias install
```

I already asked @Karl Palmskog who pointed me to this steam. Is there a way to avoid this error?

best to link to the relevant commit

I believe that the `-p`

option implies `--package`

, and that this will lead to any theories/plugins related to other packages to be ignored. So, basically, you can only use `-p`

if all the dependencies of the package you are building have been installed, even the ones from your workspace.

By the way, I suggest that you set things up so that `dune`

generates your opam files if that's not already the case.

Rodolphe Lepigre said:

I believe that the

`-p`

option implies`--package`

, and that this will lead to any theories/plugins related to other packages to be ignored. So, basically, you can only use`-p`

if all the dependencies of the package you are building have been installed, even the ones from your workspace.

So the `theories`

flag can only refer to an installed package and not to the one that is being built?

Yes, exactly.

Rodolphe Lepigre said:

By the way, I suggest that you set things up so that

`dune`

generates your opam files if that's not already the case.

It is not. Do you have a pointer?

But only when you use `-p`

.

https://dune.readthedocs.io/en/latest/howto/opam-file-generation.html

Rodolphe Lepigre said:

Yes, exactly.

Ok I'll try without the `(theories GeoCoq)`

but I think it produced another error and that adding it allowed to build using `dune build my_pack.install`

.

Rodolphe Lepigre said:

https://dune.readthedocs.io/en/latest/howto/opam-file-generation.html

Thanks.

Oh, I noticed you use `(using coq 0.2)`

, you need `(using coq 0.8)`

to be able to compose different packages.

(You do need `(theories GeoCoq)`

I believe, but I have not looked very closely.)

Rodolphe Lepigre said:

Oh, I noticed you use

`(using coq 0.2)`

, you need`(using coq 0.8)`

to be able to compose different packages.

Do I need to do so, composing packages, at the moment? I might lose compatibility with older versions of Coq that I wanted compatible for the next release. I will lift this constraint once I will have released a new version which I will do once I get dune to build the packages correctly.

It depends on your setup, if you want separate opam packages I think you do need it.

(At least if they depend on each-other.)

Rodolphe Lepigre said:

(At least if they depend on each-other.)

They do. Ok I will see if opam finds a way to have both Coq 8.11.0 and dune 3.8 (is is the earliest version that can use `using coq 0.8`

?). If not I might just not add a dune build for the release.

I don't know about Coq supported Coq versions, I only work with recent versions.

You might be fine with older versions as long as you don't have plugins, but I'm not sure if there are strict version checks in dune.

My question was more: is dune 3.8 the earliest version of dune enabling this?

Ah sorry, I think that's right.

Main problem with Dune and old Coq versions was due to some changes needed upstream to support native. If there is demand, we could now workaround this limitation and allow older Coq. IMHO that's not worth it for newer releases, it seems to me that most users are way best served by using a more recent Coq (in terms of bugfixes and performance)

```
[ERROR] Package conflict!
* Incompatible packages:
- dune = 3.8.0
- (invariant) -> coq = 8.11.1
You can temporarily relax the switch invariant with `--update-invariant'
No solution found, exiting
```

Indeed, dune 3.8.0 does not seem to be compatible with Coq 8.11.0. So I believe we will postpone adding the possibility to build with it. I will ask the other contributors of GeoCoq to be sure.

Oh Pierre, I was not aware that Dune 3.8.0 had been marked as incompatible with Coq < 8.13, that's really bizarre to be honest.

I don't have time to investigate that, but IMHO the current opam constraint is wrong, I wonder what commit added it.

Emilio Jesús Gallego Arias said:

Oh Pierre, I was not aware that Dune 3.8.0 had been marked as incompatible with Coq < 8.13, that's really bizarre to be honest.

I don't have time to investigate that, but IMHO the current opam constraint is wrong, I wonder what commit added it.

To give a bit of context, I will precise that, for the moment, we only wish to use dune to build opam packages. If I need only the content of some already installed opam packages to build a new one, can I refer to it using `(theories my_theory)`

when the content of the `dune-project`

file is the following?

```
(lang dune 2.5)
(name geocoq)
(package (name coq-geocoq-coinc))
(package (name coq-geocoq-axioms))
(package (name coq-geocoq-elements))
(package (name coq-geocoq-main))
(package (name coq-geocoq-algebraic))
(package (name coq-geocoq))
(using coq 0.2)
```

I am asking as I reorganized the folders so that dune theories should be only needed to refer to the code of some opam package(s) belonging to the dependencies of the one currently being built. However, the theory `coq-geocoq-coinc`

does not seem to be found while the package `coq-geocoq-coinc`

is installed.

```
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-geocoq-axioms.dev failed at "dune build -p coq-geocoq-axioms -j 7".
#=== ERROR while compiling coq-geocoq-axioms.dev ==============================#
# context 2.1.5 | macos/arm64 | coq.8.18.0 coq-mathcomp-field.1.19.0 | pinned(git+file:///Users/pierreboutry/Downloads/GeoCoq Repositories/GeoCoq#dune#e4fae2d32d0667b4ce5ac5cce2f2ca59bf3c69f2)
# path ~/.opam/mc.1.19.0/.opam-switch/build/coq-geocoq-axioms.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-geocoq-axioms -j 7
# exit-code 1
# env-file ~/.opam/log/coq-geocoq-axioms-1128-a0fa41.env
# output-file ~/.opam/log/coq-geocoq-axioms-1128-a0fa41.out
### output ###
# File "theories/Axioms/dune", line 5, characters 11-27:
# 5 | (theories coq-geocoq-coinc))
# ^^^^^^^^^^^^^^^^
# Theory "coq-geocoq-coinc" has not been found.
# -> required by theory GeoCoq.Axioms in theories/Axioms/dune:2
# -> required by _build/default/theories/Axioms/Definitions.vo
# -> required by
# _build/install/default/lib/coq/user-contrib/GeoCoq/Axioms/Definitions.vo
# -> required by _build/default/coq-geocoq-axioms.install
# -> required by alias install
```

Is it that the `(using coq 0.8)`

is really needed and I cannot do this with just a `(using coq 0.2)`

?

Emilio Jesús Gallego Arias said:

Oh Pierre, I was not aware that Dune 3.8.0 had been marked as incompatible with Coq < 8.13, that's really bizarre to be honest.

I don't have time to investigate that, but IMHO the current opam constraint is wrong, I wonder what commit added it.

I just opened an issue to ask about it.

The `theories`

field should contain Coq module names (logical paths, `GeoCoq....`

) rather than package names (`coq-geocoq-...`

).

Li-yao said:

The

`theories`

field should contain Coq module names (logical paths,`GeoCoq....`

) rather than package names (`coq-geocoq-...`

).

Thank you for the info. So I tried it. Now I get the following when I do a `opam install ./coq-geocoq-axioms.opam`

.

```
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-geocoq-axioms.dev failed at "dune build -p coq-geocoq-axioms -j 7".
#=== ERROR while compiling coq-geocoq-axioms.dev ==============================#
# context 2.1.5 | macos/arm64 | coq.8.11.1 coq-mathcomp-field.1.11.0 | pinned(git+file:///Users/pierreboutry/Downloads/GeoCoq Repositories/GeoCoq#dune#b06f4a97a084d11120b43b3ec9918af5ed7c6128)
# path ~/.opam/mc.1.11.0/.opam-switch/build/coq-geocoq-axioms.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-geocoq-axioms -j 7
# exit-code 1
# env-file ~/.opam/log/coq-geocoq-axioms-7051-959b63.env
# output-file ~/.opam/log/coq-geocoq-axioms-7051-959b63.out
### output ###
# File "theories/Axioms/dune", line 5, characters 11-23:
# 5 | (theories GeoCoq.Coinc))
# ^^^^^^^^^^^^
# Theory GeoCoq.Coinc not found
# -> required by theory GeoCoq.Axioms in theories/Axioms
# -> required by _build/default/theories/Axioms/Definitions.vo
# -> required by
# _build/install/default/lib/coq/user-contrib/GeoCoq/Axioms/Definitions.vo
# -> required by _build/default/coq-geocoq-axioms.install
# -> required by alias install
```

Is the error due to the (using coq 0.2) then?

I guess so since this works.

And it fails with `using coq 0.7`

Yeah, before `using dune 0.8`

, you cannot use Coq theories from other opam packages in your workspace. (At least, if I remember correctly.)

Hi PIerre, indeed the restriction was added on commit https://github.com/ocaml/opam-repository/commit/8ebbff1cc8d69b93f6f8db7b52d0307cde3a648a , I'm not sure it is worth reverting it, to be honest.

Regarding the packaging, indeed different Coq versions have different restrictions, I'd suggest using the 0.8 model, as it is the model that we hope (with small tweaks) to declare as the stable "1.0" build model.

Rodolphe Lepigre said:

Yeah, before

`using dune 0.8`

, you cannot use Coq theories from other opam packages in your workspace. (At least, if I remember correctly.)

Yes, `coq < 0.8`

won't detect installed theories.

Ok then I can postpone the build with dune to the next release since we would likely do another one soon to get compatibility with Coq 8.19.0 since I do not think we can get it to compile with the version of Coq that we target for the next release as well as with Coq 8.19.0. Thank you for the help :)

Last updated: May 25 2024 at 20:01 UTC