search

uwplse / cheerios

Formally verified Coq serialization library with support for extraction to OCaml
BSD 2-Clause "Simplified" License
23 stars 5 forks source link

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

Closed brando90 closed 1 year ago

brando90 commented 1 year ago

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: https://github.com/UCSD-PL/proverbot9001/issues/78

palmskog commented 1 year ago

This has already been discussed in #12. Coq 8.10 is now almost 4 years old, and those who want to support for it will need to use old git commits in the repo. You can see in this issue comment how to install a specific commit via opam.

brando90 commented 1 year ago

@palmskog which file do I need to update in my gitrepo such that the specified version of coq I want is used? this one? https://github.com/brando90/cheerios/blob/master/meta.yml

brando90 commented 1 year ago

or this one? https://github.com/brando90/cheerios/blob/master/coq-cheerios.opam

palmskog commented 1 year ago

I don't really understand the question(s). Did you look at how opam pinning works? https://opam.ocaml.org/doc/Manual.html#Pinning

brando90 commented 1 year ago

@palmskog yes. I think what I need is to find commit that works with some specific version of coq (I am happy with any commit that makes things work).

Currently trying this one but didn't work:

opam pin add coq-cheerios https://github.com/uwplse/cheerios.git\#9c7f66e57b91f706d70afa8ed99d64ed98ab367d
palmskog commented 1 year ago

Well, you can pin a commit in your own fork of cheerios if you like, e.g., after making fixes to it. The general gist is that the upstream repo master HEAD will stay on 8.14+.

brando90 commented 1 year ago

perhaps useful, how to freeze a deps chain in opam: https://stackoverflow.com/questions/75452407/how-does-one-pin-freeze-a-version-of-the-dependencies-of-an-opam-project-package#75453430

brando90 commented 1 year ago

@palmskog wouldn't a more stable solution to not overwrite the things pushed to opam? Similar to how things are done in python with pip? :) May this be requested?

brando90 commented 1 year ago

for my issue I think this worked:

# -- 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 officialOPAM repository
#opam -y install coq-cheerios
# 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#9c7f66e57b91f706d70afa8ed99d64ed98ab367

output:

(iit_synthesis) brando9~ $ opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367
[NOTE] Package coq-cheerios is currently pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d (version dev).
Processing: [coq-cheerios.dev: git]
[coq-cheerios.dev] synchronised (no changes)
coq-cheerios is now pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367 (version dev)

The following actions will be performed:
  ∗ install coq-cheerios dev*
Do you want to continue? [Y/n]
[NOTE] Pinning command successful, but your installed packages may be out of sync.
(iit_synthesis) brando9~ $ opam switch
#  switch    compiler                    description
→  coq-8.10  ocaml-base-compiler.4.07.1  coq-8.10
   default   ocaml.5.0.0                 default

[NOTE] Current switch is set locally through the OPAMSWITCH variable.
       The current global system switch is unset.