Stream: MetaCoq

Topic: opam install metacoq-template does not work on MacOs


view this post on Zulip Pierre Vial (Apr 21 2022 at 11:52):

Hi,
I'm trying to install various packages on a new opam switch on a MacOS, which should be identical with one of my former computer (whose OS is debian)

Actually, all this is related to the Coq package sniper, which is found here and depends on many other packages. If I'm correct, sniper depends on 81 other packages, but the only one whose installation fails is coq-metacoq-template (for instance, there does not seem to have a problem with pcuic).

I've attempted various formulas e.g. ocaml 4.09.0 or 4.11.0, or just opam install coq-metacoq. or opam install coq-metacoq-templatecoq or coq-metacoq-template.1.0~beta2+8.13 (actually, I don't think metacoqis fully compatible with Coq>=4.12.0 but it's ok with Coq.4.12.0 if one just needs templatecoq, pcuic and coq-equation).

I've also tried to install coq-metacoq and coq-metacoq-template manually , with opam install ., but I've obtained this error:

/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQC theories/utils/MCPrelude.v
File "./theories/utils/MCPrelude.v", line 75, characters 0-41:
Error: This command does not support this attribute: global.
[unsupported-attributes,parsing]

Since everything seems to be fine with debian, all this makes me think that something is going on with MacOs. Any suggestions ?

view this post on Zulip Karl Palmskog (Apr 21 2022 at 11:54):

with opam install ., you are installing something from the local filesystem, usually a git repo. The following message:

Error: This command does not support this attribute: global.

indicates that your Coq version is too old for the MetaCoq files on the local filesystem.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 11:55):

With MetaCoq, it's very important to use right branch in the repo. For example, there is no chance the branch for 8.13 works on 8.14 or later (or the converse)

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:01):

I can well imagine though that the releases of MetaCoq have some problem with OCaml 4.12 (they are 1.5 years old, and came out before 4.12 was even out)

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:04):

I recommend trying the 8.13 branch, it was updated 6 months ago and might work: https://github.com/MetaCoq/metacoq/tree/coq-8.13

view this post on Zulip Pierre Vial (Apr 21 2022 at 12:11):

Thanks, I'll try this. But what suprises me the most is that I know that I can have switch with the aforementioned versions

view this post on Zulip Pierre Vial (Apr 21 2022 at 12:32):

Well, in the following opam switch:

base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-gmp            4           Virtual package relying on a GMP lib system inst
coq                 8.13.2      Formal proof management system
coq-equations       1.3+8.13    A function definition package for Coq
num                 1.4         The legacy Num library for arbitrary-precision i
ocaml               4.11.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.0      Official release 4.11.0
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations ove

I have obtained the following error (more precisely, I tried to install templatecoq.foo just after installing a switch with ocaml 4.11.0 )

opam install coq-metacoq-template.1.0~beta2+8.13
The following actions will be performed:
   install ocamlfind            1.9.3          [required by coq]
   install conf-gmp             4              [required by zarith]
   install conf-findutils       1              [required by coq]
   install num                  1.4            [required by coq]
   install zarith               1.12           [required by coq]
   install coq                  8.13.2         [required by
                                                coq-metacoq-template]
   install coq-equations        1.3+8.13       [required by
                                                coq-metacoq-template]
   install coq-metacoq-template 1.0~beta2+8.13
=====  8 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
 retrieved coq-metacoq-template.1.0~beta2+8.13  (cached)
 installed conf-gmp.4
 installed conf-findutils.1
 retrieved num.1.4  (cached)
 retrieved coq-equations.1.3+8.13  (cached)
 retrieved ocamlfind.1.9.3  (cached)
 retrieved zarith.1.12  (cached)
 retrieved coq.8.13.2  (cached)
 installed ocamlfind.1.9.3
 installed num.1.4
 installed zarith.1.12
 installed coq.8.13.2
 installed coq-equations.1.3+8.13
[ERROR] The compilation of coq-metacoq-template.1.0~beta2+8.13 failed at "make
        -j 7 template-coq".

#=== ERROR while compiling coq-metacoq-template.1.0~beta2+8.13 ================#
# context     2.1.2 | macos/x86_64 | ocaml-base-compiler.4.11.0 | https://coq.inria.fr/opam/released#2022-04-19 09:40
# path        ~/.opam/snipdev2/.opam-switch/build/coq-metacoq-template.1.0~beta2+8.13
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j 7 template-coq
# exit-code   2
# env-file    ~/.opam/log/coq-metacoq-template-54424-e8f6d1.env
# output-file ~/.opam/log/coq-metacoq-template-54424-e8f6d1.out
### output ###
# [...]
# CAMLC -c gen-src/logic1.mli
# CAMLC -c gen-src/sumbool.mli
# CAMLC -c gen-src/signature.mli
# File "gen-src/cRelationClasses.mli", line 13, characters 11-12:
# 13 | type ('a, ') coq_Reflexive = 'a -> '
#                 ^
# Error: Syntax error
# make[3]: *** [gen-src/cRelationClasses.cmi] Error 2
# make[3]: *** Waiting for unfinished jobs....
# make[2]: *** [all] Error 2
# make[1]: *** [plugin] Error 2
# make: *** [template-coq] Error 2


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
 λ build coq-metacoq-template 1.0~beta2+8.13
└─
┌─ The following changes have been performed
  install conf-findutils 1
  install conf-gmp       4
  install coq            8.13.2
  install coq-equations  1.3+8.13
  install num            1.4
  install ocamlfind      1.9.3
  install zarith         1.12
└─

view this post on Zulip Matthieu Sozeau (Apr 25 2022 at 09:30):

Pierre Vial said:

Thanks, I'll try this. But what suprises me the most is that I know that I can have switch with the aforementioned versions

It might be an issue because you are missing GNU sed (avalailble as gnu-sed on brew). BTW, we are mostly working on the 8.14 branch now.

view this post on Zulip Pierre Vial (Apr 26 2022 at 09:36):

@Matthieu Sozeau It actually works, thanks a lot!

view this post on Zulip Karl Palmskog (Apr 26 2022 at 09:42):

there is currently no conf-sed package in opam, so ideally MetaCoq would add some kind of manual check for GNU sed

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 09:51):

I would more recommend to restrict usages of sed to posix (Linux and Mac sed are posix compliant). Most stuff one does in make shouldn't be that complicated that one requires GNU extensions of sed.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 09:51):

If you need help with this, please let me know.

view this post on Zulip Karl Palmskog (Apr 26 2022 at 09:55):

maybe we can ask @Pierre Vial to test again, but with Mac sed. Then we at least know only GNU sed works.

view this post on Zulip Théo Winterhalter (Apr 26 2022 at 09:57):

The script does try to get either gsed or sed so for him it used sed and it failed.

view this post on Zulip Pierre Vial (Apr 26 2022 at 10:23):

I did install gnu-sed as Matthieu suggested.
How could I constrain MacOs to use sed instead of gsed as @Karl Palmskog suggests?

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 10:29):

@Pierre Vial if you uninstall gnu-sed the code will user normal sed, but it seemed like your original experiment? Unless you also changed something else…

view this post on Zulip Karl Palmskog (Apr 26 2022 at 10:30):

it seems we already know that Mac sed doesn't work, due to the original failure, and Théo's comment on how sed is applied (try sed, if it doesn't exist try gsed)

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 10:32):

I guess it tries gsed first, but agreed

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 10:32):

@Michael Soegtrop do you know a good cross-platform way to do sed -i, and a way to test with BSD sed (say, installing it on Linux, or sth else?)

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:32):

@Paolo Giarrusso : posix sed doesn't support -i (see https://pubs.opengroup.org/onlinepubs/9699919799/utilities/sed.html). So if you want to stay within posix, you have to use sed together with a mv -f- not that bad IMHO unless you have in place sed all over the place.

What works on MacOS, BSD and Linux (afair) is to give a backup file sed -i.bak and delete it later.

It might also make sense to rethink if you really want to do in place editing.

Of course there are also a lot of differences in the RE support.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:33):

I am not aware of an easy way to test with Mac BSD (short of Github CI) on Linux.

view this post on Zulip Théo Winterhalter (Apr 26 2022 at 11:35):

Karl Palmskog said:

it seems we already know that Mac sed doesn't work, due to the original failure, and Théo's comment on how sed is applied (try sed, if it doesn't exist try gsed)

More precisely here is how it decides:

SED=`which gsed || which sed`

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:37):

Generally, it seems clear that a package shouldn't use BSD sed if the authors don't invest the time to support it.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:39):

And I'm somewhat skeptical people would want to support it when installing gnu-sed is so easy.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:39):

Well in my (fairly extensive) experience it is not much work to make things work with whatever sed the system has. So I would avoid depending on specific sed variants and just stick to posix features or at least the common denominator of Mac/BSD and Linux.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:40):

Maybe. But if somebody chose to invest time in MetaCoq, releasing packages for 8.14 and 8.15 seems more urgent.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:40):

I think using gnu-sed is also fine, but when you rely on it please create an opam conf package for it and depend on it. Otherwise I have to clean it up later. But again, I hardly see a need for it.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:41):

Agree re creating conf-gsed.

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:42):

Still my preference is not to depend on it.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:42):

If people set up the appropriate CI, I agree that's better.

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:43):

The problem with packages for 8.14/8.15 is not lack of time in general, but the time needed to consolidate everything into a releasable state. I had a multitude of problems coming from sed when installing MetaCoq, so I think we'll gladly take every solution

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:43):

You could do a PR to Coq platform where you add MetaCoq. It would test it on Windows, Mac and Linux then.

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:43):

I remember there was a problem with the backup files way (but I don't recall it exactly), so the mv -f way seems most promising

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:43):

@Yannick Forster I've used the current branches, and they're enough for metacoq-template

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:44):

which AFAIK is the part that most packages depend on

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:45):

@Yannick Forster : afair you need to write -i.bak not -i .bak (no space). The latter works on only one of Mac/Gnu, but don't ask me which.

view this post on Zulip Gaëtan Gilbert (Apr 26 2022 at 11:47):

it doesn't work on gnu because it interprets -i .bak as -i with no backup and then some unrelated argument

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:47):

@Yannick Forster BTW, I apologize for guessing the answer... would you want to submit metacoq-template to the Platform — aka, commit to regular releases?

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:48):

But mv -f has the advantage that it is posix compliant.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:48):

From the lack of releases, I had inferred that supporting clients wasn't the focus, since it's a research project...

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:49):

Regarding Coq Platform CI: I didn't suggest to add it now, I just suggested to use Coq Platform CI as a temporary vehicle for cross platform tests.

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:49):

... and nowadays many users could migrate to coq-elpi (not painlessly!)

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:49):

@Michael Soegtrop nevertheless, it's a question I should have asked earlier

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:52):

Afaik CertiCoq depends on MetaCoq and IMHO CertiCoq is an important project, so I hope both will make it to the Coq Platform not that far in the future.

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:52):

We definitely want to make relying on MetaCoq as easy as possible - several projects do by now. Being able to opam pin to a git commit was our way to go, but a metacoq-template package available before the rest sounds good

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:52):

And yes, the faster we have good packages for all parts of MetaCoq, the better

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:53):

Using Coq platform CI to test compatibility with Mac OS also sounds good

view this post on Zulip Paolo Giarrusso (Apr 26 2022 at 11:54):

oh, I hadn't realized pinning was the recommended solution — apologies for the misunderstanding. But agreed.

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:54):

I'm not sure it's an official recommended solution, but I recommend it :)

view this post on Zulip Karl Palmskog (Apr 26 2022 at 11:54):

unfortunately, until recently, pinning a MetaCoq commit on opam also led to trouble (see discussion in CertiCoq channel)

view this post on Zulip Karl Palmskog (Apr 26 2022 at 11:55):

if we can decide on a versioning scheme for MetaCoq (both in-repo, on extra-dev and in released), that would be great

view this post on Zulip Karl Palmskog (Apr 26 2022 at 11:56):

the simplest solution is just to follow Coq's versioning scheme and do like plugins do, e.g., 8.14.0 is the release, 8.14.dev is the version in the 8.14 branch in the repo

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 11:56):

@Yannick Forster : I would suggest that you do a fork of Coq Platform and do the following:

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:57):

Will do, thanks Michael!

view this post on Zulip Yannick Forster (Apr 26 2022 at 11:57):

(I'm on a plane now and won't be able to answer for a couple of hours)

view this post on Zulip Michael Soegtrop (Apr 26 2022 at 12:01):

Please note that with a single Coq Platform CI run you can test MetaCoq for different Coq versions (say 8.14 and 8.15) in parallel.

view this post on Zulip Matthieu Sozeau (Apr 26 2022 at 12:58):

We're actually expecting to release a first version very soon, along with CertiCoq. I'll give a try to fixing the sed issue once and for all

view this post on Zulip Matthieu Sozeau (Apr 26 2022 at 13:22):

That doesn't seem too hard to achieve indeed: https://github.com/MetaCoq/metacoq/pull/696


Last updated: Aug 11 2022 at 01:03 UTC