Abel Nieto (Jul 22 2020 at 15:54): Abel Nieto (Jul 22 2020 at 15:54):I'm trying to compile the demo file for metacoq: https://github.com/MetaCoq/metacoq/tree/master/examples/demo.v
I installed metacoq via opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-metacoq
I then opened the demo.v file in PG; the imports all load, but it has trouble with the MetaCoq vernacular command:
Require Import List Arith String.
Require Import MetaCoq.Template.All.
Import ListNotations MonadNotation.
Local Open Scope string_scope.
(** This is just printing **)
MetaCoq Test Quote (fun x : nat => x).
Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
Any suggestions for how to get MetaCoq set up?
Karl Palmskog (Jul 22 2020 at 15:55):there is no guarantee that any files in MetaCoq's master branch will work with a released version of MetaCoq.
Abel Nieto (Jul 22 2020 at 15:56):Sorry, I actually tried the 8.11 branch demo: https://github.com/MetaCoq/metacoq/blob/coq-8.11/examples/demo.v
Same issue.
Karl Palmskog (Jul 22 2020 at 15:58):the 8.11 branch may also have diverged from the release. I suggest you download the tarball from the actual release, compile the release manually, then open examples/demo.v from the unpacked tarball. Or you could do the same for the coq-8.11 branch of the repo (although it's not guaranteed to work)
Théo Winterhalter (Jul 22 2020 at 21:38):(These questions would best be asked in the MetaCoq stream, if someone could move it there, ping @Théo Zimmermann )
Otherwise, the MetaCoq vernacular syntax is relatively recent, so it might be your release still has the old syntax. If you replace MetaCoq Test Quote by just Test Quote then it would be the problem.
Notification Bot (Jul 23 2020 at 07:11):This topic was moved here from #Coq users > Trying out metacoq by Théo Zimmermann
Tadeusz Litak (Jul 24 2020 at 20:20):I think that the problem is more basic. I also wanted to play around with MetaCoq and to install it via opam. The point is that the opam version seems hopelessly out of date and it insisted on downgrading my opam-installed Coq version (from 8.11.2 to 8.9.1) together with Equations (from 1.2.2 to 1.2.1) and other packages like TLC. This despite doing all updates and upgrades. Is this how things are supposed to look like or did I miss some step?
Tadeusz Litak (Jul 24 2020 at 20:22):(the version of MetaCoq that opam sees for me is 1.0~alpha+8.9)
Théo Winterhalter (Jul 24 2020 at 20:23):You probably have Coq 8.9 installed then.
I have:
opam info coq-metacoq
<><> coq-metacoq: information on all versions <><><><><><><><><><><><><><><> 🐫
name coq-metacoq
all-installed-versions 1.0~alpha2+8.11 [coq.8.11.0]
all-versions 1.0~alpha2+8.10 1.0~alpha2+8.11 1.0~alpha+8.8 1.0~alpha+8.9
So yeah, if you use the 8.9 version, it's probably out of date, and I'm not sure we're going to be releasing any new 8.9 version.
Tadeusz Litak (Jul 24 2020 at 20:29):No, as I said, the version of Coq installed via opam is 8.11.2:
opam info coq
<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><><><>
name coq
all-installed-versions 8.11.2 [system]
all-versions 8.3 8.4pl1 8.4pl2 8.4pl4 8.4.5 8.4.6~camlp4 8.4.6
8.5.0~camlp4 8.5.0 8.5.1 8.5.2~camlp4 8.5.2 8.5.3
8.6 8.6.1 8.7.0 8.7.1 8.7.1+1 8.7.1+2 8.7.2
8.8.0 8.8.1 8.8.2 8.9.0 8.9.1 8.10.0 8.10.1
8.10.2 8.11.0 8.11.1 8.11.2
<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version 8.11.2
repository default
url.src: "https://github.com/coq/coq/archive/V8.11.2.tar.gz"
url.checksum: "sha512=f8ab307b8e39ffda5f6984e187c1f8de1cb6dec5c322726dbbe535ee611683cfeeb9cee3e11ad83f5e44e843fc51e7e2d50b4ea69ab42fde38aaf3d0cf2dea3c"
homepage: "https://coq.inria.fr/"
bug-reports: "https://github.com/coq/coq/issues"
dev-repo: "git+https://github.com/coq/coq.git"
authors: "The Coq development team, INRIA, CNRS, and contributors."
maintainer: "coqdev@inria.fr"
license: "LGPL-2.1-only"
depends: "ocaml" {>= "4.05.0" & < "4.12"}
"ocamlfind" {build}
"num"
"conf-findutils" {build}
synopsis Formal proof management system
description
this is precisely the mystery that is puzzling me
Théo Winterhalter (Jul 24 2020 at 20:31):And opam info coq-metacoq?
Tadeusz Litak (Jul 24 2020 at 20:33):hmmm... indeed, it's funny:
name coq-metacoq
all-versions 1.0~alpha2+8.10 1.0~alpha2+8.11 1.0~alpha+8.8 1.0~alpha+8.9
<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version 1.0~alpha+8.9
repository coq-released
url.src: "https://github.com/MetaCoq/metacoq/archive/1.0-alpha+8.9.tar.gz"
url.checksum: "sha256=899ef4ee73b1684a0f1d2e37ab9ab0f9b24424f6d8a10a10efd474c0ed93488e"
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.8"
Have you tried installing specifically 1.0~alpha2+8.11?
Théo Winterhalter (Jul 24 2020 at 20:37):I think the syntax is
opam install coq-metacoq.1.0~alpha2+8.11
Thanks. This looks better, but it somehow still wants to downgrade my Equations, which I don't want to do (I'm supervising students working with Equations, who need an up-to-date version):
- downgrade coq-equations 1.2.2+8.11 to 1.2.1+8.11
[required by coq-metacoq-checker]
Perhaps then you should consider installing only metacoq.template:
Théo Winterhalter (Jul 24 2020 at 20:43):coq-metacoq-template
If you only want the plugin for quoting and unquoting and don't care about the checker, then it should be enough and non-dependent on Equations.
Tadeusz Litak (Jul 24 2020 at 20:45):Thx! W/o a specific version number, opam still wants to downgrade Coq, Equations and TLC, but
opam install coq-metacoq-template.1.0~alpha2+8.11
seems to work
Théo Winterhalter (Jul 24 2020 at 20:45):On a side note, I see you are working on the [system] switch of your opam. I personally create a new switch for each configuration I want, typically one for each version of coq. This has serious drawbacks as it duplicates ocaml installations but it works.
Théo Winterhalter (Jul 24 2020 at 20:47):Tadeusz Litak said:
Thx! W/o a specific version number, opam still wants to downgrade Coq, Equations and TLC, but
opam install coq-metacoq-template.1.0~alpha2+8.11seems to work
That's interesting… You should consider pinning your coq version for opam so that it never tries to downgrade it. But it's odd that it chooses the 8.9 version by default. Is it to be expected @Matthieu Sozeau ?
Gaëtan Gilbert (Jul 24 2020 at 20:53):coq-metacoq-checker has a constraint "coq-equations" { >= "1.2" & < "1.2.2" } so it makes sense that it wants to downgrade equations
on my machine it wants to downgrade coq to 8.8.dev, perhaps because it prefers the .dev version for metacoq, which is 8.8.dev
Gaëtan Gilbert (Jul 24 2020 at 20:55):or maybe it prefers equations 8.8.dev over 1.2.***
Gaëtan Gilbert (Jul 24 2020 at 20:58):I get 8.8 instead of 8.9 because I have the extra-dev repo (tested by removing the repo)
Théo Winterhalter (Jul 24 2020 at 21:01):I don't why it would chose the oldest version rather than the most recent…
Gaëtan Gilbert (Jul 24 2020 at 21:05):the older one is 1.0~alpha+8.9, the newer is 1.0~alpha2+8.11
according to the rules https://opam.ocaml.org/doc/Manual.html#version-ordering this gets split as (common prefix removed for brevity)
|-----------+---+-----+---+-----+----|
| "~alpha+" | 8 | "." | 9 | | |
| "~alpha" | 2 | "+" | 8 | "." | 11 |
|-----------+---+-----+---+-----+----|
and by lex order "~alpha" < "~alpha+"
Matthieu Sozeau (Jul 24 2020 at 21:11):Oops :)
Matthieu Sozeau (Jul 24 2020 at 21:11):That is not what I expected
Théo Winterhalter (Jul 24 2020 at 21:38):I see!
Karl Palmskog (Jul 24 2020 at 21:50):you probably wanted ~alpha1+8.9, I think then it would have worked.
Paolo Giarrusso (Jul 24 2020 at 22:52):@Tadeusz Litak I’m afraid your mistake is trusting opam. It’s not true that I pin each opam package I install, but that doesn’t mean unpinned packages are safe.
Paolo Giarrusso (Jul 24 2020 at 22:53):Once, installing and uninstalling the same package kept upgrading and downgrading num between 1.2 and 1.3.
Paolo Giarrusso (Jul 24 2020 at 22:54):Annoyingly, everything works fine 90-99.99% of the time. Mostly.
Paolo Giarrusso (Jul 24 2020 at 22:54):(And to be sure, “your mistake” wasn’t actually your fault.)
Tadeusz Litak (Jul 24 2020 at 22:58):Paolo Giarrusso said:
Tadeusz Litak I’m afraid your mistake is trusting opam.
:dizzy: fool me once, shame on you, opam; fool me twice, shame on me
won't get fooled again
Paolo Giarrusso (Jul 24 2020 at 23:06):Reading further, my comment was a bit unfair; documentation for opam version ordering exists, but it keeps surprising people. I still believe that opam’s ranking of solution is too bad: installing a package should only affect other packages if necessary. On debian, at least aptitude lets you cycle through solutions.
Tadeusz Litak (Jul 28 2020 at 16:32):Tadeusz Litak said:
Thx! W/o a specific version number, opam still wants to downgrade Coq, Equations and TLC, but
opam install coq-metacoq-template.1.0~alpha2+8.11seems to work
An ironic PS is that after this trick, of course opam insists on removing MetaCoq Template if I want to update Coq to the newest version. Equations have the same problem btw:
opam upgrade coq
...
The following actions will be performed:
- remove coq-metacoq-template 1.0~alpha2+8.11 [conflicts with coq]
- remove coq-equations 1.2.2+8.11 [conflicts with coq]
@Tadeusz Litak unfortunately there is no version of either MetaCoq or Equations released on OPAM that is compatible with Coq 8.12.0 - yet. At least Equations will hopefully be released quite soon for 8.12. In the meantime, you can always clone the respective repos and try the branches for 8.12, e.g., branch 8.12 for Equations, if you want to use Coq 8.12.0.
Tadeusz Litak (Jul 28 2020 at 16:39):Karl Palmskog said:
unfortunately there is no version of either MetaCoq or Equations released on OPAM that is compatible with Coq 8.12.0 - yet. At least Equations will hopefully be released quite soon for 8.12.
Oh, I see. Thanks. This means I'll probably stick with 8.11.2 for a little longer. As I am teaching a SF-based lecture for two more weeks, switching horses right now might not be the best idea anyway.
Last updated: Apr 18 2024 at 06:01 UTC