After aborting install, opam refuses to download package and then fails to install it

[RalfJung]

It started when I tried to install a new version of our package that has just been put into the repository:

opam update iris-dev
opam install coq-iris.branch.gen_proofmode.2018-03-05.3

Just replacing the previously installed version of coq-iris with this one would have worked, but opam went ahead and made a completely ridiculous suggestion:

The following actions will be performed:
  ⊘  remove    coq-mathcomp-ssreflect 1.6.4*                                                                 [conflicts with coq]
  ↘  downgrade camlp5                 7.05 to 7.00                                                           [required by coq]
  ↘  downgrade coq                    8.7.2 to 8.7.1                                                         [required by coq-iris]
  ↻  recompile coq-stdpp              dev.2018-02-23.0                                                       [uses coq]
  ↗  upgrade   coq-iris               branch.gen_proofmode.2018-03-05.0 to branch.gen_proofmode.2018-03-05.3 
===== ↻  1   ↗  1   ↘  2   ⊘  1 =====
Do you want to continue ? [Y/n] n

Of course I rejected. So I tried to pin instead, maybe that would result in a smarter solution?

opam pin add coq-iris branch.gen_proofmode.2018-03-05.3 -k version

Yes, the solution now is the one I want, but installation fails. And installation keeps failing, no matter how I try to convince opam to install this package. With more verbosity, the failure is:

+ /usr/bin/ocamlc "-vnum"
- 4.05.0
The following actions will be performed:
  ↗  upgrade coq-iris                 branch.gen_proofmode.2018-03-05.0 to branch.gen_proofmode.2018-03-05.3* [required by coq-lambda-rust-builddep]
  ∗  install coq-lambda-rust-builddep dev*                                                                    
===== ∗  1   ↗  1 =====
Do you want to continue ? [Y/n] y

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+ /usr/bin/make "-j8" (CWD=/home/r/.opam/coq-rust/.opam-switch/build/coq-iris.branch.gen_proofmode.2018-03-05.3)
- make: *** No targets specified and no makefile found.  Stop.
[ERROR] The compilation of coq-iris failed at "/usr/bin/make -j8".

#=== ERROR while compiling coq-iris.branch.gen_proofmode.2018-03-05.3 =========#
# context      2.0.0~rc | linux/x86_64 | ocaml-system.4.05.0 | pinned(git+https://gitlab.mpi-sws.org/FP/iris-coq.git#a74b8077f199e2d21ff49e91b5af0dfdcee362ff)
# path         ~/.opam/coq-rust/.opam-switch/build/coq-iris.branch.gen_proofmode.2018-03-05.3
# command      /usr/bin/make -j8
# exit-code    2
# env-file     ~/.opam/log/coq-iris-31586-ffb3fd.env
# output-file  ~/.opam/log/coq-iris-31586-ffb3fd.out
### output ###
# make: *** No targets specified and no makefile found.  Stop.

Well, yes -- "no makefile found" is correct. ~/.opam/coq-rust/.opam-switch/build/coq-iris.branch.gen_proofmode.2018-03-05.3 is just empty. opam forgot to download the sources for this package. I tried to delete that directory, but all opam does is just re-create it, empty.

I have since then successfully installed that same version of the same package in another switch -- the package is fine. But somehow, it seems one of my switches is now permanently broken and refuses to download this package? I didn't delete it yet in case you want me to run some stuff in it. I'm also a bit lost, I don't even know how opam knows not to re-download the package. There must be some state somewhere that I am missing.

This is the report from the broken switch:

# opam config report
# opam-version      2.0.0~rc 
# 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), 1 (local), 1 (version-controlled) (default repo at f405cb7f)
# pinned            1 (rsync), 2 (version)
# current-switch    coq-rust

[AltGr]

Thanks a lot for the detailed report

but opam went ahead and made a completely ridiculous suggestion

This is not normal, I believe it is an instance of #3232 / #3229 . I'll revert #3170 for RC2 and that should avoid these problems. In this case, pinning should not have been necessary (specifying the version for this package specifically is enough), but it changed the results just because of the issue with the solver.

Well, yes -- "no makefile found" is correct. ~/.opam/coq-rust/.opam-switch/build/coq-iris.branch.gen_proofmode.2018-03-05.3 is just empty.

This seems like it is another issue and looks similar to #3240. Haven't seen it before and I am now investigating. What does opam show coq-iris.branch.gen_proofmode.2018-03-05.3 --switch --raw show ? The backend is git, with a specific hash, while #3240 uses an archive over https, though... Could you please retry with -vv --debug ?

The downloads can be cached in ~/.opam/download-cache (by hash for archives, or directly the git objects) and <switch>/.opam-switch/sources (unpacked source).

[RalfJung]

"Unfortunately" it seems the issue fixed itself... I just tried opam install coq-iris again and it properly synchronized the source.

What does opam show coq-iris.branch.gen_proofmode.2018-03-05.3 --switch --raw show ?

opam-version: "2.0"
name: "coq-iris"
version: "branch.gen_proofmode.2018-03-05.3"
synopsis: "This is the Coq development of the Iris Project."
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
license: "BSD"
homepage: "http://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/FP/iris-coq/issues"
depends: [
"ocaml"
"coq" {>= "8.7.1" & < "8.8~" | (= "dev")}
"coq-stdpp" {(= "dev.2018-02-23.0") | (= "dev")}
]
flags: light-uninstall
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-coq.git"
url {
src:
"git+https://gitlab.mpi-sws.org/FP/iris-coq.git#a74b8077f199e2d21ff49e91b5af0dfdcee362ff"
}

[AltGr]

The bad solution was an instance of #3239 and should be fixed. Please reopen for the latter issue in case it happens again!