search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

opam package #23

Open amahboubi opened 3 years ago

amahboubi commented 3 years ago

Hi @pi8027 , I have an opam switch with coq 8.13.1, and I get the following error message when trying to install your library with opam, following the instructions in the readme:

assia@tepoztlan:~/Repos/algebra-tactics$ opam install coq-mathcomp-algebra-tactics
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
pi8027 commented 3 years ago

Hi @amahboubi, it seems that you are using OPAM v1 (but then, there would be a problem with installing MathComp...). OPAM file generated by coq-community Templates requires OPAM 2.0 or later. The latest version of OPAM (2.1.0) may produce a better error message.

pi8027 commented 3 years ago

Also, if your OPAM switch uses OCaml < 4.07.0, I suggest using OCaml >= 4.07.0. The latest available version of Coq-Elpi compatible with Coq 8.13.1 (coq-elpi.1.11.1) requires that. (Sorry for saying random suggestions. From what I see, it's difficult to guess what's going on in your OPAM switch.)

amahboubi commented 3 years ago

Hi @amahboubi, it seems that you are using OPAM v1 (but then, there would be a problem with installing MathComp...). OPAM file generated by coq-community Templates requires OPAM 2.0 or later.

I am not: 

assia@tepoztlan:~$ opam --version
2.0.5
amahboubi commented 3 years ago

But I can try to upgrade my opam to the latest version and come back. If you think that's really useful. But wouldn't that be surprising?

amahboubi commented 3 years ago

Also, if your OPAM switch uses OCaml < 4.07.0, I suggest using OCaml >= 4.07.0. The latest available version of Coq-Elpi compatible with Coq 8.13.1 (coq-elpi.1.11.1) requires that. (Sorry for saying random suggestions. From what I see, it's difficult to guess what's going on in your OPAM switch.)

Sure, I understand. I can try to provide more information. I do not think that my OCaml version is guilty. Here is more info on the switch I tried to use for installing your work:

assia@tepoztlan:~$ opam list
# Packages matching: installed
# Name                      # Installed     # Synopsis
base                        v0.14.1         Full standard library replacement f
base-bigarray               base
base-threads                base
base-unix                   base
camlp5                      7.14            Preprocessor-pretty-printer of OCam
conf-findutils              1               Virtual package relying on findutil
conf-g++                    1.0             Virtual package relying on the g++ 
conf-gmp                    3               Virtual package relying on a GMP li
conf-m4                     1               Virtual package relying on m4
conf-perl                   1               Virtual package relying on perl
conf-perl-ipc-system-simple 1               Virtual package relying on perl's I
conf-perl-string-shellquote 1               Virtual package relying on perl's S
coq                         8.13.1          Formal proof management system
coq-coquelicot              3.2.0           A Coq formalization of real analysi
coq-elpi                    1.9.5           Elpi extension language for Coq
coq-equations               1.2.4+8.13      A function definition package for C
coq-extructures             0.2.2           Finite sets, maps, and other data s
coq-hierarchy-builder       1.1.0           High level commands to declare and 
coq-hott                    8.13            The Homotopy Type Theory library
coq-mathcomp-algebra        1.12.0          Mathematical Components Library on 
coq-mathcomp-analysis       0.3.7           An analysis library for mathematica
coq-mathcomp-bigenough      1.0.0           A small library to do epsilon - N r
coq-mathcomp-character      1.12.0          Mathematical Components Library on 
coq-mathcomp-field          1.12.0          Mathematical Components Library on 
coq-mathcomp-fingroup       1.12.0          Mathematical Components Library on 
coq-mathcomp-finmap         1.5.1           Finite sets, finite maps, finitely 
coq-mathcomp-real-closed    1.1.2           Mathematical Components Library on 
coq-mathcomp-solvable       1.12.0          Mathematical Components Library on 
coq-mathcomp-ssreflect      1.12.0          Small Scale Reflection
coq-mathcomp-zify           1.0.0+1.12+8.13 Micromega tactics for Mathematical 
cppo                        1.6.7           Code preprocessor like cpp for OCam
csexp                       1.3.2           Parsing and printing of S-expressio
dune                        2.8.1           Fast, portable, and opinionated bui
dune-configurator           2.8.1           Helper library for gathering system
elpi                        1.13.0          ELPI - Embeddable λProlog Interpre
ledit                       2.04            Line editor, a la rlwrap
num                         1.3             The legacy Num library for arbitrar
ocaml                       4.09.0          The OCaml compiler (virtual package
ocaml-base-compiler         4.09.0          Official release 4.09.0
ocaml-compiler-libs         v0.12.3         OCaml compiler libraries repackaged
ocaml-config                1               OCaml Switch Configuration
ocaml-migrate-parsetree     1.8.0           Convert OCaml parsetrees between di
ocamlfind                   1.8.1           A library manager for OCaml
ppx_derivers                1.2.1           Shared [@@deriving] plugin registry
ppx_deriving                5.1             Type-driven code generation for OCa
ppxlib                      0.14.0          Base library and tools for ppx rewr
re                          1.9.0           RE is a regular expression library 
result                      1.5             Compatibility Result module
seq                         base            Compatibility package for OCaml's s
sexplib0                    v0.14.0         Library containing the definition o
stdio                       v0.14.0         Standard IO library for OCaml
zarith                      1.12            Implements arithmetic and logical o

(I do not know how to render the underlined iterms but) I use an OCaml 4.09 compiler, coq 8.13.1 and coq-elpi 1.9.5.

amahboubi commented 3 years ago

Let me know if you need more information.

pi8027 commented 3 years ago

@amahboubi Could you try to upgrade coq-elpi to 1.11.1 by:

opam install coq-elpi.1.11.1

and then try opam install coq-mathcomp-algebra-tactics.0.1.0 again? (It may force you to remove Hierarchy Builder, but its version 1.2.0 should be compatible.)

pi8027 commented 3 years ago

Let me know if you need more information.

The output of opam pin would be useful if there is any.

pi8027 commented 3 years ago

mczify should also be 1.1.0. But, I expect there is no conflict with that.

amahboubi commented 3 years ago

@amahboubi Could you try to upgrade coq-elpi to 1.11.1 by:

opam install coq-elpi.1.11.1

It doesn't work, failing with the same message:

ssia@tepoztlan:~$ opam install coq-elpi.1.11.1
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
amahboubi commented 3 years ago

Let me know if you need more information.

The output of opam pin would be useful if there is any.

This one is empty:

assia@tepoztlan:~$ opam pin
assia@tepoztlan:~$
amahboubi commented 3 years ago

May be @gares could have a clue, since the problem seems to also affect my upgrading coq-elpi?

gares commented 3 years ago

No clue, I would try to make a clean switch and install in there just algebra tactics and see what happens.

gares commented 3 years ago

I mean, see what the constraint solver says.

pi8027 commented 3 years ago

Hmm, what about opam upgrade elpi coq-elpi coq-hierarchy-builder?

amahboubi commented 3 years ago

Hmm, what about opam upgrade elpi coq-elpi coq-hierarchy-builder?

Same error message:

Sorry, no solution found: there seems to be a problem with your request.
amahboubi commented 3 years ago

No clue, I would try to make a clean switch and install in there just algebra tactics and see what happens.

OK, will do that and report. Thank you both.

amahboubi commented 3 years ago

Reporting live:

assia@tepoztlan:~/Repos$ opam switch create algebra-tactics/
[ERROR] The following local packages don't appear to be installable:
          - coq-mathcomp-algebra-tactics.dev

Do you want to create an empty switch regardless? [Y/n] Y
coq-mathcomp-algebra-tactics is now pinned to git+file:///home/assia/Repos/algebra-tactics#master (version dev)
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
amahboubi commented 3 years ago

Now trying with a simple clean switch.

amahboubi commented 3 years ago

I am tired. I am upgrading to opam 2.1 (I was still on 2.0.5). I have so far ignored the error messages ubutnu 20.4's package manager displayed when trying to upgrade opam (or even to report the pb to devs) but I guess I have tackle my head on it at some point...

amahboubi commented 3 years ago

Keeping you posted, I now have a brand new opam version 2.1.0 (had to de-install manually opam-installer and opam-doc). But I have other issues:

assia@tepoztlan:~/Repos$ opam switch
#  switch                             compiler                    description
   /home/assia/Repos/algebra-tactics  
          /home/assia/Repos/algebra-tactics
   4.09.0                             ocaml-base-compiler.4.09.0  4.09.0
   belugo                             ocaml-base-compiler.4.10.0  belugo
→  current-coq                        ocaml-base-compiler.4.09.0  current-coq
   default                            ocaml-system.4.05.0         default
   itauto                             ocaml-base-compiler.4.11.1  itauto
   with-analysis-local                ocaml-base-compiler.4.05.0
          with-analysis-local
   with-coq                                                       with-coq
   with-smtcoq                        ocaml-base-compiler.4.09.0  with-smtcoq
assia@tepoztlan:~/Repos$ opam install coq-mathcomp-algebra-tactics
[WARNING] Opam package conf-perl-string-shellquote.1 depends on the following
          system package that can no longer be found: libstring-shellquote-perl
[ERROR] Package conflict!
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.5
    no matching version
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.6
    no matching version

No solution found, exiting

Continuing to investigate...

amahboubi commented 3 years ago

OK, the system package issue is now fixed, but I still get the dependency error messages:

assia@tepoztlan:~/Repos$ opam install coq-mathcomp-algebra-tactics
[ERROR] Package conflict!
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.5
    no matching version
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.6
    no matching version

No solution found, exiting
amahboubi commented 3 years ago

And I cannot force upgrade:

assia@tepoztlan:~/Repos$ opam upgrade elpi coq-elpi coq-hierarchy-builder
[ERROR] Package conflict!
  * Missing dependency:
    - coq-elpi >= 1.9.6 → elpi >= 1.13.1
    no matching version
  * Missing dependency:
    - coq-elpi >= 1.9.6 → elpi >= 1.13.5
    no matching version
  * Missing dependency:
    - coq-elpi >= 1.9.6 → elpi >= 1.13.6
    no matching version

Which I do not understand at all. So in the end I will try to create a fresh switch with my fresh opam...

amahboubi commented 3 years ago

(I was not expecting to have to re-install the package manager and perl libs to be able to test these tactics :-/

gares commented 3 years ago

The perl business is pulled in by camlp5, I've already complained... eventually I will get rid of it.

Sorry to keep you trying... Can you run opam show elpi so that I can see all the versions you do have at disposal? You should see 1.13.7 (https://opam.ocaml.org/packages/elpi/).

amahboubi commented 3 years ago

I also do not understand how to create fresh opam switches it seems, except if they are empty. Should that have worked?

assia@tepoztlan:~$ opam switch create clean-coq --empty
# Run eval $(opam env --switch=clean-coq) to update the current shell
environment
assia@tepoztlan:~$ eval $(opam env --switch=clean-coq)
assia@tepoztlan:~$ opam repo add coq-released https://coq.inria.fr/opam/released
[coq-released] synchronised from https://coq.inria.fr/opam/released
[NOTE] Repository coq-released has been added to the selections of switch
       clean-coq only.
       Run `opam repository add coq-released --all-switches|--set-default' to
       use it in all existing switches, or in newly created switches,
       respectively.

assia@tepoztlan:~$ opam install coq-mathcomp-algebra-tactics
[ERROR] Package conflict!
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.5
    no matching version
  * Missing dependency:
    - coq-mathcomp-algebra-tactics → coq-elpi >= 1.10.1 → elpi >= 1.13.6
    no matching version

No solution found, exiting
pi8027 commented 3 years ago

@amahboubi By following the same instruction, my OPAM (2.0.5 actually) could resolve dependencies. Did you run opam show elpi?

pi8027 commented 3 years ago

Also, did you run opam update recently?

amahboubi commented 3 years ago

Also, did you run opam update recently?

It is a fresh installation of opam with a fresh switch and a fresh opam repo add as displayed in my previous message. Anyway, I ran opam update which said no changes , as expected.

amahboubi commented 3 years ago 
assia@tepoztlan:~$ opam show elpi

<><> elpi: information on all versions ><><><><><><><><><><><><><><><><><><><><>
name                   elpi
all-installed-versions 1.13.0 [current-coq]
all-versions           1.0.2  1.0.3  1.0.4  1.0.5  1.1.0  1.1.1  1.2.0  1.3.1
                       1.4.0  1.4.1  1.5.2  1.6.0  1.7.0  1.8.0  1.9.0  1.9.1
                       1.10.0  1.10.1  1.10.2  1.11.0  1.11.1  1.11.2  1.11.3
                       1.11.4  1.11.4-1  1.12.0  1.13.0  1.13.1  1.13.2
                       1.13.4  1.13.5  1.13.6  1.13.7

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version      1.13.7
repository   default
url.src      "https://github.com/LPCIC/elpi/releases/download/v1.13.7/elpi-v1.13.7.tbz"
url.checksum
          "sha256=d106ce127ad10980369970c644a7be41809748448b26f2f3456d08abeff73fd6"
          "sha512=cb7b9442b47feefa6034ed37a0594dab6c5006fa4065dcf96248a8a611d104971386331c1e78ff07efd3e9eb2b7741fe2dcf7dac151d420a63a0abdbb30d51e6"
homepage     "https://github.com/LPCIC/elpi"
doc          "https://LPCIC.github.io/elpi/"
bug-reports  "https://github.com/LPCIC/elpi/issues"
dev-repo     "git+https://github.com/LPCIC/elpi.git"
authors      "Claudio Sacerdoti Coen" "Enrico Tassi"
maintainer   "Enrico Tassi <enrico.tassi@inria.fr>"
license      "LGPL-2.1-or-later"
depends      "ocaml" {>= "4.04.0"}
             "camlp5" {< "7.99"}
             "ppxlib" {>= "0.12.0"}
             "re" {>= "1.7.2"}
             "ppx_deriving" {>= "4.2"}
             "ANSITerminal" {with-test}
             "cmdliner" {with-test}
             "dune" {>= "2.2.0"}
             "conf-time" {with-test}
synopsis     ELPI - Embeddable λProlog Interpreter
description
          ELPI implements a variant of λProlog enriched with Constraint
          Handling Rules,
          a programming language well suited to manipulate syntax trees with
          binders.
          ELPI is designed to be embedded into larger applications written in
          OCaml as
          an extension language. (...)
assia@tepoztlan:~$
amahboubi commented 3 years ago

Installing coq-elpi seems to be ok actually. In the same empty switch:

assia@tepoztlan:~$ opam install coq-elpi
The following actions will be performed:
  ∗ install ocaml-options-vanilla 1
  ∗ install ocaml-base-compiler   4.12.1  [required by ocaml]
  ∗ install conf-gmp              3       [required by zarith]
  ∗ install conf-findutils        1       [required by coq]
  ∗ install base-bigarray         base
  ∗ install base-threads          base    [required by dune]
  ∗ install conf-perl             1       [required by camlp5]
  ∗ install base-unix             base    [required by dune]
  ∗ install ocaml-config          2       [required by ocaml]
  ∗ install ocaml                 4.12.1  [required by coq-elpi]
  ∗ install seq                   base    [required by re]
  ∗ install ocamlfind             1.9.1   [required by coq]
  ∗ install dune                  2.9.1   [required by coq, elpi]
  ∗ install camlp5                7.14    [required by elpi]
  ∗ install zarith                1.12    [required by coq]
  ∗ install stdlib-shims          0.3.0   [required by coq-elpi]
  ∗ install sexplib0              v0.14.0 [required by ppxlib]
  ∗ install result                1.5     [required by ppx_deriving]
  ∗ install re                    1.10.3  [required by elpi]
  ∗ install ppx_derivers          1.2.1   [required by ppx_deriving]
  ∗ install ocaml-compiler-libs   v0.12.4 [required by ppxlib]
  ∗ install cppo                  1.6.8   [required by ppx_deriving]
  ∗ install coq                   8.14.0  [required by coq-elpi]
  ∗ install ppxlib                0.23.0  [required by elpi]
  ∗ install ppx_deriving          5.2.1   [required by elpi]
  ∗ install elpi                  1.13.7  [required by coq-elpi]
  ∗ install coq-elpi              1.11.2
===== ∗ 27 =====
Do you want to continue? [Y/n]
amahboubi commented 3 years ago

@gares sorry, I overlooked your answer, but yes it seems fine, as I see elpi 1.13.7.

gares commented 3 years ago

so, it seems installing coq-elpi works and you get coq 8.14. If you press Y and then, once finished, you opam install coq-mathcomp-algebra-tactics, it blows up?

amahboubi commented 3 years ago

Amazing, it succeeded...

amahboubi commented 3 years ago

So the problem is when I ask for installing coq-mathcomp-algebra-tactics from an empty switch, and not if we manually impose coq-elpifirst.

gares commented 3 years ago

Something is very fishy here, looks like a bug in the constraint solver to me. I mean, it does no time out, it fails to find a solution! It would be a very common "bug" of automated provers, which typically sacrifice completeness for speed... maybe constraint solvers are the same.

gares commented 3 years ago

Would you try again passing --use-internal-solver? Maybe you happen to have an external solver installed (eg Z3...)

amahboubi commented 3 years ago

Sure. Try again which command?

gares commented 3 years ago

installing coq-mathcomp-algebra-tactics from an empty switch

That thing, which would be opam switch create ...; opam install --use-internal-solver coq-m-c-a-t

gares commented 3 years ago

I could not find a way to query which solvers opam is using, that would also answer my question: are we talking about the same solver or you are using another one? (I don't have any extra solver installed)

gares commented 3 years ago

You could also try to open an issue, (eg: https://github.com/ocaml/opam/issues/4495 ), they were helpful.