Stream: MetaCoq

Topic: Trying out metacoq


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jul 23 2020 at 07:11):

This topic was moved here from #Coq users > Trying out metacoq by Théo Zimmermann

view this post on Zulip 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?

view this post on Zulip Tadeusz Litak (Jul 24 2020 at 20:22):

(the version of MetaCoq that opam sees for me is 1.0~alpha+8.9)

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:24):

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.

view this post on Zulip 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

view this post on Zulip Tadeusz Litak (Jul 24 2020 at 20:30):

this is precisely the mystery that is puzzling me

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:31):

And opam info coq-metacoq?

view this post on Zulip 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"

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:36):

Have you tried installing specifically 1.0~alpha2+8.11?

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:37):

I think the syntax is

opam install coq-metacoq.1.0~alpha2+8.11

view this post on Zulip Tadeusz Litak (Jul 24 2020 at 20:39):

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]

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:43):

Perhaps then you should consider installing only metacoq.template:

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:43):

coq-metacoq-template

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 20:44):

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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.11

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jul 24 2020 at 20:55):

or maybe it prefers equations 8.8.dev over 1.2.***

view this post on Zulip 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)

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 21:01):

I don't why it would chose the oldest version rather than the most recent…

view this post on Zulip 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+"

view this post on Zulip Matthieu Sozeau (Jul 24 2020 at 21:11):

Oops :)

view this post on Zulip Matthieu Sozeau (Jul 24 2020 at 21:11):

That is not what I expected

view this post on Zulip Théo Winterhalter (Jul 24 2020 at 21:38):

I see!

view this post on Zulip Karl Palmskog (Jul 24 2020 at 21:50):

you probably wanted ~alpha1+8.9, I think then it would have worked.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 24 2020 at 22:54):

Annoyingly, everything works fine 90-99.99% of the time. Mostly.

view this post on Zulip Paolo Giarrusso (Jul 24 2020 at 22:54):

(And to be sure, “your mistake” wasn’t actually your fault.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.11

seems 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]

view this post on Zulip Karl Palmskog (Jul 28 2020 at 16:36):

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

view this post on Zulip 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: Aug 11 2022 at 02:03 UTC