Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

opam compiles the wrong sources after overwriting a pin #3651

Closed
RalfJung opened this Issue Nov 3, 2018 · 2 comments

Comments

Projects
None yet
3 participants
@RalfJung
Copy link

RalfJung commented Nov 3, 2018

opam somehow managed to fetch the wrong sources for one of the packages. I wanted to downgrade coq from 8.9.dev to 8.8.2, and what opam ended up doing is compile the 8.9.dev sources with the opam files for 8.8.2. That didn't work out so well because some binaries got removed since then.

Basically, #3262 is back.

Here's the commands I ran:

opam install coq-stdpp.1.1.0 # failed because not compatible with coq.8.9.dev
opam install coq.8.8.2 # failed because 8.9.dev is pinned
opam pin coq 8.8.2 # replaced the pin but failed to build because it used the wrong sources

The output:

r@r-thinktop:~ [coq-test]$ opam install coq.8.8.2

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq.8.9.dev] synchronised from git+https://github.com/coq/coq.git#v8.9

[ERROR] coq = 8.8.2 not available because the package is pinned to version 8.9.dev
r@r-thinktop:~ [coq-test]$ opam pin coq 8.8.2
[NOTE] Package coq used to be pinned to version 8.9.dev
coq is now pinned to version 8.8.2

The following actions will be performed:
  ↘ downgrade coq               8.9.dev to 8.8.2*
  ↻ recompile coq-stdpp         dev.2018-10-15.1.b7f1f6b1 [uses coq]
  ↻ recompile coq-iris-builddep dev*                      [uses coq]
===== ↻ 2   ↘ 1 =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-stdpp.dev.2018-10-15.1.b7f1f6b1] no changes from git+https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git#b7f1f6b178091ca6e3d363208d7875d73321903c

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   coq-iris-builddep.dev
⊘ removed   coq-stdpp.dev.2018-10-15.1.b7f1f6b1
⊘ removed   coq.8.9.dev
[ERROR] Installation of coq.8.8.2 failed

#=== ERROR while installing coq.8.8.2 =========================================#
Some files in /home/r/.opam/coq-test/.opam-switch/install/coq.install couldn't be installed:
  - /home/r/.opam/coq-test/.opam-switch/build/coq.8.8.2/bin/gallina to /home/r/.opam/coq-test/bin



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ∗ install coq 8.8.2
└─ 
┌─ The following changes have been performed (the rest was aborted)
│ ⊘ remove coq               8.9.dev
│ ⊘ remove coq-iris-builddep dev
│ ⊘ remove coq-stdpp         dev.2018-10-15.1.b7f1f6b1
└─ 
[NOTE] Pinning command successful, but your installed packages may be out of sync.

The former state can be restored with:
    opam switch import "/home/r/.opam/coq-test/.opam-switch/backup/state-20181103173624.export"
Or you can retry to install your package selection with:
    opam install --restore

I guess I could fix this switch by deleting /home/r/.opam/coq-test/.opam-switch/build/coq.8.8.2 but I do not need this switch so I will just leave it as-is.

# opam config report
# opam-version      2.0.1 
# self-upgrade      no
# system            arch=x86_64 os=linux os-distribution=debian os-version=testing
# solver            builtin-mccs+glpk
# install-criteria  -removed,-count[version-lag,request],-count[version-lag,changed],-changed
# upgrade-criteria  -removed,-count[version-lag,solution],-new
# jobs              8
# repositories      4 (http), 4 (local), 1 (version-controlled) (default repo at 7ed1cc7a)
# pinned            1 (git), 1 (rsync), 1 (version)
# current-switch    coq-test

@RalfJung RalfJung changed the title opam downloaded the wrong sources opam compiles the wrong sources after overwriting a pin Nov 3, 2018

@AltGr

This comment has been minimized.

Copy link
Member

AltGr commented Nov 5, 2018

Thanks for the detailed report.
I wonder what made you think that opam used the wrong sources though ? I couldn't find the clues leading to this in the log. Is it by looking at what was in /home/r/.opam/coq-test/.opam-switch/build/coq.8.8.2 ?

What I could notice from the logs and might help you, though:

  • the log mentions that install coq 8.8.2 failed. Which implies that the build actually worked!

  • Some files couldn't be installed [...] bin/gallina. This file is listed in files/coq.install in the "official" package for coq.8.8.2 (also, the package uses both an install: directive and a .install file; that is allowed, but discouraged. The install: directive will get executed first, so it must have been successful as well.)

  • coq.8.9 doesn't seem to have any in-source package definition, so I imagine you ported or adapted the one for 8.8.2 manually? Shouldn't really matter though, since we are supposed to be building 8.8.2 here.

  • Deleting .opam-switch/build/coq.8.8.2 won't help: this temporary directory is kept in case of errors to help with debugging, but opam will always junk it and start fresh when building.

@RalfJung

This comment has been minimized.

Copy link
Author

RalfJung commented Nov 5, 2018

Is it by looking at what was in /home/r/.opam/coq-test/.opam-switch/build/coq.8.8.2 ?

Sorry I should have mentioned. It is exactly that: I went there, and the CHANGELOG contained stuff that was never added in the 8.8 branch. It was clearly from the 8.9 branch.

Which implies that the build actually worked!

Yes, the build commands are the same for both versions. However, a binary got removed, and hence opam using the 8.8.2 install file failed to copy that binary.

coq.8.9 doesn't seem to have any in-source package definition, so I imagine you ported or adapted the one for 8.8.2 manually? Shouldn't really matter though, since we are supposed to be building 8.8.2 here.

8.9.dev is from the repo at https://github.com/coq/opam-coq-archive/tree/master/core-dev (deployed at https://coq.inria.fr/opam/core-dev/ but that server seems to be down right now).

@rjbou rjbou closed this in #3726 Jan 25, 2019

@rjbou rjbou added this to the 2.0.4 milestone Jan 25, 2019

@rjbou rjbou modified the milestones: 2.0.4, 2.1.0 Feb 28, 2019

@rjbou rjbou modified the milestones: 2.1.0, 2.0.4 Mar 28, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.