Stream: math-comp users

Topic: Coqeal


view this post on Zulip Assia Mahboubi (May 26 2020 at 10:48):

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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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) ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenji Maillard (May 26 2020 at 12:00):

can't you upgrade coq-mathcomp-multinomials to 1.5.1 ?

view this post on Zulip Kenji Maillard (May 26 2020 at 12:01):

that should go with coq-mathcomp-finmap.1.5.0

view this post on Zulip Assia Mahboubi (May 26 2020 at 12:02):

How can I do that?

view this post on Zulip Kenji Maillard (May 26 2020 at 12:02):

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

view this post on Zulip 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.

view this post on Zulip Kenji Maillard (May 26 2020 at 12:04):

hmm, my opam claim they exists though ^^'

view this post on Zulip 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.

view this post on Zulip Christian Doczkal (May 26 2020 at 12:05):

(I was going to answer, when I got a phone call)

view this post on Zulip Kenji Maillard (May 26 2020 at 12:05):

So how come it appears on my opam ?

view this post on Zulip Christian Doczkal (May 26 2020 at 12:06):

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

view this post on Zulip Kenji Maillard (May 26 2020 at 12:06):

it's from coq-extra-dev https://coq.inria.fr/opam/extra-dev

view this post on Zulip 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:

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (May 26 2020 at 13:06):

this bump is not as trivial as it seems

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 26 2020 at 13:42):

@Cyril Cohen finmap-1.4.0 has this: "coq" {(>= "8.7" & < "8.11.1")}

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (May 26 2020 at 13:46):

this was the commit by Anton Trunov: https://github.com/coq/opam-coq-archive/commit/075eed9cb834dd67ef994182bcd1e141ed7086cb

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 26 2020 at 13:46):

coq8.11mathcomp1.10.0-finmap-1.4.0+coq-8.11

view this post on Zulip Cyril Cohen (May 26 2020 at 13:47):

There is indeed a problem, with finmap 1.4.0

view this post on Zulip Cyril Cohen (May 26 2020 at 13:47):

that's why I released finmap-1.4.0+coq-8.11 later on (and forgot about it)

view this post on Zulip Cyril Cohen (May 26 2020 at 13:47):

there should be an opam package for it

view this post on Zulip Assia Mahboubi (May 26 2020 at 13:48):

(deleted)

view this post on Zulip Assia Mahboubi (May 26 2020 at 13:48):

(deleted)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 26 2020 at 14:03):

https://github.com/coq/opam-coq-archive/pull/1259

view this post on Zulip Assia Mahboubi (May 26 2020 at 14:03):

Thanks @Karl Palmskog .

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (May 26 2020 at 14:09):

I tested the tarball now manually on 8.11.0, seems to work fine.

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (May 26 2020 at 14:41):

Thanks, I just updated+upgraded, and it is now processing everything

view this post on Zulip Christian Doczkal (May 26 2020 at 15:38):

Assia Mahboubi said:

[...] Meta-question : is this the right place to ask? Cyril Cohen (I could not find Pierre Roux @proux01 in the completion)

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

view this post on Zulip Assia Mahboubi (May 26 2020 at 15:56):

:slight_smile:

view this post on Zulip Pierre Roux (May 26 2020 at 16:02):

Thanks a lot everyone (looks like I wasn't fast enough ;) ) !

view this post on Zulip Bas Spitters (Mar 07 2022 at 14:09):

Is there a reason why CoqEAL defines its own ZArith library? Did anyone make the connection between the two libraries?
https://github.com/coq-community/coqeal/blob/master/refinements/binint.v
@Cyril Cohen ?

view this post on Zulip Karl Palmskog (Mar 07 2022 at 14:10):

I thought this was because the Z in stdlib is not typeclass aware

Looks like it's because the alternative definition of Z is actually parameterized on arbitrary P and N, for refinement reasons


Last updated: Feb 08 2023 at 07:02 UTC