How to install metalib so that is fully compatible with proverbot9001 dependency install?

[brando90]

My hypothesis is to install the coq 8.10 coq-metalib via it's commit using only opam pin e.g.:

eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq-metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897

seems alright:

(iit_synthesis) brando9~/proverbot9001/deps/metalib $ opam pin add -y coq-metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897

[NOTE] Package coq-metalib is already pinned to git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 (version dev).
[coq-metalib.dev] synchronised (no changes)
coq-metalib is now pinned to git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 (version dev)

Already up-to-date.
Nothing to do.

is this all?

---

The only final part that is confusing me is if we actually need the metalib version that we got via submodules under deps/metalib and coq-projects/metalib.

tentative commands that seem to work:

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

@HazardousPeach are these two version of metalib actually needed?

---

if you want to see the output of commands that seem to work see this: #82 but it's a lot...likely not needed. Here just for completeness.

[HazardousPeach]

Ah yeah I don't think you need the version of metalib under "deps" if you use that opam git commit trick, that's actually a really good idea. You'll still need one in coq-projects to actually use the proofs in there,

[brando90]

if you use that opam git commit trick,

Ok just to confirm you mean I only need:

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

right?

and we do need

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

only, right?