Zulip Chat Archive

Hello, I am trying to install coqeal via opam and the coq-coqeal opam package requires downgrading coq to 8.11. Is this on purpose? Meta-question : is this the right place to ask? @Cyril Cohen (I could not find Pierre Roux @proux01 in the completion)

Christian Doczkal (May 26 2020 at 11:07):

I'm not quite sure I understand the question/problem. coq-8.11.1 is the latest released version of coq and the latest released version of coqeal (1.0.3) appears to be compatible with that. Are you asking for a "dev" package compatible with coq.dev and mathcomp.dev?

Assia Mahboubi (May 26 2020 at 11:38):

Yes, coq-8.11.1 is the latest released version and opam install coq-coqeal asks me whether I want to downgrade coq from 8.11.1 to 8.11.

Assia Mahboubi (May 26 2020 at 11:41):

$ opam install coq-coqeal
The following actions will be performed:
  ↘ downgrade coq                       8.11.1 to 8.11.0
          [required by coq-coqeal]
  ∗ install   coq-bignums               8.11.0
          [required by coq-coqeal]
  ↻ recompile coq-paramcoq              1.1.2+coq8.11    [uses coq]
  ↻ recompile coq-mathcomp-ssreflect    1.10.0           [uses coq]
  ∗ install   coq-mathcomp-fingroup     1.10.0
          [required by coq-mathcomp-algebra]
  ↻ recompile coq-mathcomp-bigenough    1.0.0
          [uses coq-mathcomp-ssreflect]
  ∗ install   coq-mathcomp-algebra      1.10.0
          [required by coq-coqeal]
  ∗ install   coq-mathcomp-finmap       1.4.0
          [required by coq-mathcomp-multinomials]
  ∗ install   coq-mathcomp-multinomials 1.5
          [required by coq-coqeal]
  ∗ install   coq-coqeal                1.0.3
===== ∗ 6   ↻ 3   ↘ 1 =====
Do you want to continue? [Y/n] Y

Kenji Maillard (May 26 2020 at 11:43):

strange, for me opam info coq-coqeal indicates "coq" {>= "8.7" & < "8.12~"}. Did you opam update (in case the package for coq-coqeal changed) ?

Assia Mahboubi (May 26 2020 at 11:50):

Thanks @Kenji Maillard : I did what you suggested and opam update (which did nothing as far as I can tell) but opam upgrade is more informative as it says:

$ opam upgrade
Everything as up-to-date as possible (run with --verbose to show unavailable
upgrades).

The following packages are not being upgraded because the new versions conflict
with other installed packages:
  - coq.8.11.1
  - coq-mathcomp-finmap.1.4.1
    ∗ coq-mathcomp-multinomials.1.5 is installed and requires
    coq-mathcomp-finmap (>= 1.4 & < 1.4.1)
However, you may "opam upgrade" these packages explicitly, which will ask
permission to downgrade or uninstall the conflicting packages.
Nothing to do.

Assia Mahboubi (May 26 2020 at 11:56):

So my understanding is that although the coq-coqeal metadata look fine, the blocking issue is somewhere in its dependencies, right?
I will now try to understand where, which is not obvious to me for now.

Assia Mahboubi (May 26 2020 at 11:59):

Ok, so the problem is that coq-mathcomp-finmap.1.4.0 requires a coq version (>= "8.7" & < "8.11.1") and that coq-mathcomp-multinomials require a coq-finmap version exactly equal to 1.4.0.

Kenji Maillard (May 26 2020 at 12:00):

Kenji Maillard (May 26 2020 at 12:01):

Assia Mahboubi (May 26 2020 at 12:02):

Kenji Maillard (May 26 2020 at 12:02):

I guess opam install coq-mathcomp-finmap.1.5.0 coq-mathcomp-multinomials.1.5.1

Assia Mahboubi (May 26 2020 at 12:03):

$ opam install coq-mathcomp-finmap.1.5.0 coq-mathcomp-multinomials.1.5.1
[ERROR] Package coq-mathcomp-finmap has no version 1.5.0.
[ERROR] Package coq-mathcomp-multinomials has no version 1.5.1.

Kenji Maillard (May 26 2020 at 12:04):

Christian Doczkal (May 26 2020 at 12:05):

Yes, I think you need to ask the maintainer of coq-mathcomp-multinomials to do a point release. I don't have a 1.5.1 either.

Christian Doczkal (May 26 2020 at 12:05):

Kenji Maillard (May 26 2020 at 12:05):

Christian Doczkal (May 26 2020 at 12:06):

@Kenji Maillard , can you check which repository this is from? opam show coq-mathcomp-multinomials

Kenji Maillard (May 26 2020 at 12:06):

Christian Doczkal (May 26 2020 at 12:08):

Okay, then apparently someone submitted the version bump to the wrong repository. This should be in coq-released, if it is a point release. :unamused:

Christian Doczkal (May 26 2020 at 12:12):

So, I guess the temporary fix is to add extra-dev, but someone should file a bug against opam-coq-archive to get this moved (if it really doesn't depend on any development versions).

Cyril Cohen (May 26 2020 at 13:05):

multinomials 1.5.1 is in extra-dev because it depends on mathcomp 1.11.0+beta1 which is not a release...

Cyril Cohen (May 26 2020 at 13:06):

Cyril Cohen (May 26 2020 at 13:11):

However, what I do not understand is opam finds no solution given coq 8.11.1 and multinomials 1.5.
While making nix packages a few weeks ago, I found a solution manually:

{
   mathcomp-finmap       = "1.4.0";
   mathcomp-bigenough    = "1.0.0";
   mathcomp-analysis     = "0.2.3";
   multinomials          = "1.5";
   mathcomp-real-closed  = "1.0.4";
   coqeal                = "1.0.3";
}

One should investigate each opam package to check which one was not updated to take in subsequent versions of its dependencies

Karl Palmskog (May 26 2020 at 13:42):

Karl Palmskog (May 26 2020 at 13:43):

have you checked that finmap 1.4.0 works with Coq 8.11.1? If so, we can just update the OPAM definition. But one should look at the archive revision history why that requirement is so specific, it may have been added due to user reports?

Karl Palmskog (May 26 2020 at 13:46):

Cyril Cohen (May 26 2020 at 13:46):

$ nix-shell https://tinyurl.com/math-comp-nix --arg config '{coq = "8.11"; mathcomp = "1.10.0";}' --run nixEnv
Here is your work environement
buildInputs:
propagatedBuildInputs:
  coq8.11-mathcomp-all-1.10.0
  coq8.11mathcomp1.10.0-coqeal-1.0.3
  coq8.11mathcomp1.10.0-analysis-0.2.3
  coq8.11mathcomp1.10.0-bigenough-1.0.0
  coq8.11mathcomp1.10.0-finmap-1.4.0+coq-8.11
  coq8.11mathcomp1.10.0-real-closed-1.0.4
  coq8.11mathcomp1.10.0-multinomials-1.5
you can pass option --arg config '{coq = "x.y"; math-comp = "x.y.z";}' to nix-shell to change coq and/or math-comp versions

Cyril Cohen (May 26 2020 at 13:46):

Cyril Cohen (May 26 2020 at 13:47):

Assia Mahboubi (May 26 2020 at 13:48):

Assia Mahboubi (May 26 2020 at 13:56):

So, what is the conclusion? That there will be soon an opam package in coq-release which will solve the issue?

Karl Palmskog (May 26 2020 at 14:01):

conclusion: either Cyril or I can submit a package of finmap-1.4.0+coq8.11 to the regular OPAM repo, and after this package is merged, CoqEAL 1.0.3 will work on Coq 8.11.1

Cyril Cohen (May 26 2020 at 14:03):

Assia Mahboubi (May 26 2020 at 14:03):

Karl Palmskog (May 26 2020 at 14:03):

@Cyril Cohen is it known that the release works on Coq 8.11.0? (Since it won't be tested by CI)

Karl Palmskog (May 26 2020 at 14:09):

Karl Palmskog (May 26 2020 at 14:41):

@Assia Mahboubi package is now available in the repo (after opam update), I just checked that opam install coq-coqeal works on 8.11.1

Assia Mahboubi (May 26 2020 at 14:41):

Christian Doczkal (May 26 2020 at 15:38):

I think, given the time it took to resolve the problem, the answer is "yes" :slight_smile:

Assia Mahboubi (May 26 2020 at 15:56):

Pierre Roux (May 26 2020 at 16:02):