Closed brando90 closed 1 year ago
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
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? https://github.com/UCSD-PL/proverbot9001/issues/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 "palmskog@gmail.com"
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 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)
#(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 .)
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?
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 :)
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.
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:
I tried installing it from source:
but it doesn't seem it was to happy about it?
looking at the opam switch perhaps it's working?
Anyway, what commit am I advised to use?
list of commits: https://github.com/uwplse/cheerios/commits/master
related: https://github.com/uwplse/cheerios/issues/12 related: https://github.com/UCSD-PL/proverbot9001/issues/92