Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

last commit compatible with coq 8.10? #29

Open
brando90 opened this issue Dec 11, 2022 · 5 comments
Open

last commit compatible with coq 8.10? #29

brando90 opened this issue Dec 11, 2022 · 5 comments

Comments

@brando90
Copy link

brando90 commented Dec 11, 2022

related: UCSD-PL/proverbot9001#82
related: UCSD-PL/proverbot9001#86

@sweirich
Copy link
Contributor

@brando90
Copy link
Author

this worked for me:

# -- Get metalib for coq-8.10 via commit when getting it through git submodules (unsure if needed)
#rm -rf coq-projects/metalib
#git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib
# - use the one with commit even if it doesn't work just to document the commit explicitly in the .modules file
git submodule add -f --name coq-projects/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 coq-projects/metalib
git submodule update --init coq-projects/metalib
(cd coq-projects/metalib && git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897)
(git rev-parse HEAD && cd ..)
# Metalib doesn't install properly through opam unless we use a specific commit.
eval $(opam env --switch=coq-8.10 --set-switch)
(cd coq-projects/metalib && opam install .)

# install it again since I think his code has pointers to a version under deps, could unify with above but it's less work to just accept as is and install it, ref: https://github.com/UCSD-PL/proverbot9001/issues/77
rm -rf deps/metalib
#git submodule add -f --name deps/metalib git+https://github.com/plclub/metalib.git deps/metalib
# - use the one with commit even if it doesn't work just to document the commit explicitly in the .modules file
git submodule add -f --name deps/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 deps/metalib
git submodule update --init deps/metalib
(cd deps/metalib && git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897)
(git rev-parse HEAD && cd ..)
# Metalib doesn't install properly through opam unless we use a specific commit.
eval $(opam env --switch=coq-8.10 --set-switch)
(cd deps/metalib && opam install .)

# -- Install metalib for coq-8.10 via opam pin (it seems to overwrite the isntalled versions so let's have opam pin be the last one?)
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq-metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897

@brando90
Copy link
Author

related: UCSD-PL/proverbot9001#86

@brando90
Copy link
Author

@sweirich does your response mean that:

opam pin add -y coq-metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897

is not needed? how do you recommend installing/pinning the right version I need?

@brando90 brando90 reopened this Feb 15, 2023
@Lysxia
Copy link

Lysxia commented Feb 15, 2023

The tag coq8.10 just identifies a commit. Since you already have found a commit that builds, you can leave it be for now and come back to it later if problems arise because of it. If you do want to use that tag, you get a shorter URL:

opam pin add -y coq-metalib git+https://github.com/plclub/metalib.git#coq8.10

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants