Pull request #11 Breaks Support for Coq 8.10

[HazardousPeach]

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

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]

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]

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

Logs

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]

@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 Adapt w.r.t. coq/coq#16004. #11 was merged, for example 9c7f66e (git checkout 9c7f66e)

[thalesmg]

Hi @palmskog , thanks for the answer!

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

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

Thanks again!

[palmskog]

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

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

[palmskog]

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

[brando90]

Hi @palmskog , thanks for the answer!

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

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

Thanks again!

@HazardousPeach didn't work. Which commits did you use for coq-cheerios and verdi? Those are breaking for me.

[brando90]

cool, seemed to work with coq-8.10. Now I need to find a commit of verdi that works with coq-8.10.

(iit_synthesis) brando9~ $ eval $(opam env --switch=coq-8.10 --set-switch)
(iit_synthesis) brando9~ $
(iit_synthesis) brando9~ $ opam pin add coq-cheerios https://github.com/uwplse/cheerios.git\#9c7f66e57b91f706d70afa8ed99d64ed98ab367d
[coq-cheerios.dev] synchronised (git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d)
coq-cheerios is now pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d (version dev)

The following actions will be performed:
  ∗ install coq-cheerios dev*
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  2/3: [coq-cheerios: make]
∗ installed coq-cheerios.dev
Done.

[brando90]

perhaps useful, how to freeze a deps chain in opam: https://stackoverflow.com/questions/75452407/how-does-one-pin-freeze-a-version-of-the-dependencies-of-an-opam-project-package#75453430

[brando90]

for my issue I think this worked:

# -- Get cheerios, req to have old versions work in opam: https://github.com/uwplse/cheerios/issues/17
eval $(opam env --switch=coq-8.10 --set-switch)
# opam install might give issues since it gets the most recent version from the officialOPAM repository
#opam -y install coq-cheerios
# use opam pin since pin is created to install specific version (e.g. from git, local, etc.)
opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367

output:

(iit_synthesis) brando9~ $ opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367
[NOTE] Package coq-cheerios is currently pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d (version dev).
Processing: [coq-cheerios.dev: git]
[coq-cheerios.dev] synchronised (no changes)
coq-cheerios is now pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367 (version dev)

The following actions will be performed:
  ∗ install coq-cheerios dev*
Do you want to continue? [Y/n]
[NOTE] Pinning command successful, but your installed packages may be out of sync.
(iit_synthesis) brando9~ $ opam switch
#  switch    compiler                    description
→  coq-8.10  ocaml-base-compiler.4.07.1  coq-8.10
   default   ocaml.5.0.0                 default

[NOTE] Current switch is set locally through the OPAMSWITCH variable.
       The current global system switch is unset.

[brando90]

@thalesmg how did you fix the verdi installation?

[brando90]

I think I found a version of verdi that works (and install cheerios too it seems):

(iit_synthesis) brando9~ $ opam pin add coq-verdi git+https://github.com/uwplse/verdi.git#f3ef8d77afcac495c0864de119e83b25d294e8bb

[coq-verdi.dev] synchronised (git+https://github.com/uwplse/verdi.git#f3ef8d77afcac495c0864de119e83b25d294e8bb)
coq-verdi is now pinned to git+https://github.com/uwplse/verdi.git#f3ef8d77afcac495c0864de119e83b25d294e8bb (version dev)

The following actions will be performed:
  ∗ install coq-cheerios dev* [required by coq-verdi]
  ∗ install coq-verdi    dev*
===== ∗ 2 =====
Do you want to continue? [Y/n] Y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  3/6: [coq-cheerios: make]
∗ installed coq-cheerios.dev
∗ installed coq-verdi.dev
Done.

ref: uwplse/verdi#137

[brando90]

related: #20 but for coq 8.12

[brando90]

related: UCSD-PL/proverbot9001#92 but for coq 8.12 proverbot issues