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

What's your OCaml version?

`ocamlc -v`

should tell you

4.08.1

Mh, that should be fine

Can you try `opam install coq-metacoq -v -v -v -v`

and send the full output here?

And just to be safe, run `opam update`

first

I assume you also did

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

[WARNING] Running as root is not recommended

[NOTE] Pinning unchanged

coq-metacoq is now pinned to version 1.0~beta2+8.13

- /usr/bin/lsb_release "-s" "-r"
- 20.04
- /usr/bin/ocamlc "-vnum"
- 4.08.1

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.

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

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

What does

```
opam info coq-metacoq
```

say?

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

What happens if you try to install just template?

```
opam install coq-metacoq-template
```

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

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

No solution found, exiting

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

what's your coq version?

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?

```
# 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
```

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"
]
```

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

The OCaml compiler of your opam switch is on version `4.05`

. That's too low for MetaCoq.

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

`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

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

Can you give us the output of `opam switch`

?

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

(I swear I did delete and reinstall)

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

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

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.

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"
]
```

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`

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"`

?

This looks fine. Can you show the output of `opam repo`

(with the switch selected)?

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.

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

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
```

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

Yes, it seems to be an opam problem. Did you `make`

and `make install`

metacoq while building with a `coq`

from an opam switch?

Oh I see now, the problem is with `coq-equations`

. You should use `1.2.4+8.13`

rather than the new beta release...

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?

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.

I will do a local test on my machine.

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

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.

[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 =====

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

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

@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

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.

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~"}
```

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.

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.

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

instead

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

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

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.

Alright, we should have a beta3 ready soon

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

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: Apr 14 2024 at 11:02 UTC