Ember Edison (Jun 20 2021 at 17:08): 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."
Yannick Forster (Jun 20 2021 at 17:11):What's your OCaml version?
Yannick Forster (Jun 20 2021 at 17:11):ocamlc -v should tell you
Ember Edison (Jun 20 2021 at 17:59):4.08.1
Yannick Forster (Jun 20 2021 at 18:29):Mh, that should be fine
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?
Yannick Forster (Jun 20 2021 at 18:29):And just to be safe, run opam update first
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
[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.
Ember Edison (Jun 20 2021 at 19:10):The most terrible thing is that I have just successfully installed coq-hott without any errors.
Théo Winterhalter (Jun 20 2021 at 19:17):What does
opam info coq-metacoq
say?
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.
Théo Winterhalter (Jun 20 2021 at 19:26):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.)
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
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.)
Gaëtan Gilbert (Jun 20 2021 at 19:33):what's your coq version?
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?
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
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.
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
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
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.
Can you give us the output of opam switch?
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)
Yannick Forster (Jun 21 2021 at 11:43):And there is no warning that your environment is out of sync?
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?
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.
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"
]
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
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" ?
Michael Soegtrop (Jun 21 2021 at 16:16):This looks fine. Can you show the output of opam repo (with the switch selected)?
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.
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 as4.12.0, but I don't really see a reason why the error would come up on4.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
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
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
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?
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...
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?
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.
Michael Soegtrop (Jun 22 2021 at 15:09):I will do a local test on my machine.
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
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.
[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 =====
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?
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
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
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.
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~"}
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.
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.
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
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
Matthieu Sozeau (Jun 25 2021 at 08:54):The current metacoq is no longer affected, so we'll just need a new release
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.
Matthieu Sozeau (Jun 25 2021 at 09:53):Alright, we should have a beta3 ready soon
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
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: Apr 19 2024 at 19:02 UTC