what commit or version of cheerios supports coq 8.12?

[brando90]

Apologies in advance for the request. Is there a version cheerios that supports coq 8.12?

Tried skimming a couple of commits but doesn't seem obvious which one would work. I saw:

• 9c7f66e
• make warn_deprecated_hint_without_locality AsError coq/coq#16004
• 81a8f82
• 48bdcef

I tried installing it from source:

(iit_synthesis) brando9~/proverbot9001 $ git clone [email protected]: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"

but it doesn't seem it was to happy about it?

looking at the opam switch perhaps it's working?

(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

Anyway, what commit am I advised to use?

list of commits: https://github.com/uwplse/cheerios/commits/master

---

related: #12
related: UCSD-PL/proverbot9001#92

[brando90]

ok tried each one at a time and it seems there isn't official support from a commit's point of view:

(iit_synthesis) brando9~/proverbot9001 $ cd deps/cheerios && git checkout 9c7f66e57b91f706d70afa8ed99d64ed98ab367d  && git rev-parse HEAD)
-bash: syntax error near unexpected token `)'
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && git checkout 9c7f66e57b91f706d70afa8ed99d64ed98ab367d && git rev-parse HEAD)
Note: switching to '9c7f66e57b91f706d70afa8ed99d64ed98ab367d'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 9c7f66e update opam and Travis for 8.11
9c7f66e57b91f706d70afa8ed99d64ed98ab367d
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && opam install -y .)
[NOTE] Package coq-cheerios is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master (version dev).
coq-cheerios is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD (version dev)
[NOTE] Package cheerios-runtime is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#master (version dev).
cheerios-runtime is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD (version dev)
[cheerios-runtime.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)
[coq-cheerios.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)
[ERROR] Package conflict!
  * Missing dependency:
    - coq (< 8.12~ | >= dev)
    not available because the package is pinned to version 8.12.2

No solution found, exiting
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && git checkout 37a30160b4e232555245fbbfb64acfc3d03fda91 && git rev-parse HEAD)
Previous HEAD position was 9c7f66e update opam and Travis for 8.11
HEAD is now at 37a3016 Adapt w.r.t. coq/coq#16004. (#11)
37a30160b4e232555245fbbfb64acfc3d03fda91
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && opam install -y .)

[cheerios-runtime.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)
[coq-cheerios.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)


[ERROR] Package conflict!
  * Missing dependency:
    - coq (< 8.12~ | >= dev)
    not available because the package is pinned to version 8.12.2

No solution found, exiting
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && git checkout 81a8f820e639067fda0082493a18c7a9b30ee69d && git rev-parse HEAD)
Previous HEAD position was 37a3016 Adapt w.r.t. coq/coq#16004. (#11)
HEAD is now at 81a8f82 add meta.yml and generate boilerplate (#13)
81a8f820e639067fda0082493a18c7a9b30ee69d
(iit_synthesis) brando9~/proverbot9001 $ (cd deps/cheerios && opam install -y .)
[cheerios-runtime.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)
[coq-cheerios.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD)
[coq-cheerios] Installing new package description from upstream git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD

[ERROR] Package conflict!
  * Missing dependency:
    - coq >= 8.14
    not available because the package is pinned to version 8.12.2

No solution found, exiting

[brando90]

if I really want to record a commit perhaps choosing one before it said >= 8.14 is enough. Thought using most recent and ignoring coq seems to be ok? UCSD-PL/proverbot9001#92

ok, trying to tie it to this commit but it ends up going to dev & cheerious-runtime:

(iit_synthesis) brando9~/proverbot9001 $ opam show cheerios-runtime

<><> cheerios-runtime: information on all versions ><><><><><><><><><><><><><><>
name                   cheerios-runtime
all-installed-versions dev [coq-8.12]
all-versions           dev

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version     dev
pin         git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD
source-hash 37a30160
url.src     "git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/cheerios#HEAD"
homepage    "https://github.com/uwplse/cheerios"
bug-reports "https://github.com/uwplse/cheerios/issues"
dev-repo    "git+https://github.com/uwplse/cheerios.git"
authors     "Justin Adsuara"
            "Karl Palmskog"
            "Keith Simmons"
            "James R. Wilcox"
            "Doug Woos"
maintainer  "[email protected]"
license     "BSD-2-Clause"
depends     "ocaml" {>= "4.02.3"} "ocamlbuild" {build}
synopsis    Cheerios serialization framework runtime library
description OCaml support library for the Coq library Cheerios,
            enabling running extracted verified serialization code.

after running:

git clone [email protected]: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)
#(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 .)

[sorawee]

I don't think it's appropriate to use GitHub issue like a chatting service. It is extremely spammy for people who watch the repo. May I suggest that the communication be moved to other channels instead?

[brando90]

I don't think it's appropriate to use GitHub issue like a chatting service. It is extremely spammy for people who watch the repo. May I suggest that the communication be moved to other channels instead?

sure!

We can also just close this if you know the commit for coq 8.12 :)

[palmskog]

Repo issues here are not some "commit request service". The only Coq versions we support are 8.14+. Please use your own fork to solve any other issues.