deps/verdi doesn't seem to work for coq 8.12 even with the --ignore-constraints-on=coq trick, is it really needed?

[brando90]

I tried the following but it doesn't seem to have worked:

git clone git@github.com:uwplse/verdi.git deps/verdi
(cd coq-projects/verdi && 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 verdi-runtime
#git clone git@github.com:uwplse/verdi.git deps/verdi
#(cd deps/verdi && git checkout fdb4ede19d2150c254f0ebcfbed4fb9547a734b0 && git rev-parse HEAD)
#(cd deps/verdi && git checkout 3d22ce073f7d16da58eb8e1aa3c71bf8f588a04f && git rev-parse HEAD)
#(cd deps/verdi && git checkout 35508f2af94f9da979ece0cbdfa191019f2c5478 && git rev-parse HEAD) # right before coq >=8.14 warning
#(cd deps/verdi && git checkout cb016cf9d2ae61ff757a0b6fa443b391a5416b63 && git rev-parse HEAD)  # coq >=8.14 warning
#(cd deps/verdi && opam install -y .)

output:

(iit_synthesis) brando9~/proverbot9001 $ git clone git@github.com:uwplse/verdi.git deps/verdi
fatal: destination path 'deps/verdi' already exists and is not an empty directory.
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/verdi && opam install -y --ignore-constraints-on=coq .)

[NOTE] Package coq-verdi is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/verdi#HEAD (version dev).
coq-verdi is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/verdi#HEAD (version dev)
[coq-verdi.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/verdi#HEAD)
 list

The following actions will be performed:
  ∗ install coq-cheerios dev* [required by coq-verdi]
  ∗ install coq-verdi    dev*
===== ∗ 2 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-cheerios.dev failed at "make -j127".

#=== 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#HEAD#37a30160)
# 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-1200967-616b45.env
# output-file ~/.opam/log/coq-cheerios-1200967-616b45.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:17: default] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-cheerios dev
└─
╶─ No changes have been performed
(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#HEAD
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

what did you end up doing for this one Alex @HazardousPeach?

[brando90]

my request for verdi coq 8.12, though I doubt it will work: uwplse/verdi#138

[brando90]

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

1. 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
2. create out own forks that support 8.12. Likely option 1 is better.

[HazardousPeach]

You should be able to just use verdi with this commit: uwplse/verdi@064cc4f .

[brando90]

You should be able to just use verdi with this commit: uwplse/verdi@064cc4f .

related to this #92 the reason I originally asked this becuase at the end of your script you have this source installation after coq 8.12 has been activated. Is that not needed?

# Create the coq 8.12 switch
opam switch create coq-8.12 4.07.1
eval $(opam env --switch=coq-8.12 --set-switch)
opam pin add -y coq 8.12.2

# Install the packages that can be installed directly through opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev


...

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

[brando90]

You should be able to just use verdi with this commit: uwplse/verdi@064cc4f .

for coq 8.10 I am using:

opam pin add coq-verdi git+https://github.com/uwplse/verdi.git#f3ef8d77afcac495c0864de119e83b25d294e8bb

for 8.12

git clone git@github.com:uwplse/verdi.git deps/verdi
(cd coq-projects/verdi && opam install -y --ignore-constraints-on=coq .)

since no commit worked. But I am assuming based on previous conv #92 that cheerios doesn't need 8.12 and therefore verdi doesn't either (despite the source installation that is confusing me personally right now).

@HazardousPeach all of that is correct right?

[brando90]

this is the final issue to confirm a stable deps file for proverbot's coqgym :)

[HazardousPeach]

I don't think that's quite correct, there is a commit that works for Coq 8.12, the one I just gave you (064cc4f). I just tested it on my end, it compiles fine. You can't use it in an opam link I think, I get the error message "Sorry, no solution found". But that seems to be an issue on the opam end, if you git clone the project and checkout that commit, opam install --ignore-constraints-on=coq works. So, for 8.12, the commands should be:

git clone git@github.com:uwplse/verdi.git deps/verdi
git -C deps/verdi checkout 064cc4f
(cd deps/verdi && opam install -y --ignore-constraints-on=coq .)

Maybe you were thinking the commit didn't work because you were trying to build the wrong version? The commands you posted git clone to deps/verdi, but then try to build from coq-projects/verdi instead.