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)
coq-metacoq-template.1.0~beta2+8.13
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 metacoq
is 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 ?
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.
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)
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)
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
Thanks, I'll try this. But what suprises me the most is that I know that I can have switch with the aforementioned versions
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
└─
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.
@Matthieu Sozeau It actually works, thanks a lot!
there is currently no conf-sed
package in opam, so ideally MetaCoq would add some kind of manual check for GNU sed
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
.
If you need help with this, please let me know.
maybe we can ask @Pierre Vial to test again, but with Mac sed. Then we at least know only GNU sed works.
The script does try to get either gsed
or sed
so for him it used sed
and it failed.
I did install gnu-sed
as Matthieu suggested.
How could I constrain MacOs to use sed
instead of gsed
as @Karl Palmskog suggests?
@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…
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
)
I guess it tries gsed first, but agreed
@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?)
@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.
I am not aware of an easy way to test with Mac BSD (short of Github CI) on Linux.
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 trygsed
)
More precisely here is how it decides:
SED=`which gsed || which sed`
Generally, it seems clear that a package shouldn't use BSD sed if the authors don't invest the time to support it.
And I'm somewhat skeptical people would want to support it when installing gnu-sed is so easy.
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.
Maybe. But if somebody chose to invest time in MetaCoq, releasing packages for 8.14 and 8.15 seems more urgent.
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.
Agree re creating conf-gsed
.
Still my preference is not to depend on it.
If people set up the appropriate CI, I agree that's better.
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
You could do a PR to Coq platform where you add MetaCoq. It would test it on Windows, Mac and Linux then.
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
@Yannick Forster I've used the current branches, and they're enough for metacoq-template
which AFAIK is the part that most packages depend on
@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.
it doesn't work on gnu because it interprets -i .bak
as -i with no backup and then some unrelated argument
@Yannick Forster BTW, I apologize for guessing the answer... would you want to submit metacoq-template to the Platform — aka, commit to regular releases?
But mv -f
has the advantage that it is posix compliant.
From the lack of releases, I had inferred that supporting clients wasn't the focus, since it's a research project...
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.
... and nowadays many users could migrate to coq-elpi (not painlessly!)
@Michael Soegtrop nevertheless, it's a question I should have asked earlier
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.
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
And yes, the faster we have good packages for all parts of MetaCoq, the better
Using Coq platform CI to test compatibility with Mac OS also sounds good
oh, I hadn't realized pinning was the recommended solution — apologies for the misunderstanding. But agreed.
I'm not sure it's an official recommended solution, but I recommend it :)
unfortunately, until recently, pinning a MetaCoq commit on opam also led to trouble (see discussion in CertiCoq channel)
if we can decide on a versioning scheme for MetaCoq (both in-repo, on extra-dev
and in released
), that would be great
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
@Yannick Forster : I would suggest that you do a fork of Coq Platform and do the following:
Will do, thanks Michael!
(I'm on a plane now and won't be able to answer for a couple of hours)
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.
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
That doesn't seem too hard to achieve indeed: https://github.com/MetaCoq/metacoq/pull/696
Last updated: Sep 25 2023 at 12:01 UTC