install_coqgym_deps.sh fails when running giant opam install -- due to coq-cheerios (only tried coq-cheerios)

[brando90]

I'm trying to do the following giant opam install:

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

but it fails because the previous command pins to coq 8.10.2

[ERROR] Package conflict!
  * Missing dependency:
    - coq >= 8.14
    not available because the package is pinned to version 8.10.2

No solution found, exiting

what would the solution be for this?

[brando90]

Found which one it was:

$ 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

I might on my own version of it for now that actually installs with whatever opam tells me (since idk how to resolve it to match your original stuff since I"m not a coq expert). But hence my post here :) hopefully it can help!

[brando90]

what would happen if I install all of them with 8.14? trying to figure out what I should do. Some coq projs won't get updated...so those can stay with your original setting I suppose

[HazardousPeach]

Agh yeah that script gets out of date pretty quickly unfortunately... What happens is the underlying coq projects are in various states of development activity, so it seems like one of those projects used to have a version which supported coq 8.10 when that script was last updated (a couple of months ago I think, unless something didn't make it to the main branches), but now they no longer support that version. Ideally folks would tag their version breaking commits and point opam at the tag for older versions of Coq, but these are often written by researchers so it's not their top priority. So, you can binary search that projects list to figure out which coq project has the incompatibility, then you have a couple of options. Option A: Proverbot currently supports Coq versions through 8.15.x, so you can just create a switch for newer Coq to move the project to. You just have to change the install, then change the "switch" field in the project splits json to point to your new switch. But if another project depends on the one that's not working, things will get tricky because you have to transitively move them. If you're lucky that works fine, but if one of the dependents doesn't support new enough Coq, then you're out of luck, and have to switch to option B. Option B: instead of installing that project via opam, find a git commit which is compatible with Coq 8.10 (shouldn't have to go too far back, since it worked recently), and install it directly through git. You might be able to do a git-commit-through-opam thing, not sure. If not, you might have to install transitive dependents through git too.

…

On Sat, Dec 10, 2022, 12:00 PM Brando Miranda ***@***.***> wrote: I'm trying to do the following giant opam install: 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 but it fails because the previous command pins to coq 8.10.2 [ERROR] Package conflict! * Missing dependency: - coq >= 8.14 not available because the package is pinned to version 8.10.2 No solution found, exiting what would the solution be for this? — Reply to this email directly, view it on GitHub <#55>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOEZG2UB4MUZ6QKYZBWF33WMTON7ANCNFSM6AAAAAAS2OYNII> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[brando90]

Option A: Proverbot currently supports Coq versions through 8.15.x, so you can just create a switch for newer Coq to move the project to. You just have to change the install, then change the "switch" field in the project splits json to point to your new switch. But if another project depends on the one that's not working, things will get tricky because you have to transitively move them. If you're lucky that works fine, but if one of the dependents doesn't support new enough Coq, then you're out of luck, and have to switch to option B. Option B: instead of installing that project via opam, find a git commit which is compatible with Coq 8.10 (shouldn't have to go too far back, since it worked recently), and install it directly through git. You might be able to do a git-commit-through-opam thing, not sure. If not, you might have to install transitive dependents through git too.

I think we should have recorded the commits for all the projects so that no one has to retroactively come back to fix it...is this possible to automate once a working version of all the installs with the different switches is give?

https://stackoverflow.com/questions/75452407/how-does-one-pin-freeze-a-version-of-the-dependencies-of-an-opam-project-package

[brando90]

related: #78

[brando90]

for cheerios

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.