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)

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?

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`

.

```
$ 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
```

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

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

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.

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`

.

can't you upgrade `coq-mathcomp-multinomials`

to 1.5.1 ?

that should go with `coq-mathcomp-finmap.1.5.0`

How can I do that?

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

```
$ 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.
```

hmm, my opam claim they exists though ^^'

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.

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

So how come it appears on my opam ?

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

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

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:

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

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

this bump is not as trivial as it seems

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

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

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?

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

```
$ 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
```

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

There is indeed a problem, with finmap 1.4.0

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

there should be an opam package for it

(deleted)

(deleted)

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

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

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

Thanks @Karl Palmskog .

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

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

@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

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

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:

:slight_smile:

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

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 ?

~~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