why does metalib need coq 8.15 and how to fix it so that it compatible with proverbot9001 -- do we need coq-8.10 really?

[brando90]

related to https://github.com/UCSD-PL/proverbot9001/issues/78 I am trying to understand if the reason I needed to create a coq 8.15 opam switch was due to

1. git submdolues issues or
2. deps from the internet that opam needs for metalib (so metalibs dependencies)

which one is it?

For further context this is the cmd that seems to work right now:

# - Get metalib (so far needs coq 8.15.2)
# - Create the coq 8.15 switch
opam switch create coq-8.15 4.07.1
eval $(opam env --switch=coq-8.15 --set-switch)
opam pin add -y coq 8.15.2
# Libs that break stuff, likely need to fork each one and thus fix the version so the data gen is fixed
# - Get metalib
# Q: metalib missing, how do I pull it with original git submodule commands? ref1: https://stackoverflow.com/questions/74757297/how-do-i-make-sure-to-re-add-a-submodule-correctly-with-a-git-command-without-ma, ref2: https://github.com/UCSD-PL/proverbot9001/issues/59, ref3: https://github.com/UCSD-PL/proverbot9001/issues/60
# Metalib doesn't install properly through opam unless we use a specific commit.
git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib
git submodule update --init coq-projects/metalib
(cd coq-projects/metalib && opam install .)
# alex wasn't clear if this was needed, most likely just install both so you don't need to refactor his code, ref: https://github.com/UCSD-PL/proverbot9001/issues/77
git submodule add -f --name deps/metalib https://github.com/plclub/metalib.git deps/metalib
git submodule update --init deps/metalib
(cd deps/metalib && opam install .)

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

[HazardousPeach]

Well, you're building metalib from source, so if you use the latest commit, it's going to try to pull in a recent version of Coq. What you really want to do is check out an older commit of metalib that's compatible with the Coq version you want to use. As far as I can tell this commit: https://github.com/plclub/metalib/commit/104fd9efbfd048b7df25dbac7b971f41e8e67897 should do the trick; it's just before the adding of #[global] annotations that breaks backwards compatibility.

Now, even once you do that, it might need dependencies to build that don't have compatible opam versions, so you would have to switch them to git recursively.

The script you're showing doesn't seem like it'll work for packages that depend on metalib. Because you're installing metalib (the deps/metalib version in this case) on Coq8.15, projects that aren't on Coq8.15 won't be able to use it as a dependency. You need to install it in deps/ with the version of Coq the projects that depend on it are going to use.

[brando90]

The script you're showing doesn't seem like it'll work for packages that depend on metalib. Because you're installing metalib (the deps/metalib version in this case) on Coq8.15, projects that aren't on Coq8.15 won't be able to use it as a dependency. You need to install it in deps/ with the version of Coq the projects that depend on it are going to use.

@HazardousPeach ok I think I got the gist. We need to install the right version of the deps that will work when we try to build the coq-projs/pkgs we git subomulded into coq-projec when we run build_coq_projects.sh. Is that correct?

Therefore in general something like this might work (assuming the right commit & opam switch):

opam switch create coq-8.10 4.07.1
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq 8.10.2

opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897

but for metalib specifically what worries me is that proverbot seems to have a dependency installation from source to it. So even if the above worked how do I make the rest of the stuff dependent on metalib work if I installed it with opam?

[brando90]

The script you're showing doesn't seem like it'll work for packages that depend on metalib. Because you're installing metalib (the deps/metalib version in this case) on Coq8.15, projects that aren't on Coq8.15 won't be able to use it as a dependency. You need to install it in deps/ with the version of Coq the projects that depend on it are going to use.

@HazardousPeach ok I think I got the gist. We need to install the right version of the deps that will work when we try to build the coq-projs/pkgs we git subomulded into coq-projec when we run build_coq_projects.sh. Is that correct?

Therefore in general something like this might work (assuming the right commit & opam switch):

opam switch create coq-8.10 4.07.1
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq 8.10.2

opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897

but for metalib specifically what worries me is that proverbot seems to have a dependency installation from source to it. So even if the above worked how do I make the rest of the stuff dependent on metalib work if I installed it with opam?

sad the above seemed to have failed:

(iit_synthesis) brando9~ $ eval $(opam env --switch=coq-8.10 --set-switch)
(iit_synthesis) brando9~ $ opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897
[NOTE] Package coq-metalib is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/metalib#master (version dev).
[coq-metalib.dev] fetching sources failed: Unknown archive type: /tmp/user/22003/opam-3178002-9918a9/104fd9efbfd048b7df25dbac7b971f41e8e67897
[ERROR] Error getting source from https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897:
          - Could not extract archive:
            Unknown archive type: /tmp/user/22003/opam-3178002-9918a9/104fd9efbfd048b7df25dbac7b971f41e8e67897

[brando90]

What I'm still confused is if metalib needs to be installed from source or an opam install will be sufficient.

The confusion is caused by these two lines in the .gitsubomdules file:

[submodule "coq-projects/metalib"]
    path = coq-projects/metalib
    url = https://github.com/plclub/metalib.git

and

[submodule "deps/metalib"]
    path = deps/metalib
    url = https://github.com/plclub/metalib.git

[brando90]

ok I think at least the opam pin I just did is working:

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

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

The following actions will be performed:
  ∗ install coq-metalib dev*
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  2/3: [coq-metalib: make Metalib]
∗ installed coq-metalib.dev
Done.

[brando90]

for the coq-projects & deps I hope the url I provided for the pin also works. Will report commands.

[brando90]

What I'm still confused is if metalib needs to be installed from source or an opam install will be sufficient.

The confusion is caused by these two lines in the .gitsubomdules file:

[submodule "coq-projects/metalib"]
  path = coq-projects/metalib
  url = https://github.com/plclub/metalib.git

and

[submodule "deps/metalib"]
  path = deps/metalib
  url = https://github.com/plclub/metalib.git

To address this issue I was trying to git init the submodule with the commit I know works, but the git submodule command doesn't work as I'd expect:

(iit_synthesis) brando9~/proverbot9001 $ git submodule add -f --name coq-projects/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 coq-projects/metalib
Reactivating local git directory for submodule 'coq-projects/metalib'.

(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ cd metalib
-bash: cd: metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001 $ cd coq-projects/
(iit_synthesis) brando9~/proverbot9001/coq-projects $ cd metalib
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git rev-parse HEAD
4ea92d82286cf66e54b4119b2bb2b039827204ab

It's the wrong commit -- even though the .gitmodules file show the expected url. Will just manually cd and change the commit.

[brando90]

ok this seemed to work:

# -- Get metalib foor coq-8.10 via commit when getting it through git submodules
#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 status && 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 .)

output:

(iit_synthesis) brando9~/proverbot9001 $ git submodule add -f --name coq-projects/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 coq-projects/metalib
Reactivating local git directory for submodule 'coq-projects/metalib'.

(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ cd metalib
-bash: cd: metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001 $ cd coq-projects/
(iit_synthesis) brando9~/proverbot9001/coq-projects $ cd metalib
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git rev-parse HEAD
4ea92d82286cf66e54b4119b2bb2b039827204ab
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ cd coq-projects/metalib
-bash: cd: coq-projects/metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897
Note: switching to '104fd9efbfd048b7df25dbac7b971f41e8e67897'.

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 104fd9e Sync Makefile coq version with README/Docker
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git status
HEAD detached at 104fd9e
nothing to commit, working tree clean
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ cd coq-projects/metalib && opam install .)
-bash: syntax error near unexpected token `)'
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ (cd coq-projects/metalib && opam install .)
-bash: cd: coq-projects/metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ opam install .
[NOTE] Package coq-metalib is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/metalib#master (version dev).
coq-metalib is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/metalib#HEAD (version dev)
[coq-metalib.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/metalib#HEAD)

The following actions will be performed:
  ↻ recompile coq-metalib dev*

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   coq-metalib.dev
∗ installed coq-metalib.dev
Done.

now lets do deps

[brando90]

deps install seemed to work:

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

output:

(iit_synthesis) brando9~/proverbot9001/deps/metalib $ git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897
HEAD is now at 104fd9e Sync Makefile coq version with README/Docker
(iit_synthesis) brando9~/proverbot9001/deps/metalib $ git rev-parse HEAD
104fd9efbfd048b7df25dbac7b971f41e8e67897
(iit_synthesis) brando9~/proverbot9001/deps/metalib $ eval $(opam env --switch=coq-8.10 --set-switch)
(iit_synthesis) brando9~/proverbot9001/deps/metalib $ (cd deps/metalib && opam install .)
-bash: cd: deps/metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001/deps/metalib $ opam install .
[NOTE] Package coq-metalib is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/metalib#HEAD (version dev).
coq-metalib is now pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/metalib#HEAD (version dev)
[coq-metalib.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/metalib#HEAD)
The following actions will be performed:
  ↻ recompile coq-metalib dev*

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   coq-metalib.dev
∗ installed coq-metalib.dev
Done.
(iit_synthesis) brando9~/proverbot9001/deps/metalib $ opam pin add coq-metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897

[NOTE] Package coq-metalib is currently pinned to git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/deps/metalib#HEAD (version dev).
[coq-metalib.dev] synchronised (git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897)
coq-metalib is now pinned to git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 (version dev)

The following actions will be performed:
  ↻ recompile coq-metalib dev*
Do you want to continue? [Y/n] Y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  2/4: [coq-metalib: make Metalib]
⊘ removed   coq-metalib.dev
∗ installed coq-metalib.dev
Done.
(iit_synthesis) brando9~/proverbot9001/deps/metalib $

[brando90]

Finally the opam pin at the end:

(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.

seems to have worked

[brando90]

to make it more organized and hopefully no one has to read the above, the solution will be documented and confirmed here: https://github.com/UCSD-PL/proverbot9001/issues/86

[brando90]

other ref: https://stackoverflow.com/questions/75417355/how-does-one-git-submodule-add-a-specific-commit-and-have-it-be-recorded-in-the/75455526#75455526

[brando90]

related: https://github.com/UCSD-PL/proverbot9001/issues/86

[brando90]

old issue: https://github.com/UCSD-PL/proverbot9001/issues/59