uwplse/cheerios

Formally verified Coq serialization library with support for extraction to OCaml

cheerios's Issues

what commit or version of cheerios supports coq 8.12?

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
• 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

May old versions of cheerios be available on opam besides dev?

According to this page https://coq.inria.fr/opam/extra-dev/packages/coq-cheerios/, the only version of coq-cheerios available in opam is the dev version which follows the newest Coq. Can old version also be made available so to not break previous usages of cheerios?

context of previous installations: UCSD-PL/proverbot9001#78

readme says coq-cheerios is compatible with coq version above 8.14 but it fails to opam install with 8.15, why?

code I ran:

(iit_synthesis) brando9~ $ eval $(opam env --switch=coq-8.10 --set-switch)
(iit_synthesis) brando9~ $ opam install -y coq-cheerios

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

No solution found, exiting

is it true that cheerios is overwriting the previous versions itself on the official OPAM repository?

related: https://discuss.ocaml.org/t/is-it-true-that-the-official-opam-repository-allows-non-additive-updates-to-the-projects-packages-pushed-to-it/11432

Pull request #11 Breaks Support for Coq 8.10

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