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

brando90 · 2023-02-14T19:02:41Z

related to #78 I am trying to understand if the reason I needed to create a coq 8.15 opam switch was due to

git submdolues issues or
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

The text was updated successfully, but these errors were encountered:

HazardousPeach · 2023-02-14T19:36:35Z

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: plclub/metalib@104fd9e 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 · 2023-02-14T21:28:25Z

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 · 2023-02-14T21:29:47Z

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 · 2023-02-15T02:50:50Z

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 · 2023-02-15T04:08:57Z

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 · 2023-02-15T04:09:39Z

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

brando90 · 2023-02-15T04:21:25Z

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 · 2023-02-15T04:36:59Z

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 · 2023-02-15T04:45:41Z

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 · 2023-02-15T04:46:11Z

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 · 2023-02-15T04:50:22Z

to make it more organized and hopefully no one has to read the above, the solution will be documented and confirmed here: #86

brando90 · 2023-02-15T04:51:47Z

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 · 2023-02-15T04:52:57Z

related: #86

brando90 · 2023-02-15T04:57:18Z

old issue: #59

brando90 changed the title ~~why does metalib need coq 8.15?~~ 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? Feb 15, 2023

brando90 closed this as completed Feb 15, 2023

brando90 mentioned this issue Feb 15, 2023

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

Closed

brando90 mentioned this issue Feb 15, 2023

last commit compatible with coq 8.10? plclub/metalib#29

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

brando90 commented Feb 14, 2023 •

edited

Loading

HazardousPeach commented Feb 14, 2023

brando90 commented Feb 14, 2023 •

edited

Loading

brando90 commented Feb 14, 2023

brando90 commented Feb 15, 2023 •

edited

Loading

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

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

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

Comments

brando90 commented Feb 14, 2023 • edited Loading

HazardousPeach commented Feb 14, 2023

brando90 commented Feb 14, 2023 • edited Loading

brando90 commented Feb 14, 2023

brando90 commented Feb 15, 2023 • edited Loading

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 15, 2023

brando90 commented Feb 14, 2023 •

edited

Loading

brando90 commented Feb 14, 2023 •

edited

Loading

brando90 commented Feb 15, 2023 •

edited

Loading