Could we make coq-ltac2 a dummy package in 8.11 instead of requiring Coq < 8.11?

[cpitclaudel]

Description of the problem

I'm trying to support 8.9 through 8.11 in the same project. I use Ltac2, so I have a dependency on the coq-ltac2 package. But currently that package requires Coq < 8.11.

Could the coq-ltac2 be marked as compatible with 8.11 and made to install a dummy package there? Or is there a simpler solution that I overlooked?

cc @ppedrot

[SkySkimmer]

Can't you depend on coq-ltac2 || (Coq >= 8.11)? Gaëtan Gilbert

…

On 19/05/2020 20:36, Clément Pit-Claudel wrote: Description of the problem I'm trying to support 8.9 through 8.11 in the same project. I use Ltac2, so I have a dependency on the coq-ltac2 package. But currently that package requires Coq < 8.11. Could the coq-ltac2 be marked as compatible with 8.11 and made to install a dummy package there? Or is there a simpler solution that I overlooked? cc @ppedrot <https://github.com/ppedrot> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <https://github.com/coq/coq/issues/12367>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AASZB3EGVS5JVSNBCRJDOGTRSLGTHANCNFSM4NFH6N7Q>.

[JasonGross]

According to https://opam.ocaml.org/doc/Manual.html, the correct syntax is probably "coq-ltac2" | "coq" { >= "8.11~" } (the ~ allows capturing also the beta versions, I believe)

[cpitclaudel]

Thanks, I should have looked there. I only looked at https://dune.readthedocs.io/en/stable/dune-files.html#package, and AFAICT dune doesn't support that. Am I missing something?

[JasonGross]

Indeed, it looks like this feature might be missing from dune. @ejgallego?

[ejgallego]

I don't recall the status of that, at least on master you should be able to do:

(package
 (name cohttp)
 (synopsis "An OCaml library for HTTP clients and servers")
 (description "A longer description")
 (depends
  (alcotest :with-test)
  (dune (> 1.5))
  (foo (or :dev (> 1.5) (< 2.0)))
  (uri (>= 1.9.0))
  (uri (< 2.0.0))
  (fieldslib (> v0.12))
  (fieldslib (< v0.13))))

[cpitclaudel]

This is an OR between versions, but we need an OR between packages.

[ejgallego]

This is an OR between versions, but we need an OR between packages.

If that's not yet implemented I'd suggest you file a feature request and hopefully will solved soon. I can check what's the status of this but not today sorry.

[cpitclaudel]

ocaml/dune#3497

[ejgallego]

Thanks a lot for the report @cpitclaudel , regarding the opam issue, I suggest to re-submit at https://github.com/coq/opam-coq-archive/issues as it is an issue of the repos.

[Zimmi48]

Isn't it the whole issue? It is easy to transfer issues between repos of the same organization @ejgallego.

[ejgallego]

It is easy to transfer issues between repos of the same organization @ejgallego.

Oh sorry I was not aware of that, thanks for taking care of the transfer.