Stream: Dune devs & users

Topic: Theory "mytheory" has not been found


view this post on Zulip Pierre Boutry (Mar 19 2024 at 09:39):

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?

view this post on Zulip Karl Palmskog (Mar 19 2024 at 09:44):

best to link to the relevant commit

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:28):

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.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:30):

By the way, I suggest that you set things up so that dune generates your opam files if that's not already the case.

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:30):

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?

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:30):

Yes, exactly.

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:31):

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?

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:31):

But only when you use -p.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:31):

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

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:32):

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.

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:32):

Rodolphe Lepigre said:

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

Thanks.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:34):

Oh, I noticed you use (using coq 0.2), you need (using coq 0.8) to be able to compose different packages.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:35):

(You do need (theories GeoCoq) I believe, but I have not looked very closely.)

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:37):

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.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:40):

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

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:40):

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

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:42):

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.

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:43):

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

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:44):

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.

view this post on Zulip Pierre Boutry (Mar 19 2024 at 10:45):

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

view this post on Zulip Rodolphe Lepigre (Mar 19 2024 at 10:48):

Ah sorry, I think that's right.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 19 2024 at 12:52):

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)

view this post on Zulip Pierre Boutry (Mar 19 2024 at 14:00):

[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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 09:08):

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.

view this post on Zulip Pierre Boutry (Mar 20 2024 at 12:32):

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)?

view this post on Zulip Pierre Boutry (Mar 20 2024 at 12:45):

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.

view this post on Zulip Li-yao (Mar 20 2024 at 13:05):

The theories field should contain Coq module names (logical paths, GeoCoq....) rather than package names (coq-geocoq-...).

view this post on Zulip Pierre Boutry (Mar 20 2024 at 13:18):

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?

view this post on Zulip Pierre Boutry (Mar 20 2024 at 13:22):

I guess so since this works.

view this post on Zulip Pierre Boutry (Mar 20 2024 at 13:24):

And it fails with using coq 0.7

view this post on Zulip Rodolphe Lepigre (Mar 20 2024 at 13:31):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 13:31):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 13:32):

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.

view this post on Zulip Pierre Boutry (Mar 20 2024 at 13:38):

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