Pierre Vial (Apr 21 2022 at 11:52): 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)
coq-metacoq-template.1.0~beta2+8.13Actually, 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 ?
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.
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)
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)
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
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
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
└─
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.
Pierre Vial (Apr 26 2022 at 09:36):@Matthieu Sozeau It actually works, thanks a lot!
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
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.
Michael Soegtrop (Apr 26 2022 at 09:51):If you need help with this, please let me know.
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.
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.
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?
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…
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)
Paolo Giarrusso (Apr 26 2022 at 10:32):I guess it tries gsed first, but agreed
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?)
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.
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.
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 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.
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.
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.
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.
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.
Paolo Giarrusso (Apr 26 2022 at 11:41):Agree re creating conf-gsed.
Michael Soegtrop (Apr 26 2022 at 11:42):Still my preference is not to depend on it.
Paolo Giarrusso (Apr 26 2022 at 11:42):If people set up the appropriate CI, I agree that's better.
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
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.
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
Paolo Giarrusso (Apr 26 2022 at 11:43):@Yannick Forster I've used the current branches, and they're enough for metacoq-template
Paolo Giarrusso (Apr 26 2022 at 11:44):which AFAIK is the part that most packages depend on
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.
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
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?
Michael Soegtrop (Apr 26 2022 at 11:48):But mv -f has the advantage that it is posix compliant.
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...
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.
Paolo Giarrusso (Apr 26 2022 at 11:49):... and nowadays many users could migrate to coq-elpi (not painlessly!)
Paolo Giarrusso (Apr 26 2022 at 11:49):@Michael Soegtrop nevertheless, it's a question I should have asked earlier
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.
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
Yannick Forster (Apr 26 2022 at 11:52):And yes, the faster we have good packages for all parts of MetaCoq, the better
Yannick Forster (Apr 26 2022 at 11:53):Using Coq platform CI to test compatibility with Mac OS also sounds good
Paolo Giarrusso (Apr 26 2022 at 11:54):oh, I hadn't realized pinning was the recommended solution — apologies for the misunderstanding. But agreed.
Yannick Forster (Apr 26 2022 at 11:54):I'm not sure it's an official recommended solution, but I recommend it :)
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)
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
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
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:
Yannick Forster (Apr 26 2022 at 11:57):Will do, thanks Michael!
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)
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.
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
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: Jun 01 2023 at 11:01 UTC