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

Hello !

I am starting using Coqeal, typically on some toy examples on rationals, using refinements that we can find in `binrat.v`

.

I was wondering if there is a way to print the refinements instances used during the execution of the tactic `coqeal`

, since it is not very verbose.

If you `Print Ltac coqeal`

(or look at the definition in `refinements.v`

) it is defined as `apply: refines_goal; vm_compute`

, so I usually only apply `refines_goal`

to try understanding what happens. You can get more verbosity with something like `Set Typeclasses Debug`

(or something like that, I don't remember the details but theyr are somewhere in the refman of Coq).

Thank you, `Set Typeclasses Debug`

helped me figure out

I tried to use the refinements defined in `binrat`

```
From Coq Require Import Uint63.
From mathcomp Require Import all_ssreflect all_algebra.
From CoqEAL Require Import refinements hrel param.
Local Open Scope ring_scope.
Import Refinements Op.
From CoqEAL Require Import binrat.
From Bignums Require Import BigQ.
Section CoqEAL_binrat.
Notation "[ x ]" := (bigQ2rat x).
Goal (10*10 < 100*100 :> rat) ==> (100 < 1000*100 :> rat).
by coqeal. (* 2.061s *)
Abort.
Goal ([10]*[10] < [100]*[100]) ==> ([100] < [1000]*[100]).
by coqeal. (*0.029s*)
Abort.
End CoqEAL_binrat.
```

By using `Set Typeclasses Debug`

, I think that no instances declared in `binrat`

is used during the execution of `coqeal`

. They are used for the second goal, thought.

What is the good way to provide computational goals like that ?

For the first one to work, you would probably need to add an instance for mathcomp's `%:~R`

like the one for `bigQ2rat`

at the end of https://github.com/coq-community/coqeal/blob/master/refinements/binrat.v

I'm not sure I'd recommend that though, since this means constants will be parsed as unary `nat`

(or mathcomp `int`

which are basically signed nat) which is pretty inefficient. Using `bigQ2rat`

looks like the good solution to input constants.

Thanks ! I have some other question about CoqEAL. As my goal would be to relate sequences with persistent arrays, I try to find inspiration from other containers datatypes such as matrices.

In `seqmx`

, I do not understand the purpose `hzero_of`

or `const_mx_of`

, since there is only one instance of these. Are they here in case the user want to define other implementations of matrices ?

`hzero_of`

is used in this example at the end of seqmx.v https://github.com/coq-community/coqeal/blob/a69718512ac899e837ca39509d5485c96cc91de2/refinements/seqmx.v#L1452-L1454 `const_mx_of`

indeed seems less used. In any case, they could be used for other refinements of matrices (for instances with persistent arrays)

Last updated: Jul 25 2024 at 15:02 UTC