Wrong elpi dependency for coq-elpi in coqorg/coq:dev

chdoc commented 3 years ago

I'm getting build failures using the coqorg/coq:dev image for a coq development that has coq-elpi as a dependecy. The problem appears to be that opam for some unknown reason tries to install elpi-1.10.2 even though the coq-elpi.dev package specifies 1.12 as the minimum version for elpi:

    - install elpi                    1.10.2
    - install coq-elpi                dev
    - install coq-hierarchy-builder   dev
[...]
  [coq-elpi.dev] synchronised from git+https://github.com/LPCIC/coq-elpi.git#coq-master

According to the opam file at the given location, this is not a valid solution: https://github.com/LPCIC/coq-elpi/blob/coq-master/coq-elpi.opam

Full build log

Unfortunately, I don't have a docker setup, so I cannot look into the container to see what's wrong. I'm filing this here, because I cannot reproduce the problem using my local opam installation.

erikmd commented 3 years ago

Hi @chdoc, thanks for opening this, I am able to reproduce the issue locally with Docker (see minimal working example below).

But, it seems there is no "bug" in docker-coq side: the "issue" is just related to opam and your dependencies, namley:

elpi.1.10.2 is just an admissible version of the dependency (not the latest one, indeed)
as shown in the example session, if you pin elpi to 1.12.0 manually, opam just computes another admissible version for the other dependencies;
so I'd just suggest that you add in your coq-elpi.opam a constraint that enforces the fact that coq-graph-theory does not compile with elpi.1.10.2 and requires a more recent version.

MWE session

$ docker pull coqorg/coq:dev
$ docker run --name=coq-community_docker-coq_issue-16 -it coqorg/coq:dev
coq@1e7515edd4f4:~$ opam pin add -n coq-graph-theory https://github.com/coq-community/graph-theory.git#hierarchy-builder
[coq-graph-theory.0.7] synchronised from git+https://github.com/coq-community/graph-theory.git#hierarchy-builder
coq-graph-theory is now pinned to git+https://github.com/coq-community/graph-theory.git#hierarchy-builder (version dev)

coq@1e7515edd4f4:~$ opam install coq-graph-theory

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-graph-theory.dev] no changes from git+https://github.com/coq-community/graph-theory.git#hierarchy-builder

The following actions will be performed:
  - install coq-mathcomp-ssreflect  dev        [required by coq-graph-theory]
  - install ppx_derivers            1.2.1      [required by ocaml-migrate-parsetree, ppx_deriving]
  - install camlp5                  7.13       [required by elpi]
  - install result                  1.5        [required by ocaml-migrate-parsetree, ppx_deriving]
  - install seq                     0.2.2      [required by re]
  - install cppo                    1.6.6      [required by ppx_deriving]
  - install ppx_tools               5.0+4.05.0 [required by ppx_deriving]
  - install coq-mathcomp-bigenough  1.0.0      [required by coq-mathcomp-finmap]
  - install ocaml-migrate-parsetree 1.8.0      [required by elpi]
  - install re                      1.9.0      [required by elpi]
  - install coq-mathcomp-finmap     dev        [required by coq-graph-theory]
  - install ppxfind                 1.4        [required by ppx_deriving]
  - install ppx_tools_versioned     5.4.0      [required by elpi]
  - install ppx_deriving            4.5        [required by elpi]
  - install elpi                    1.10.2     [required by coq-elpi]
  - install coq-elpi                dev        [required by coq-hierarchy-builder]
  - install coq-hierarchy-builder   dev        [required by coq-graph-theory]
  - install coq-graph-theory        dev*
===== 18 to install =====
Do you want to continue? [Y/n] 

coq@1e7515edd4f4:~$ opam pin add -n -y -k version elpi 1.12.0
elpi is now pinned to version 1.12.0

coq@1e7515edd4f4:~$ opam install coq-graph-theory

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-graph-theory.dev] no changes from git+https://github.com/coq-community/graph-theory.git#hierarchy-builder

The following actions will be performed:
  - install coq-mathcomp-ssreflect  dev        [required by coq-graph-theory]
  - install ppx_derivers            1.2.1      [required by ppx_deriving, ocaml-migrate-parsetree,
                                               ppxlib]
  - install camlp5                  7.13       [required by elpi]
  - install ocaml-compiler-libs     v0.12.3    [required by ppxlib]
  - install sexplib0                v0.12.0    [required by base]
  - install result                  1.5        [required by ocaml-migrate-parsetree, ppx_deriving]
  - install seq                     0.2.2      [required by re]
  - install cppo                    1.6.6      [required by ppx_deriving]
  - install ppx_tools               5.0+4.05.0 [required by ppx_deriving]
  - install coq-mathcomp-bigenough  1.0.0      [required by coq-mathcomp-finmap]
  - install base                    v0.12.0    [required by ppxlib]
  - install ocaml-migrate-parsetree 1.8.0      [required by elpi]
  - install re                      1.9.0      [required by elpi]
  - install coq-mathcomp-finmap     dev        [required by coq-graph-theory]
  - install stdio                   v0.12.0    [required by ppxlib]
  - install ppxfind                 1.4        [required by ppx_deriving]
  - install ppxlib                  0.14.0     [required by elpi]
  - install ppx_deriving            4.5        [required by elpi]
  - install elpi                    1.12.0*    [required by coq-elpi]
  - install coq-elpi                dev        [required by coq-hierarchy-builder]
  - install coq-hierarchy-builder   dev        [required by coq-graph-theory]
  - install coq-graph-theory        dev*
===== 22 to install =====
Do you want to continue? [Y/n] 

coq@1e7515edd4f4:~$ opam config report 
# opam config report
# opam-version      2.0.7 
# self-upgrade      no
# system            arch=x86_64 os=linux os-distribution=debian os-version=10
# solver            builtin-mccs+glpk
# install-criteria  -removed,-count[version-lag,request],-count[version-lag,changed],-changed
# upgrade-criteria  -removed,-count[version-lag,solution],-new
# jobs              1
# repositories      4 (http) (default repo at 36c4e477)
# pinned            2 (git), 5 (version)
# current-switch    4.05.0

coq@1e7515edd4f4:~$ opam list    
# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 base        Num library distributed with the OCaml compiler
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-gmp                 2           Virtual package relying on a GMP lib system installation
conf-m4                  1           Virtual package relying on m4
conf-perl                1           Virtual package relying on perl
coq                      dev         pinned to version dev at git+https://github.com/coq/coq#2eeeba765982
coq-bignums              dev         Bignums, the Coq library of arbitrary large numbers
dune                     2.5.1       pinned to version 2.5.1
num                      0           pinned to version 0
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.8.1       pinned to version 1.8.1
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compiler
opam-depext              1.1.5       install OS distribution packages
zarith                   1.10        pinned to version 1.10

coq@1e7515edd4f4:~$ opam pin list
coq.dev                              git      git+https://github.com/coq/coq#2eeeba76598258bd5691a9825fd888c350fbcef3
coq-graph-theory.dev  (uninstalled)  git      git+https://github.com/coq-community/graph-theory.git#hierarchy-builder
dune.2.5.1                           version  2.5.1
elpi.1.12.0           (uninstalled)  version  1.12.0
num.0                                version  0
ocamlfind.1.8.1                      version  1.8.1
zarith.1.10                          version  1.10

coq@1e7515edd4f4:~$ opam config list

<><> Global opam variables ><><><><><><><><><><><><><><><><><><><><><><><><><><>
arch              x86_64          # Inferred from system
jobs              1               # The number of parallel jobs set up in opam configuration
make              make            # The 'make' command to use
opam-version      2.0.7           # The currently running opam version
os                linux           # Inferred from system
os-distribution   debian          # Inferred from system
os-family         debian          # Inferred from system
os-version        10              # Inferred from system
root              /home/coq/.opam # The current opam root directory
switch            4.05.0          # The identifier of the current switch
sys-ocaml-version                 # OCaml version present on your system independently of opam, if any

<><> Configuration variables from the current switch ><><><><><><><><><><><><><>
prefix   /home/coq/.opam/4.05.0
lib      /home/coq/.opam/4.05.0/lib
bin      /home/coq/.opam/4.05.0/bin
sbin     /home/coq/.opam/4.05.0/sbin
share    /home/coq/.opam/4.05.0/share
doc      /home/coq/.opam/4.05.0/doc
etc      /home/coq/.opam/4.05.0/etc
man      /home/coq/.opam/4.05.0/man
toplevel /home/coq/.opam/4.05.0/lib/toplevel
stublibs /home/coq/.opam/4.05.0/lib/stublibs
user     coq
group    coq

<><> Package variables ('opam config list PKG' to show) <><><><><><><><><><><><>
PKG:name       # Name of the package
PKG:version    # Version of the package
PKG:depends    # Resolved direct dependencies of the package
PKG:installed  # Whether the package is installed
PKG:enable     # Takes the value "enable" or "disable" depending on whether the package is installed
PKG:pinned     # Whether the package is pinned
PKG:bin        # Binary directory for this package
PKG:sbin       # System binary directory for this package
PKG:lib        # Library directory for this package
PKG:man        # Man directory for this package
PKG:doc        # Doc directory for this package
PKG:share      # Share directory for this package
PKG:etc        # Etc directory for this package
PKG:build      # Directory where the package was built
PKG:hash       # Hash of the package archive
PKG:dev        # True if this is a development package
PKG:build-id   # A hash identifying the precise package version with all its dependencies

coq@1e7515edd4f4:~$ opam switch export dump 
coq@1e7515edd4f4:~$ cat dump
opam-version: "2.0"
compiler: [
  "base-bigarray.base"
  "base-threads.base"
  "base-unix.base"
  "ocaml.4.05.0"
  "ocaml-base-compiler.4.05.0"
  "ocaml-config.1"
]
roots: [
  "coq.dev"
  "coq-bignums.dev"
  "dune.2.5.1"
  "num.0"
  "ocaml-base-compiler.4.05.0"
  "ocamlfind.1.8.1"
  "opam-depext.1.1.5"
  "zarith.1.10"
]
installed: [
  "base-bigarray.base"
  "base-num.base"
  "base-threads.base"
  "base-unix.base"
  "conf-findutils.1"
  "conf-gmp.2"
  "conf-m4.1"
  "conf-perl.1"
  "coq.dev"
  "coq-bignums.dev"
  "dune.2.5.1"
  "num.0"
  "ocaml.4.05.0"
  "ocaml-base-compiler.4.05.0"
  "ocaml-config.1"
  "ocaml-secondary-compiler.4.08.1-1"
  "ocamlfind.1.8.1"
  "ocamlfind-secondary.1.8.1"
  "opam-depext.1.1.5"
  "zarith.1.10"
]
pinned: [
  "coq.dev"
  "coq-graph-theory.dev"
  "dune.2.5.1"
  "elpi.1.12.0"
  "num.0"
  "ocamlfind.1.8.1"
  "zarith.1.10"
]
package "coq" {
  opam-version: "2.0"
  version: "dev"
  synopsis: "The Coq Proof Assistant"
  description: """
Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming
languages (e.g. the CompCert compiler certification project, or the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g. the full formalization of the Feit-Thompson theorem
or homotopy type theory) and teaching."""
  maintainer: "The Coq development team "
  authors: "The Coq development team, INRIA, CNRS, and contributors."
  license: "LGPL-2.1"
  homepage: "https://coq.inria.fr/"
  bug-reports: "https://github.com/coq/coq/issues"
  depends: [
    "ocaml" {>= "4.05.0"}
    "ocamlfind" {build}
    "zarith" {>= "1.10"}
    "conf-findutils" {build}
  ]
  build: [
    ["./configure" "-prefix" prefix "-coqide" "no"]
    [make "-j%{jobs}%"]
    [make "-j%{jobs}%" "byte"]
  ]
  install: [
    [make "install"]
    [make "install-byte"]
  ]
  dev-repo: "git+https://github.com/coq/coq.git"
  url {
    src:
      "git+https://github.com/coq/coq#2eeeba76598258bd5691a9825fd888c350fbcef3"
  }
}
package "coq-graph-theory" {
  opam-version: "2.0"
  version: "dev"
  synopsis: "Graph theory results in Coq and MathComp"
  description: """
A library of formalized graph theory results, including various
standard results from the literature (e.g., Menger’s Theorem, Hall’s
Marriage Theorem, and the excluded minor characterization of
treewidth-two graphs) as well as some more recent results arising
from the study of relation algebra within the ERC CoVeCe project
(e.g., soundness and completeness of an axiomatization of graph
isomorphism)."""
  maintainer: "christian.doczkal@inria.fr"
  authors: ["Christian Doczkal" "Damien Pous"]
  license: "CECILL-B"
  tags: [
    "category:Computer Science/Graph Theory"
    "keyword:graph theory"
    "keyword:minors"
    "keyword:treewidth"
    "keyword:algebra"
    "logpath:GraphTheory"
  ]
  homepage: "https://github.com/coq-community/graph-theory"
  bug-reports: "https://github.com/coq-community/graph-theory/issues"
  depends: [
    "coq" {(>= "8.11" & < "8.13~") | (= "dev")}
    "coq-mathcomp-ssreflect" {(>= "1.10" & < "1.12~") | (= "dev")}
    "coq-mathcomp-finmap"
    "coq-hierarchy-builder" {>= "0.10"}
  ]
  build: [make "-j%{jobs}%"]
  install: [make "install"]
  dev-repo: "git+https://github.com/coq-community/graph-theory.git"
  url {
    src:
      "git+https://github.com/coq-community/graph-theory.git#hierarchy-builder"
  }
}

chdoc commented 3 years ago

Well, the thing is, that according to the opam repository for coq-elpi, the minium requirement for coq-elpi is 1.12.0 (since Friday): https://github.com/LPCIC/coq-elpi/blob/coq-master/coq-elpi.opam

depends: [
  "elpi" {>= "1.12.0" & < "1.13.0~"}
  "coq" {= "dev"}
  ]

Further, my CI run performs and opam update and locally my opam does install the right version of elpi when I pin the development version of graph-theory. So there is still something amiss here.

chdoc commented 3 years ago

So this is not so much about fixing my CI, but about understanding how the opam in the docker container can see different dev packages than my opam on the outside.

erikmd commented 3 years ago

Well, the thing is, that according to the opam repository for coq-elpi, the minium requirement for coq-elpi is 1.12.0 (since Friday): https://github.com/LPCIC/coq-elpi/blob/coq-master/coq-elpi.opam
depends: [
  "elpi" {>= "1.12.0" & < "1.13.0~"}
  "coq" {= "dev"}
  ]

No, opam does not take into account the committed coq-elpi.opam in the upstream git repository (this would only be done in the case of opam's git pinning).

In your context, opam will rely on the package specification from the extra-dev repository: https://github.com/coq/opam-coq-archive/blob/5fe8b6e10d36aa579ff87a1ec31c29b5aa79f5eb/extra-dev/packages/coq-elpi/coq-elpi.dev/opam#L12-L15

depends: [
  "elpi"
  "coq" {= "dev"}
]

so I guess you should open a PR to fix this dependency in opam-coq-archive.

chdoc commented 3 years ago

Thank you, that was the bit I was missing. In retrospect this should have been clear, since gathering the sources for the dev version happens after dependency resolution. Still doesn't answer the question why the opam in the docker image doesn't try to satisfy the dependency using the latest stable version of elpi in the same way my local opam installation does. :confused:

erikmd commented 3 years ago

Still doesn't answer the question why the opam in the docker image doesn't try to satisfy the dependency using the latest stable version of elpi in the same way my local opam installation does.

As I mentioned in my previous message, this looks definitely unrelated to the docker packaging (which is just an encapsulation of a fresh opam switch in a Debian 10 environment), but it is related to the way opam computes the dependencies, in a way that looks suboptimal for us, indeed (albeit which was reproducible, both in GitHub Actions CI and locally with docker run, also if we'd take the result of the opam switch export dump in my previous comment https://github.com/coq-community/docker-coq/issues/16#issuecomment-736938821, import it a new opam 2.0.7 switch outside of docker, I guess the outcome would also be reproducible).

Anyway, if you think this looks as a bug of opam's way of computing dependencies, you might just as well want to open an issue in https://github.com/ocaml/opam/issues ?

chdoc commented 3 years ago

Sorry, for not closing the issue immediately. You are right, this is almost surely not related to the docker packaging, assuming the docker packaging does not tamper with any options regarding the solver for dependency resolution. I might try to reproduce this if I have a bit more time. For now I hope that fixing the dependency in the coq-opam-archive resolve the issue.

coq-community / docker-coq

Wrong elpi dependency for coq-elpi in coqorg/coq:dev #16