HazardousPeach commented 2 years ago

11 appears to break the build on Coq 8.10.2. Maybe other versions too, haven't checked. You might want to note that this version is no longer supported in the README, or provide a workaround.

The error I get on 8.10.2 is:

make coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[1]: Entering directory '/home/alexss/research/coq-projects/cheerios' COQDEP VFILES COQC core/Types.v COQC core/ByteDecidable.v COQC core/Core.v File "./core/Core.v", line 174, characters 0-60: Error: This command does not support this attribute: global.

palmskog commented 2 years ago

This error is due to Coq master requiring locality attributes for certain code. It's not possible for a project to be compatible with Coq 8.10 and Coq master at the same time, so we go with master as always. Coq 8.10 is now around 3 years old. I'll document the minimum Coq version in the near future, but there are no plans to support Coq 8.10 or earlier anymore.

HazardousPeach commented 2 years ago

Ah that makes sense. Yeah you might consider also making a branch or release for the last commit before that pull request, so that the opam repos can point to it when users want to use coq 8.10.

thalesmg commented 2 years ago

Seems like this breaks Verdi's installation. Any workarounds I could use to install Verdi?

Logs

```sh opam switch create verdi --packages=coq-verdi --repos=coq-extra-dev=https://coq.inria.fr/opam/extra-dev,distributedcomponents-dev=http://opam-dev.distributedcomponents.net,default <><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><> Switch invariant: ["coq-verdi"] [NOTE] Packages coq-verdi.dev don't have the 'compiler' flag set (nor any of their direct dependencies). You may want to use `opam switch set-invariant' to keep a stable compiler version on upgrades. <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> ∗ installed base-bigarray.base ∗ installed base-threads.base ∗ installed base-unix.base ⬇ retrieved coq.8.11.2 (cached) ∗ installed conf-findutils.1 ⬇ retrieved coq-cheerios.dev (git+https://github.com/uwplse/cheerios.git#master) ⬇ retrieved coq-inf-seq-ext.dev (git+https://github.com/DistributedComponents/InfSeqExt.git#master) ⬇ retrieved coq-struct-tact.dev (git+https://github.com/uwplse/StructTact.git#master) ⬇ retrieved num.1.4 (cached) ⬇ retrieved ocamlfind.1.9.5 (cached) ⬇ retrieved ocaml-base-compiler.4.11.2 (cached) ⬇ retrieved coq-verdi.dev (git+https://github.com/uwplse/verdi.git#master) ∗ installed ocaml-base-compiler.4.11.2 ∗ installed ocaml-config.1 ∗ installed ocaml.4.11.2 ∗ installed ocamlfind.1.9.5 ∗ installed num.1.4 ∗ installed coq.8.11.2 ∗ installed coq-inf-seq-ext.dev ∗ installed coq-struct-tact.dev [ERROR] The compilation of coq-cheerios.dev failed at "make -j3". #=== ERROR while compiling coq-cheerios.dev ===================================# # context 2.1.3 | linux/x86_64 | | https://coq.inria.fr/opam/extra-dev#2022-09-10 19:10 # path ~/.opam/verdi/.opam-switch/build/coq-cheerios.dev # command ~/.opam/opam-init/hooks/sandbox.sh build make -j3 # exit-code 2 # env-file ~/.opam/log/coq-cheerios-31856-39bdcf.env # output-file ~/.opam/log/coq-cheerios-31856-39bdcf.out ### output ### # [...] # COQDEP VFILES # COQC core/Types.v # COQC core/ByteDecidable.v # COQC core/Core.v # File "./core/Core.v", line 174, characters 0-60: # Error: This command does not support this attribute: global. # [unsupported-attributes,parsing] # # make[2]: *** [Makefile.coq:678: core/Core.vo] Error 1 # make[1]: *** [Makefile.coq:327: all] Error 2 # make[1]: Leaving directory '/home/thales/.opam/verdi/.opam-switch/build/coq-cheerios.dev' # make: *** [Makefile:17: default] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> ┌─ The following actions failed │ λ build coq-cheerios dev └─ ┌─ The following changes have been performed (the rest was aborted) │ ∗ install base-bigarray base │ ∗ install base-threads base │ ∗ install base-unix base │ ∗ install conf-findutils 1 │ ∗ install coq 8.11.2 │ ∗ install coq-inf-seq-ext dev │ ∗ install coq-struct-tact dev │ ∗ install num 1.4 │ ∗ install ocaml 4.11.2 │ ∗ install ocaml-base-compiler 4.11.2 │ ∗ install ocaml-config 1 │ ∗ install ocamlfind 1.9.5 └─ # Run eval $(opam env --switch=verdi) to update the current shell environment Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [Y/n] n ```

palmskog commented 2 years ago

@thalesmg there are two options to make the Verdi build work:

switch to Coq 8.12 or later
use a Cheerios commit from before PR #11 was merged, for example 9c7f66e (git checkout 9c7f66e)

thalesmg commented 2 years ago

Hi @palmskog , thanks for the answer!

Indeed, trying to pin cheerios to that commit worked for me! :beers:

For anyone else having this problem:

opam pin add coq-cheerios https://github.com/uwplse/cheerios.git\#9c7f66e57b91f706d70afa8ed99d64ed98ab367d

About using Coq >= 8.12, since Verdi requires Coq < 8.12~, I guess that lib would need to relax that constraint to allow for this Coq version? Or maybe I should force the Coq version when installing coq-verdi? The fresh opam switch resolved to Coq 8.11 probably because of that. :thinking:

Thanks again!

palmskog commented 2 years ago

@thalesmg Verdi (and Verdi Raft) works fine on 8.12 if you compile it from repo sources - the bound in any opam packages are incorrect, I'll fix this soon. In the meantime, you could clone the Verdi repo, locally edit the package definition to allow 8.12 and later, and use: opam pin add . -k path in the repo root directory.

thalesmg commented 2 years ago

@palmskog I'll try that! Thanks for the fast responses! :beers:

palmskog commented 1 year ago

Minimum Coq version (which is actually 8.14) should now be documented everywhere, including in all relevant opam packages in repos, etc.