Stream: MetaCoq

Topic: opam install not working


view this post on Zulip Ember Edison (Jun 20 2021 at 17:08):

I am installing metacoq on a new computer. But no matter I run

opam install coq-metacoq
opam install coq-metacoq.1.0~beta2+8.13
opam pin add coq-metacoq https://github.com/MetaCoq/metacoq.git

it shows
"Sorry, no solution found: there seems to be a problem with your request."

view this post on Zulip Yannick Forster (Jun 20 2021 at 17:11):

What's your OCaml version?

view this post on Zulip Yannick Forster (Jun 20 2021 at 17:11):

ocamlc -v should tell you

view this post on Zulip Ember Edison (Jun 20 2021 at 17:59):

4.08.1

view this post on Zulip Yannick Forster (Jun 20 2021 at 18:29):

Mh, that should be fine

view this post on Zulip Yannick Forster (Jun 20 2021 at 18:29):

Can you try opam install coq-metacoq -v -v -v -v and send the full output here?

view this post on Zulip Yannick Forster (Jun 20 2021 at 18:29):

And just to be safe, run opam update first

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 18:33):

I assume you also did

opam repo add coq-released https://coq.inria.fr/opam/released

view this post on Zulip Ember Edison (Jun 20 2021 at 19:05):

opam pin add coq-metacoq 1.0~beta2+8.13 -v -v -v -v

[WARNING] Running as root is not recommended
[NOTE] Pinning unchanged
coq-metacoq is now pinned to version 1.0~beta2+8.13

[NOTE] Pinning command successful, but your installed packages may be out of sync.
'opam pin add coq-metacoq 1.0~beta2+8.13 -v -v -v -v' failed.

view this post on Zulip Ember Edison (Jun 20 2021 at 19:10):

The most terrible thing is that I have just successfully installed coq-hott without any errors.

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 19:17):

What does

opam info coq-metacoq

say?

view this post on Zulip Ember Edison (Jun 20 2021 at 19:22):

[WARNING] Running as root is not recommended

<><> coq-metacoq: information on all versions <><><><><><><><><><><><><><><><><>
name coq-metacoq
all-versions 1.0~alpha1+8.8 1.0~alpha1+8.9 1.0~alpha2+8.10 1.0~alpha2+8.11 1.0~beta1+8.11 1.0~beta1+8.12
1.0~beta2+8.11 1.0~beta2+8.12 1.0~beta2+8.13

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version 1.0~beta2+8.13
repository coq-released
pin https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz
url.src: "https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz"
url.checksum: "sha256=15e1cfde70e6c4dbf33bff1a77266ac5c0c3e280586ef059e0cdec07bee814f2"
homepage: "https://metacoq.github.io/metacoq"
bug-reports: "https://github.com/MetaCoq/metacoq/issues"
dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.11"
authors: "Abhishek Anand <aa755@cs.cornell.edu>"
"Simon Boulier <simon.boulier@inria.fr>"
"Cyril Cohen <cyril.cohen@inria.fr>"
"Yannick Forster <forster@ps.uni-saarland.de>"
"Fabian Kunze <fkunze@fakusb.de>"
"Gregory Malecha <gmalecha@gmail.com>"
"Matthieu Sozeau <matthieu.sozeau@inria.fr>"
"Nicolas Tabareau <nicolas.tabareau@inria.fr>"
"Théo Winterhalter <theo.winterhalter@inria.fr>"
maintainer: "matthieu.sozeau@inria.fr"
license: "MIT"
depends: "coq-metacoq-template" {= version}
"coq-metacoq-pcuic" {= version}
"coq-metacoq-safechecker" {= version}
"coq-metacoq-erasure" {= version}
"coq-metacoq-translations" {= version}
synopsis A meta-programming framework for Coq
description MetaCoq is a meta-programming framework for Coq.
The meta-package includes the template-coq library, unverified checker for Coq,
PCUIC development including a verified translation from Coq to PCUIC,
safe checker and erasure for PCUIC and example translations.
See individual packages for more detailed descriptions.

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 19:26):

What happens if you try to install just template?

opam install coq-metacoq-template

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 19:27):

(I have no idea what could be wrong so I'm just trying to pinpoint the problem, others mights have better intuition.)

view this post on Zulip Ember Edison (Jun 20 2021 at 19:28):

Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting

view this post on Zulip Ember Edison (Jun 20 2021 at 19:29):

(I don’t want to accuse anything, but I successfully installed coq-bignums just now, I don’t think this is just my problem.)

view this post on Zulip Gaëtan Gilbert (Jun 20 2021 at 19:33):

what's your coq version?

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 19:33):

I'm guessing this is a dependency problem that the solver doesn't explain well (as in https://github.com/ocaml/opam/issues/3912). It might be a conflict with another package you have on your switch. Which version of equations do you have installed?

view this post on Zulip Ember Edison (Jun 21 2021 at 01:35):

# opam config report
# opam-version      2.0.5
# self-upgrade      no
# system            arch=x86_64 os=linux os-distribution=ubuntu os-version=20.04
# 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              11
# repositories      2 (http) (default repo at 2f66dcb5)
# pinned            3 (version)
# current-switch    with-coq

view this post on Zulip Ember Edison (Jun 21 2021 at 01:36):

Gaëtan Gilbert said:

what's your coq version?

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.8.13.2"
  "coq-bignums.8.13.0"
  "coq-hott.8.13"
  "coqide.8.13.2"
  "ocaml-base-compiler.4.05.0"
  "opam-depext.1.1.5"
]

view this post on Zulip Ember Edison (Jun 21 2021 at 01:59):

opam pin add coq-metacoq https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz

[WARNING] Running as root is not recommended
[NOTE] Package coq-metacoq is already pinned to https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz
       (version 1.0~beta2+8.13).
[coq-metacoq.1.0~beta2+8.13] downloaded from https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz
coq-metacoq is now pinned to https://github.com/MetaCoq/metacoq/archive/v1.0-beta2-8.13.tar.gz (version 1.0~beta2+8.13)

Sorry, no solution found: there seems to be a problem with your request.

[NOTE] Pinning command successful, but your installed packages may be out of sync.

view this post on Zulip Yannick Forster (Jun 21 2021 at 05:40):

The OCaml compiler of your opam switch is on version 4.05. That's too low for MetaCoq.

view this post on Zulip Yannick Forster (Jun 21 2021 at 06:21):

This also likely means that your opam environment is out of sync and you need to run eval $(opam env) again. Afterwards, ocamlc -v should show 4.05 as well

view this post on Zulip Yannick Forster (Jun 21 2021 at 06:22):

opam switch create formetacoq 4.07.1 will create a fresh opam switch with the right compiler version. You'll then have to re-add the repositories and re-install the right packages

view this post on Zulip Ember Edison (Jun 21 2021 at 11:22):

I'm delete old switch and re-install everything about opam. It doesn't work.

ocamlc -v

The OCaml compiler, version 4.12.0
Standard library directory: /root/.opam/with-coq/lib/ocaml

opam install coq-metacoq -v -v -v -v

+ /usr/bin/lsb_release "-s" "-r"
- 20.04
+ /root/.opam/with-coq/bin/ocamlc "-vnum"
- 4.12.0
Sorry, no solution found: there seems to be a problem with your request.

No solution found, exiting
'opam install coq-metacoq -v -v -v -v' failed.

view this post on Zulip Yannick Forster (Jun 21 2021 at 11:39):

Can you give us the output of opam switch?

view this post on Zulip Ember Edison (Jun 21 2021 at 11:42):

#  switch    compiler                    description
  with-coq  ocaml-base-compiler.4.12.0  with-coq

(I swear I did delete and reinstall)

view this post on Zulip Yannick Forster (Jun 21 2021 at 11:43):

And there is no warning that your environment is out of sync?

view this post on Zulip Théo Winterhalter (Jun 21 2021 at 11:46):

If you print the thing that said you had ocam 4.05 what does it say now?

view this post on Zulip Michael Soegtrop (Jun 21 2021 at 12:11):

Can you show the result of opam list? Usually if there is such a conflict it means that some dependency is pinned to an incompatible version, maybe coq-equations.

view this post on Zulip Ember Edison (Jun 21 2021 at 13:18):

Michael Soegtrop said:

Can you show the result of opam list? Usually if there is such a conflict it means that some dependency is pinned to an incompatible version, maybe coq-equations.

# Packages matching: installed
# Name                  # Installed   # Synopsis
base-bigarray           base
base-threads            base
base-unix               base
cairo2                  0.6.2         Binding to Cairo, a 2D Vector Graphics Library
conf-adwaita-icon-theme 1             Virtual package relying on adwaita-icon-theme
conf-cairo              1             Virtual package relying on a Cairo system installation
conf-findutils          1             Virtual package relying on findutils
conf-gmp                3             Virtual package relying on a GMP lib system installation
conf-gtk3               18            Virtual package relying on GTK+ 3
conf-gtksourceview3     0+2           Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config         2             Check if pkg-config is installed and create an opam switch local pkgconfig folder
coq                     8.13.2        Formal proof management system
coq-bignums             8.13.0        Bignums, the Coq library of arbitrary large numbers
coq-equations           1.3~beta+8.13 A function definition package for Coq
coq-hott                8.13          The Homotopy Type Theory library
coqide                  8.13.2        IDE of the Coq formal proof management system
csexp                   1.5.1         Parsing and printing of S-expressions in Canonical form
dune                    2.8.5         Fast, portable, and opinionated build system
dune-configurator       2.8.5         Helper library for gathering system configuration
lablgtk3                3.1.1         OCaml interface to GTK+3
lablgtk3-sourceview3    3.1.1         OCaml interface to GTK+ gtksourceview library
num                     1.4           The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                   4.12.0        The OCaml compiler (virtual package)
ocaml-base-compiler     4.12.0        Official release 4.12.0
ocaml-config            2             OCaml Switch Configuration
ocaml-options-vanilla   1             Ensure that OCaml is compiled with no special options enabled
ocamlfind               1.9.1         A library manager for OCaml
opam-depext             1.1.5         install OS distribution packages
result                  1.5           Compatibility Result module
zarith                  1.12          Implements arithmetic and logical operations over arbitrary-precision integers

Théo Winterhalter said:

If you print the thing that said you had ocam 4.05 what does it say now?

Because I deleted the switch, this is now (~~~~/.opam-switch/switch-state)

opam-version: "2.0"
compiler: [
  "base-bigarray.base"
  "base-threads.base"
  "base-unix.base"
  "ocaml.4.12.0"
  "ocaml-base-compiler.4.12.0"
  "ocaml-config.2"
  "ocaml-options-vanilla.1"
]
roots: [
  "coq.8.13.2"
  "coq-bignums.8.13.0"
  "coq-equations.1.3~beta+8.13"
  "coq-hott.8.13"
  "coqide.8.13.2"
  "ocaml-base-compiler.4.12.0"
  "opam-depext.1.1.5"
]

view this post on Zulip Yannick Forster (Jun 21 2021 at 13:24):

I only have the idea to try 4.07.1, not something as new as 4.12.0, but I don't really see a reason why the error would come up on 4.12

view this post on Zulip Matthieu Sozeau (Jun 21 2021 at 13:49):

That's quite surprising, your package list looks fine. Maybe try opam install coq-metacoq.1.0~beta2+8.13 --ignore-constraints-on="coq coq-equations" ?

view this post on Zulip Michael Soegtrop (Jun 21 2021 at 16:16):

This looks fine. Can you show the output of opam repo (with the switch selected)?

view this post on Zulip Michael Soegtrop (Jun 21 2021 at 16:19):

In order to nail this down, I would install these dependencies manually:

  "coq-metacoq-template" {= version}
  "coq-metacoq-pcuic" {= version}
  "coq-metacoq-safechecker" {= version}
  "coq-metacoq-erasure" {= version}
  "coq-metacoq-translations" {= version}

If one of these fails, you can install the dependencies of this. This process should lead to a dependency you cannot install.

view this post on Zulip Ember Edison (Jun 21 2021 at 17:06):

Yannick Forster said:

I only have the idea to try 4.07.1, not something as new as 4.12.0, but I don't really see a reason why the error would come up on 4.12

I use the latest version of the compiler, so I can tell my mentor "It's all the fault of the metacoq development team"
(~ ̄▽ ̄)~Then I can rest for a while.
Matthieu Sozeau said:

That's quite surprising, your package list looks fine. Maybe try opam install coq-metacoq.1.0~beta2+8.13 --ignore-constraints-on="coq coq-equations" ?

It doesn't work.
But at least I manually compiled it successfully, so the problem should all be attributed to opam.
image.png

view this post on Zulip Ember Edison (Jun 21 2021 at 17:11):

Michael Soegtrop said:

This looks fine. Can you show the output of opam repo (with the switch selected)?

coq-metacoq-template ok
coq-metacoq-pcuic ok
coq-metacoq-safechecker failure
coq-metacoq-erasure failure
coq-metacoq-translations ok
coq-metacoq failure

># opam upgrade
[WARNING] Running as root is not recommended
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-equations.1.3~beta+8.13
     coq-metacoq-pcuic.1.0~beta2+8.13 is installed and requires coq-equations (>= 1.2.3 & < 1.3~)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the
conflicting packages.
Nothing to do.
># opam list
[WARNING] Running as root is not recommended
# Packages matching: installed
# Name                   # Installed    # Synopsis
base-bigarray            base
base-threads             base
base-unix                base
cairo2                   0.6.2          Binding to Cairo, a 2D Vector Graphics Library
conf-adwaita-icon-theme  1              Virtual package relying on adwaita-icon-theme
conf-cairo               1              Virtual package relying on a Cairo system installation
conf-findutils           1              Virtual package relying on findutils
conf-gmp                 3              Virtual package relying on a GMP lib system installation
conf-gtk3                18             Virtual package relying on GTK+ 3
conf-gtksourceview3      0+2            Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config          2              Check if pkg-config is installed and create an opam switch local pkgconfig folde
coq                      8.13.2         Formal proof management system
coq-bignums              8.13.0         Bignums, the Coq library of arbitrary large numbers
coq-equations            1.2.4+8.13     A function definition package for Coq
coq-hott                 8.13           The Homotopy Type Theory library
coq-metacoq-pcuic        1.0~beta2+8.13 A type system equivalent to Coq's and its metatheory
coq-metacoq-template     1.0~beta2+8.13 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.0~beta2+8.13 Translations built on top of MetaCoq
coqide                   8.13.2         IDE of the Coq formal proof management system
csexp                    1.5.1          Parsing and printing of S-expressions in Canonical form
dune                     2.8.5          Fast, portable, and opinionated build system
dune-configurator        2.8.5          Helper library for gathering system configuration
lablgtk3                 3.1.1          OCaml interface to GTK+3
lablgtk3-sourceview3     3.1.1          OCaml interface to GTK+ gtksourceview library
num                      1.4            The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.12.0         The OCaml compiler (virtual package)
ocaml-base-compiler      4.12.0         Official release 4.12.0
ocaml-config             2              OCaml Switch Configuration
ocaml-options-vanilla    1              Ensure that OCaml is compiled with no special options enabled
ocamlfind                1.9.1          A library manager for OCaml
opam-depext              1.1.5          install OS distribution packages
result                   1.5            Compatibility Result module
zarith                   1.12           Implements arithmetic and logical operations over arbitrary-precision integers

view this post on Zulip Ember Edison (Jun 21 2021 at 17:24):

Ember Edison said:

Yannick Forster said:

>

I use the latest version of the compiler, so I can tell my mentor "It's all the fault of the metacoq development team"
(~ ̄▽ ̄)~Then I can rest for a while.
Matthieu Sozeau said:

>

It doesn't work.

But at least I manually compiled it successfully, so the problem should all be attributed to opam.

That’s great, it seems I destroyed something while fighting with opam
image.png

view this post on Zulip Matthieu Sozeau (Jun 22 2021 at 07:24):

Yes, it seems to be an opam problem. Did you make and make install metacoq while building with a coq from an opam switch?

view this post on Zulip Matthieu Sozeau (Jun 22 2021 at 07:26):

Oh I see now, the problem is with coq-equations. You should use 1.2.4+8.13 rather than the new beta release...

view this post on Zulip Michael Soegtrop (Jun 22 2021 at 10:08):

So the issue seems to be that in coq-equations a beta release is the "best release available" according to opam's rules - which I find questionable but is not uncommon - and at the same time coq-metacoq-pcuic.1.0~beta2+8.13 says that it doesn't want a 8.13 beta release of coq-equations. But what I don't understand is why opam doesn't suggest to "downgrade" coq-equations to 1.2.4+8.13?

view this post on Zulip Ember Edison (Jun 22 2021 at 13:47):

I deleted the switch again, reinstall everything again, and pin coq-equations to 1.2.4+8.13...It doesn't work. opam refuses to install coq-metacoq-safechecker and coq-metacoq-erasure.

But manual compilation is success, if you can't retrore this problem, I can only give up.

view this post on Zulip Michael Soegtrop (Jun 22 2021 at 15:09):

I will do a local test on my machine.

view this post on Zulip Michael Soegtrop (Jun 23 2021 at 08:16):

There seems to be a weird dependency on the OCaml version. With OCaml 4.07 it works fine, with OCaml 4.10 it wants to reinstall half of the packages (but still finds a solution). I couldn't find a setup in which opam doesn't find a solution, but I did not try OCaml newer than 4.10. I attached two logs based on different versions of Coq Platform, which differ only in the OCaml version and the version of the platform opam patch repo, but neither contains relevant packages. The two files are best viewed with a diff tool.

@Ember Edison : it might still be that you have odd repos - this doesn't necessarily go away when you create a new switch. So please post the output of opam repo - I didn't find this in your above posts. When you registered a repo for all switches, it will also apply to new switches.

The good news is that with a plain Coq Platform 2021.02, coq-metacoq installs as expected, so I would recommend to use just that.

Install_2021_02.txt
Install_main.txt

view this post on Zulip Ember Edison (Jun 24 2021 at 10:51):

Michael Soegtrop said:

.......

in OCaml 4.10, opam install coq-metacoq is work.
But the new interesting thing is that opam asked me to downgrade when I tried to install coq-hott.

opam install coq-hott

[WARNING] Running as root is not recommended
The following actions will be performed:
∗ install conf-autoconf 0.1 [required by coq-hott]
↘ downgrade coq 8.12.2 to 8.11.2 [required by coq-hott]
∗ install coq-hott 8.11
↗ upgrade coq-equations 1.2.3+8.12 to 1.2.4+8.11 [uses coq]
↘ downgrade coqide 8.12.2 to 8.11.2 [uses coq]
↘ downgrade coq-metacoq-template 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-bignums 8.12.0 to 8.11.0 [uses coq]
↘ downgrade coq-metacoq-checker 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-metacoq-translations 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-metacoq-pcuic 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-metacoq-safechecker 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-metacoq-erasure 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
↘ downgrade coq-metacoq 1.0~beta1+8.12 to 1.0~beta1+8.11 [uses coq]
===== ∗ 2 ↗ 1 ↘ 10 =====

opam-test.txt

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 11:03):

@Ember Edison : yes, that's the same what I saw as well (and reported). With OCaml 4.07.1 it works fine, though. Please have a look at the logs I attached to my post. You might want to use Coq Platform to setup Coq - it is since 8.13 the recommended way to setup Coq and gives you the environment most people and most automatic test systems use. Of cause it should also work with different OCaml. Coq Platform 2021.02 (Coq 8.13) still uses OCaml 4.07.1, but Coq Platform 2021.08 will use 4.10.

@Matthieu Sozeau : will you have a look at the opam files, or should I do this?

view this post on Zulip Matthieu Sozeau (Jun 24 2021 at 12:24):

I'm not sure what we should do here, except provide a coq-hott for 8.12

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 13:57):

@Matthieu Sozeau : I would say the culprit is this line: (https://github.com/coq/opam-coq-archive/blob/b8c9b6503d23e9fe7581c1a3579fc9c17899fb6e/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.0%7Ebeta2%2B8.13/opam#L25) which restricts coq-metacoq (via dependency) to ocaml < 4.10

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 13:58):

Some other files have restrictions to ocaml < 4.12, but coq-metacoq-safechecker has on various versions ocaml < 4.10. I would think about changing this (to < 4.12) for all affected versions unless there is a good reason to keep that.

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 14:01):

Here is a complete list of coq-metacoq packages with OCaml version upper bounds (a minority):

packages$ grep "ocaml.*<" coq-metacoq*/*/opam
coq-metacoq-erasure/coq-metacoq-erasure.1.0~beta2+8.12/opam:  "ocaml" {>= "4.07.1" & < "4.12~"}
coq-metacoq-pcuic/coq-metacoq-pcuic.1.0~beta2+8.12/opam:  "ocaml" {>= "4.07.1" & < "4.12~"}
coq-metacoq-safechecker/coq-metacoq-safechecker.1.0~beta2+8.11/opam:  "ocaml" {>= "4.07.1" & < "4.10~"}
coq-metacoq-safechecker/coq-metacoq-safechecker.1.0~beta2+8.12/opam:  "ocaml" {>= "4.07.1" & < "4.10~"}
coq-metacoq-safechecker/coq-metacoq-safechecker.1.0~beta2+8.13/opam:  "ocaml" {>= "4.07.1" & < "4.10~"}
coq-metacoq-template/coq-metacoq-template.1.0~alpha2+8.11/opam:  "ocaml" {>= "4.07.1" & < "4.10"}
coq-metacoq-translations/coq-metacoq-translations.1.0~beta2+8.12/opam:  "ocaml" {>= "4.07.1" & < "4.12~"}
coq-metacoq/coq-metacoq.1.0~beta2+8.12/opam:  "ocaml" {>= "4.07.1" & < "4.12~"}

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 14:04):

I would suggest to remove all ocaml upper bounds unless there is evidence that these are required. You can do this without changing the version of the opam package, since it won't change anything for systems where it did install fine before.

view this post on Zulip Michael Soegtrop (Jun 24 2021 at 14:17):

Btw.: the Coq opam repo CI checks with these OCaml version:

opam-build:4.05.0
opam-build:4.07.1
opam-build:4.09.0
opam-build:4.11.2

So in order to know if it works with these versions, just make a PR and see what CI says.

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 08:49):

Ah right indeed. We found an incompatibility with 4.10 at some point, maybe we just need <> 4.10 instead

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 08:54):

The issue affects anything above 4.10, as a warning was made fatal in those versions: https://github.com/MetaCoq/metacoq/issues/541

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 08:54):

The current metacoq is no longer affected, so we'll just need a new release

view this post on Zulip Michael Soegtrop (Jun 25 2021 at 09:17):

In Coq Platform I wanted to use 4.10, which is the latest version available on all supported platforms. So it would be good to have a meta-coq working with 4.10, since I want to add it to Coq Platform 2021.08.

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 09:53):

Alright, we should have a beta3 ready soon

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 15:32):

For 2021.08, I think we should have Equations 1.3 "final" + a new beta for metacoq relying on it

view this post on Zulip Michael Soegtrop (Jun 25 2021 at 16:03):

Indeed for equations we should have a non beta release.
For MetCoq the plan is to put it into the extended section (2021.08 has levels Coq/Full/Extended) where a beta release would be acceptable.


Last updated: Aug 11 2022 at 03:02 UTC