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

view this post on Zulip Quentin Canu (Feb 08 2023 at 14:07):

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.

view this post on Zulip Pierre Roux (Feb 08 2023 at 14:32):

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

view this post on Zulip Quentin Canu (Feb 08 2023 at 15:00):

Thank you, Set Typeclasses Debug helped me figure out

view this post on Zulip Quentin Canu (Feb 09 2023 at 10:00):

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 ?

view this post on Zulip Pierre Roux (Feb 09 2023 at 12:54):

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

view this post on Zulip Pierre Roux (Feb 09 2023 at 12:57):

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.

view this post on Zulip Quentin Canu (Feb 10 2023 at 12:40):

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 ?

view this post on Zulip Pierre Roux (Feb 10 2023 at 12:52):

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