UCSD-PL / proverbot9001

GNU General Public License v3.0
39 stars 17 forks source link

Some packages that don't have an official opam repository version don't need commit hashes -- StructTact? #90

Closed brando90 closed 1 year ago

brando90 commented 1 year ago

As I was trying to make a stable install script I found this:

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

...

git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y .)
# f8d4f8a0e04df0522a839462e725a48d54145b48

does this mean we don't need to clone exact commits sometimes since once cloned the opam install magically knows what version to install?

brando90 commented 1 year ago

wrote this just in case:

# Install some coqgym deps that don't have the right versions in their official opam packages
# Some packages that don't have an official opam repository version don't need commit hashes? ref: https://github.com/UCSD-PL/proverbot9001/issues/90
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y .)
# above worked, but leaving code bellow in case it's needed
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && git checkout f8d4f8a0e04df0522a839462e725a48d54145b48 && git rev-parse HEAD)
(cd deps/StructTact && opam install -y .)

seems to work...for now.

HazardousPeach commented 1 year ago

Ah, no you still need to check out a particular commit if you want long term stability. StructTact had it's own thing where the opam version had bad metadata, but the main up to date repository worked, so I wasn't trying to ensure version stability there.

brando90 commented 1 year ago

Ah, no you still need to check out a particular commit if you want long term stability. StructTact had it's own thing where the opam version had bad metadata, but the main up to date repository worked, so I wasn't trying to ensure version stability there.

ok so you think the newest one would work?

brando90 commented 1 year ago

if you have time to confirm I have the right commit you are using great!

Otherwise I'm closing this and putting the commit I used to make this install stable according to me:

# - Install some coqgym deps that don't have the right versions in their official opam packages
# The head commit at this time worked, so I am leaving it hardcoded after this install. If bellow fails use the hardcoded commit one. Details, ref: https://github.com/UCSD-PL/proverbot9001/issues/90
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y .)
# above worked, but leaving code bellow in case it's needed
#git clone git@github.com:uwplse/StructTact.git deps/StructTact
#(cd deps/StructTact && git checkout f8d4f8a0e04df0522a839462e725a48d54145b48 && git rev-parse HEAD)
#(cd deps/StructTact && opam install -y .)
brando90 commented 1 year ago

as of this writing the most recent commit is: 2f2ff253be29bb09f36cab96d036419b18a95b00 but I've not tested if it works for coq 8.12. Commit history: https://github.com/uwplse/StructTact/commits/master

brando90 commented 1 year ago

2f2ff253be29bb09f36cab96d036419b18a95b00

# - Install some coqgym deps that don't have the right versions in their official opam packages
# The head commit at this time worked, so I am leaving it hardcoded after this install. If bellow fails use the hardcoded commit one. Details, ref: https://github.com/UCSD-PL/proverbot9001/issues/90
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y .)
# above worked, but leaving code bellow in case it's needed
#git clone git@github.com:uwplse/StructTact.git deps/StructTact
#(cd deps/StructTact && git checkout f8d4f8a0e04df0522a839462e725a48d54145b48 && git rev-parse HEAD)
#(cd deps/StructTact && opam install -y .)
# if above fails perhaps this will work? most recent commit at this time 2f2ff253be29bb09f36cab96d036419b18a95b00
#git clone git@github.com:uwplse/StructTact.git deps/StructTact
#(cd deps/StructTact && git checkout 2f2ff253be29bb09f36cab96d036419b18a95b00 && git rev-parse HEAD)
#(cd deps/StructTact && opam install -y .)