current deps/cheerios for coq 8.12 really works?

brando90 commented 1 year ago

I tried looking for a commit for cheerios for coq 8.12 https://github.com/uwplse/cheerios/issues/20 but didn't really seem to find one. But I tried the proverbot command anyway and the install looks fishy but it seems fine from the opam list...is it really ok as is?

(iit_synthesis) brando9~/proverbot9001 $ git clone git@github.com:uwplse/cheerios.git deps/cheerios
Cloning into 'deps/cheerios'...

remote: Enumerating objects: 1555, done.
remote: Counting objects: 100% (59/59), done.
remote: Compressing objects: 100% (38/38), done.
remote: Total 1555 (delta 24), reused 37 (delta 16), pack-reused 1496
Receiving objects: 100% (1555/1555), 368.27 KiB | 1.88 MiB/s, done.
Resolving deltas: 100% (997/997), done.
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && opam install -y --ignore-constraints-on=coq .)
coq-cheerios is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master (version dev)
Package cheerios-runtime does not exist, create as a NEW package? [Y/n] y
cheerios-runtime is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master (version dev)

The following actions will be performed:
  ∗ install ocamlbuild       0.14.2 [required by cheerios-runtime]
  ∗ install coq-cheerios     dev*
  ∗ install cheerios-runtime dev*
===== ∗ 3 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved ocamlbuild.0.14.2  (cached)
⬇ retrieved coq-cheerios.dev  (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master)
⬇ retrieved cheerios-runtime.dev  (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master)
[ERROR] The compilation of coq-cheerios.dev failed at "make -j127".
∗ installed ocamlbuild.0.14.2
∗ installed cheerios-runtime.dev

#=== ERROR while compiling coq-cheerios.dev ===================================#
# context     2.1.4 | linux/x86_64 | ocaml-base-compiler.4.07.1 | pinned(git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master#bad8ad24)
# path        ~/.opam/coq-8.12/.opam-switch/build/coq-cheerios.dev
# command     /usr/bin/make -j127
# exit-code   2
# env-file    ~/.opam/log/coq-cheerios-1177511-535ceb.env
# output-file ~/.opam/log/coq-cheerios-1177511-535ceb.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:716: core/Core.vo] Error 1
# make[1]: *** [Makefile.coq:339: all] Error 2
# make[1]: Leaving directory '/lfs/ampere1/0/brando9/.opam/coq-8.12/.opam-switch/build/coq-cheerios.dev'
# make: *** [Makefile:4: default] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-cheerios dev
└─
┌─ The following changes have been performed
│ ∗ install cheerios-runtime dev
│ ∗ install ocamlbuild       0.14.2
└─

The former state can be restored with:
    /lfs/ampere1/0/brando9/.local/bin/opam switch import "/lfs/ampere1/0/brando9/.opam/coq-8.12/.opam-switch/backup/state-20230215231431.export"
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ opam list
# Packages matching: installed
# Name                   # Installed    # Synopsis
base                     v0.14.0        Full standard library replacement for OCaml
base-bigarray            base
base-threads             base
base-unix                base
cheerios-runtime         dev            pinned to version dev at git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master
cmdliner                 1.0.4          Declarative definition of command line interfaces for OCaml
conf-findutils           1              Virtual package relying on findutils
coq                      8.12.2         pinned to version 8.12.2
coq-equations            1.2.3+8.12     A function definition package for Coq
coq-ext-lib              dev            a library of Coq definitions, theorems, and tactics
coq-inf-seq-ext          dev            pinned to version dev at git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/InfSeqExt#master
coq-mathcomp-algebra     1.14.0         Mathematical Components Library on Algebra
coq-mathcomp-field       1.14.0         Mathematical Components Library on Fields
coq-mathcomp-fingroup    1.14.0         Mathematical Components Library on finite groups
coq-mathcomp-solvable    1.14.0         Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect   1.14.0         Small Scale Reflection
coq-metacoq-checker      1.0~beta1+8.12 Specification of Coq's type theory and reference checker implementation
coq-metacoq-template     1.0~beta1+8.12 A quoting and unquoting library for Coq in Coq
coq-serapi               8.12.0+0.12.1  Serialization library and protocol for machine interaction with the Coq proof assistant
coq-simple-io            dev            IO monad for Coq
coq-smpl                 8.12           Smpl: An Extensible Tactic for Coq
coq-struct-tact          dev            pinned to version dev at git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/StructTact#master
cppo                     1.6.9          Code preprocessor like cpp for OCaml
csexp                    1.5.1          Parsing and printing of S-expressions in Canonical form
dune                     3.6.1          Fast, portable, and opinionated build system
dune-configurator        3.6.1          Helper library for gathering system configuration
num                      1.4            The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.07.1         The OCaml compiler (virtual package)
ocaml-base-compiler      4.07.1         Official release 4.07.1
ocaml-compiler-libs      v0.12.4        OCaml compiler libraries repackaged
ocaml-config             1              OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1       OCaml 4.08.1 Secondary Switch Compiler
ocamlbuild               0.14.2         OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind                1.9.1          A library manager for OCaml
ocamlfind-secondary      1.9.1          Adds support for ocaml-secondary-compiler to ocamlfind
parsexp                  v0.14.2        S-expression parsing library
ppx_derivers             1.2.1          Shared [@@deriving] plugin registry
ppx_deriving             5.2.1          Type-driven code generation for OCaml
ppx_deriving_yojson      3.6.1          JSON codec generator for OCaml
ppx_import               1.9.1          A syntax extension for importing declarations from interface files
ppx_sexp_conv            v0.14.3        [@@deriving] plugin to generate S-expression conversion functions
ppxlib                   0.25.1         Standard library for ppx rewriters
result                   1.5            Compatibility Result module
seq                      base           Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib                  v0.14.0        Library for serializing OCaml values to and from S-expressions
sexplib0                 v0.14.0        Library containing the definition of S-expressions and some base converters
stdlib-shims             0.3.0          Backport some of the new stdlib features to older compiler
yojson                   2.0.2          Yojson is an optimized parsing and printing library for the JSON format

brando90 commented 1 year ago

For now this is what works, which is no different from what you tried had:

# Cheerios has its own issues
git clone git@github.com:uwplse/cheerios.git deps/cheerios
(cd deps/cheerios && opam install -y --ignore-constraints-on=coq .)
## this doesn't seem to do anything different than the above attempt, above uses dev & ends up using cheerios-runtime
#git clone git@github.com:uwplse/cheerios.git deps/cheerios
##(cd deps/cheerios && git checkout 9c7f66e57b91f706d70afa8ed99d64ed98ab367d && git rev-parse HEAD)
#(cd deps/cheerios && git checkout 37a30160b4e232555245fbbfb64acfc3d03fda91 && git rev-parse HEAD)  # right before coq >=8.14 warning
##(cd deps/cheerios && git checkout 81a8f820e639067fda0082493a18c7a9b30ee69d && git rev-parse HEAD)  # coq >=8.14 warning
##(cd deps/cheerios && opam install -y .)
#(cd deps/cheerios && opam install -y --ignore-constraints-on=coq .)

crossing fingers it works and there is no name space confusion due to cheerious-runtime vs coq-cheerios

brando90 commented 1 year ago

my request for verdi coq 8.12, though I doubt it will work: https://github.com/uwplse/verdi/issues/138

brando90 commented 1 year ago

either what you did did work for you or the other solutions:

when building the projects, whichever depends on cheerios, verdi coq 8.12 switch, upgrade to a version were those two work e.g. 8.14+ likely most recent is what I'd go with
create out own forks that support 8.12. Likely option 1 is better.

HazardousPeach commented 1 year ago

coq-cheerios and cheerios-runtime aren't different names for the same package, they are two different packages. coq-cheerios depends on cheerios-runtime to work. Your original opam command installed cheerios-runtime, but failed to install coq-cheerios. I never built Cheerios for Coq 8.12, in the Proverbot install it uses Coq 8.10. There's a Coq 8.10 compatible commit here: https://github.com/uwplse/cheerios/commit/f0c7659c44999c6cfcd484dc3182affc3ff4248a

brando90 commented 1 year ago

I never built Cheerios for Coq 8.12, in the Proverbot install it uses Coq 8.10.

Hi Alex! @HazardousPeach

You have this line in your install coqgym deps:

https://github.com/UCSD-PL/proverbot9001/blob/ccb49c5397cb4c890c54cd269ee695cb0cdb3024/install_coqgym_deps.sh#L89

and this one

https://github.com/UCSD-PL/proverbot9001/blob/ccb49c5397cb4c890c54cd269ee695cb0cdb3024/install_coqgym_deps.sh#L90

they come after activating coq 8.12 switch

https://github.com/UCSD-PL/proverbot9001/blob/ccb49c5397cb4c890c54cd269ee695cb0cdb3024/install_coqgym_deps.sh#L69

which made me think and try to install a stable version of cheerios and verdi from source fcsl-pcm is also installed later:

https://github.com/UCSD-PL/proverbot9001/blob/ccb49c5397cb4c890c54cd269ee695cb0cdb3024/install_coqgym_deps.sh#L91

actually all of these are installed for coq 8.12

# Install some coqgym deps that don't have the right versions in their
# official opam packages
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y . )
git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && opam install -y . )
# Cheerios has its own issues
git clone git@github.com:uwplse/cheerios.git deps/cheerios
(cd deps/cheerios && opam install -y --ignore-constraints-on=coq . )
(cd coq-projects/verdi && opam install -y --ignore-constraints-on=coq . )
(cd coq-projects/fcsl-pcm && make "$@" && make install)

code: https://github.com/UCSD-PL/proverbot9001/blob/develop/install_coqgym_deps.sh

I assume we don't need them given your response. As always thanks for the responses.

brando90 commented 1 year ago

There's a Coq 8.10 compatible commit here: uwplse/cheerios@f0c7659

cool I am using a different one that seems to install. Will record that commit in my file just in case:

# -- 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 official OPAM repository
#opam -y install coq-cheerios
#opam install -y coq-verdi
# 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#f0c7659c44999c6cfcd484dc3182affc3ff4248a
opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367

brando90 commented 1 year ago

8.12 doesn't seem to be needed for verdi or cheerios. Confirmation will be here I hope: https://github.com/UCSD-PL/proverbot9001/issues/93

UCSD-PL / proverbot9001

current deps/cheerios for coq 8.12 really works? #92