installing deps for coq doesn't work, need >=8.14 not 8.10, most likely coq-cheerios and verdi - help fix!
brando90 opened this issue · 13 comments
Running instructions as is fails at this stage with error:
(iit_synthesis) brando9~/proverbot9001 $ opam install -y coq-serapi \
> coq-struct-tact \
> coq-inf-seq-ext \
> coq-cheerios \
> coq-verdi \
> coq-smpl \
> coq-int-map \
> coq-pocklington \
> coq-mathcomp-ssreflect coq-mathcomp-bigenough coq-mathcomp-algebra\
> coq-fcsl-pcm \
> coq-ext-lib \
> coq-simple-io \
> coq-list-string \
> coq-error-handlers \
> coq-function-ninjas \
> coq-algebra \
> coq-zorns-lemma
[ERROR] Package conflict!
* Missing dependency:
- coq >= 8.14
not available because the package is pinned to version 8.10.
current file:
#!/usr/bin/env bash
ruby --version
if ! command -v ruby &> /dev/null
then
# First, install Ruby, as that is for some reason required to build
# the "system" project
git clone https://github.com/rbenv/ruby-build.git ~/ruby-build
mkdir -p ~/.local
PREFIX=~/.local ./ruby-build/install.sh
~/.local/ruby-build 3.1.2 ~/.local/
fi
git submodule update && git submodule init
# Sync opam state to local https://github.com/UCSD-PL/proverbot9001/issues/52 (this can be removed for me)
rsync -av --delete $HOME/.opam.dir/ /tmp/${USER}_dot_opam | tqdm --desc="Reading shared opam state" > /dev/null
# Create the 8.10 switch (cmd options opam switch create SWITCH [COMPILER])
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
# Install dependency packages for 8.10
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add psl-opam-repository https://github.com/uds-psl/psl-opam-repository.git
opam install -y coq-serapi \
coq-struct-tact \
coq-inf-seq-ext \
coq-cheerios \
coq-verdi \
coq-smpl \
coq-int-map \
coq-pocklington \
coq-mathcomp-ssreflect coq-mathcomp-bigenough coq-mathcomp-algebra\
coq-fcsl-pcm \
coq-ext-lib \
coq-simple-io \
coq-list-string \
coq-error-handlers \
coq-function-ninjas \
coq-algebra \
coq-zorns-lemma
opam pin -y add menhir 20190626
# coq-equations seems to rely on ocamlfind for it's build, but doesn't
# list it as a dependency, so opam sometimes tries to install
# coq-equations before ocamlfind. Splitting this into a separate
# install call prevents that.
opam install -y coq-equations \
coq-metacoq coq-metacoq-checker coq-metacoq-template
# Metalib doesn't install properly through opam unless we use a
# specific commit.
(cd coq-projects/metalib && opam install .)
(cd coq-projects/lin-alg && make "$@" && make install)
# Install the psl base-library from source
mkdir -p deps
git clone -b coq-8.10 git@github.com:uds-psl/base-library.git deps/base-library
(cd deps/base-library && make "$@" && make install)
git clone git@github.com:davidnowak/bellantonicook.git deps/bellantonicook
(cd deps/bellantonicook && make "$@" && make install)
# Create the coq 8.12 switch
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
opam install -y coq-serapi \
coq-smpl=8.12 coq-metacoq-template coq-metacoq-checker \
coq-equations \
coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-field \
menhir
# Install some coqgym deps that don't have the right versions in their
# official opam packages
git clone git@github.com:uwplse/StructTact.git deps/StructTact
(cd deps/StructTact && opam install -y . )
git clone git@github.com:DistributedComponents/InfSeqExt.git deps/InfSeqExt
(cd deps/InfSeqExt && opam install -y . )
# Cheerios has its own issues
git clone git@github.com:uwplse/cheerios.git deps/cheerios
(cd deps/cheerios && opam install -y --ignore-constraints-on=coq . )
(cd coq-projects/verdi && opam install -y --ignore-constraints-on=coq . )
(cd coq-projects/fcsl-pcm && make "$@" && make install)
# Finally, sync the opam state back to global
rsync -av --delete /tmp/${USER}_dot_opam/ $HOME/.opam.dir | tqdm --desc="Writing shared opam state" > /dev/null
perhaps useful: https://stackoverflow.com/questions/75452407/how-does-one-pin-freeze-a-version-of-the-dependencies-of-an-opam-project-package
related: #55
One of the projects in that first command made a change that broke compatibility without properly registering the old version with opam. This unfortunately happens, as many of these are research projects that don't pay the most attention to compatibility. To fix, you need to first figure out which project made the breaking change, which you can do with simple binary search (remove half the projects from the command, see if it installs properly. If it does, recurse on the other half, if it doesn't, recurse on the half that didn't install). Then clone the project from github and try to build it on coq 8.10, and see if it breaks. Sometimes it's only the opam metadata that's changed, and you will just be able to build it. If not, there was some recent commit which broke compatibility (possibly having to do with the global specifier, look for something about that in the commits), so try to track it down, and check out the commit before it. Then, remove the offending project from the first command, and add instructions to clone the proper commit for it in the "# Install some coqgym deps that don't have the right versions..." block. Test it to verify that it works, and then please make a pull request for the script changes so that future users can benefit from your work.
One of the projects in that first command made a change that broke compatibility without properly registering the old version with opam. This unfortunately happens, as many of these are research projects that don't pay the most attention to compatibility.
wouldn't this solve it?
No, that doesn't solve it. The submodule commits checked out for the coq-projects aren't relevant here, because the command that's failing isn't touching the coq-projects directory, it's installing dependencies from the internet to the internal opam directories. But the project authors are breaking invariants of opam package management, causing these problems with have to be resolved manually.
No, that doesn't solve it. The submodule commits checked out for the coq-projects aren't relevant here, because the command that's failing isn't touching the coq-projects directory, it's installing dependencies from the internet to the internal opam directories. But the project authors are breaking invariants of opam package management, causing these problems with have to be resolved manually.
I think I conceptually understand. So there is some underlying depedency in (for example) coq-cheerios that requires a different version. But cherioos isn't telling me which deps in breaking things:
(iit_synthesis) brando9~ $ eval $(opam env --switch=coq-8.10 --set-switch)
(iit_synthesis) brando9~ $
(iit_synthesis) brando9~ $
(iit_synthesis) brando9~ $ opam install -y coq-cheerios
[ERROR] Package conflict!
* Missing dependency:
- coq >= 8.14
not available because the package is pinned to version 8.10.2
No solution found, exiting
How does one fix this s.t. all versions of the ocaml/coq code fixed/pinned?
(Is there no way to pin everything to a specific version such that nothing ever changes so that this doesn't break again?)
The submodule commits checked out for the coq-projects aren't relevant here, because the command that's failing isn't touching the coq-projects directory
but is still an issue in the current set up, isn't it? (although yes it's perpendicular for now)
it's installing dependencies from the internet to the internal opam directories. But the project authors are breaking invariants of opam package management, causing these problems with have to be resolved manually.
curious, how did you know that this was the issue? i.e. an external deps for the coq-proj we are trying to build?
In python it's quite easy to pin a version with a requirements.txt file or a setup.py file. Does Coq/Ocaml/Opam not have this?
So, opam does allow you to pin a version of a specific package. The problem is, opam authors have full control over all the revisions of their package, and control which ones are available at any time. So, cheerios can have a version X.YY that works for us perfectly, and we tell opam to install it. But at any point, the cheerios authors can decide that they want to change version X.YY to rely on a newer Coq, without preserving the old version. In Pip, you would have to bump the version number to upload a new package, and users could always install the old version.
According to this page https://coq.inria.fr/opam/extra-dev/packages/coq-cheerios/, the only version of coq-cheerios available in opam is the dev version which follows the newest Coq. So it's constantly changing, and there isn't another version to pin to. If you want to transition all the packages to git checkouts so we can pin all the versions, and provide a script to test it, I'd be happy to merge it.
The ultimate solution is to stop installing any dependencies from opam, and rely instead on git cloning and checking out known commits. But doing stuff with opam is easier when it works, so I've just been transitioning packages from opam to git as-needed.
the cheerios authors can decide that they want to change version X.YY to rely on a newer Coq,
so we can't use a version of cheerios that is older and use the dependency version that we pin to that cheerios version (pin/freeze/fix both version so it always works for us? My understanding is that this is not possible because the authors can retroactively break version if they want? (though, does this happen often?)
I suppose in those edge cases we could fork a version, get requirements.txt (or however opam pins/freezes dependencies) and that way have a stable install that way). I suppose if they were very malicious or we were unluckly we'd have to fork every dependency too to avoid retroactive changes to past versions.
Is this more or less a correct understanding?
So, opam does allow you to pin a version of a specific package.
Not even via this method:
opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897
I must admit I am slightly puzzled why coq-cheerios is (maybe) working:
opam list
# Packages matching: installed
...
coq-cheerios dev pinned to version dev at git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d
...
I must have ran something like this:
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367
I can't verify but will leave this comment for future readers (e.g. myself XD).
for my issue I think this worked:
# -- Get cheerios, req to have old versions work in opam: https://github.com/uwplse/cheerios/issues/17
eval $(opam env --switch=coq-8.10 --set-switch)
# opam install might give issues since it gets the most recent version from the officialOPAM repository
#opam -y install coq-cheerios
# use opam pin since pin is created to install specific version (e.g. from git, local, etc.)
opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367
output:
(iit_synthesis) brando9~ $ opam pin add coq-cheerios git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367
[NOTE] Package coq-cheerios is currently pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367d (version dev).
Processing: [coq-cheerios.dev: git]
[coq-cheerios.dev] synchronised (no changes)
coq-cheerios is now pinned to git+https://github.com/uwplse/cheerios.git#9c7f66e57b91f706d70afa8ed99d64ed98ab367 (version dev)
The following actions will be performed:
∗ install coq-cheerios dev*
Do you want to continue? [Y/n]
[NOTE] Pinning command successful, but your installed packages may be out of sync.
(iit_synthesis) brando9~ $ opam switch
# switch compiler description
→ coq-8.10 ocaml-base-compiler.4.07.1 coq-8.10
default ocaml.5.0.0 default
[NOTE] Current switch is set locally through the OPAMSWITCH variable.
The current global system switch is unset.