opam package

[amahboubi]

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]

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]

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]

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]

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]

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]

Let me know if you need more information.

[pi8027]

@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]

Let me know if you need more information.

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

[pi8027]

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

[amahboubi]

@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]

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]

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

[gares]

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

[gares]

I mean, see what the constraint solver says.

[pi8027]

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