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?

there is no guarantee that any files in MetaCoq's `master`

branch will work with a released version of MetaCoq.

Sorry, I actually tried the 8.11 branch demo: https://github.com/MetaCoq/metacoq/blob/coq-8.11/examples/demo.v

Same issue.

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)

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

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

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?

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

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.

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

And `opam info coq-metacoq`

?

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`

?

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:

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

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

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.

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 ?

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

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

I get 8.8 instead of 8.9 because I have the extra-dev repo (tested by removing the repo)

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

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

Oops :)

That is not what I expected

I see!

you probably wanted `~alpha1+8.9`

, I think then it would have worked.

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

Once, installing and uninstalling the same package kept upgrading and downgrading num between 1.2 and 1.3.

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

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

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

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

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

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: Oct 13 2024 at 01:02 UTC