I am getting this error trying to install coq dev today via opam:
[ERROR] The installation of coq failed at "make install". #=== ERROR while installing coq.dev ===========================================# # context 2.1.0~rc2 | linux/x86_64 | ocaml-variants.4.11.2+flambda | https://coq.inria.fr/opam/core-dev#2021-07-02 15:00 # path /mnt/sdd1/.opam/coq-hott-dep/.opam-switch/build/coq.dev # command /mnt/sdd1/.opam/opam-init/hooks/sandbox.sh install make install # exit-code 2 # env-file /mnt/sdd1/.opam/log/coq-30704-f27909.env # output-file /mnt/sdd1/.opam/log/coq-30704-f27909.out ### output ### # [...] # DUNE sources # dune install --display quiet --mandir=""/mnt/sdd1/.opam/coq-hott-dep/man"" --prefix="/mnt/sdd1/.opam/coq-hott-dep" coq-core # Installing /mnt/sdd1/.opam/coq-hott-dep/lib/coq-core/META # git (internal) (exit 128) # /usr/bin/git describe --always --dirty > /tmp/dunebf3fc1.output # error: object directory /mnt/sdd1/.opam/download-cache/git/objects does not exist; check .git/objects/info/alternates. # fatal: unable to read tree d7cf1571dc8ea55a0866ce47df23d39c4c38e503 # Makefile.install:56: recipe for target 'install-dune' failed # make: *** [install-dune] Error 1 # make: Leaving directory '/mnt/sdd1/.opam/coq-hott-dep/.opam-switch/build/coq.dev' # Makefile.make:122: recipe for target 'submake' failed # make: *** [submake] Error 2
Not really sure what is going on?
Can anyone else check if coq dev is working?
coq.dev works just fine for me as of a couple of minutes ago.
I wonder if it's because my .opam is syslinked to an external drive
I also tried 8.14.dev and that hasn't worked
I am getting the same error
Looks like I messed up the opam switch. I created a new one and everything works fine now.
hmm I take that back
I didn't notice that the build actually failed the same way
OK so randomly in the middle of the build dune is throwing an error causing opam to fail:
- COQC theories/Numbers/Integer/Abstract/ZDivFloor.v - COQC theories/Numbers/Integer/Abstract/ZGcd.v - COQC theories/Numbers/Integer/Abstract/ZDivEucl.v - COQC theories/Numbers/Integer/Abstract/ZLcm.v - COQC theories/Numbers/Integer/Abstract/ZBits.v - bash revision - error: object directory /mnt/sdd1/.opam/download-cache/git/objects does not exist; check .git/objects/info/alternates. - error: object directory /mnt/sdd1/.opam/download-cache/git/objects does not exist; check .git/objects/info/alternates. - error: Could not read d91d22da976a89c42c2904b5cbdf0344dc6fdba9 - fatal: Failed to traverse parents of commit 8560c27c81f8622f3f3e5a430c70336d46d4c547 - COQC theories/Numbers/Natural/Abstract/NProperties.v - COQC theories/Arith/PeanoNat.v - COQC theories/Arith/Le.v - COQC theories/Arith/EqNat.v - COQC theories/Lists/List.v
Why does dune need to do anything with git at all?
Or is this an opam problem?
I am running opam 2.1
Could it be due to having pinned the Coq version to the one from the git repository at some point? Anyway, this looks like your
.opam root might be corrupted. Can you try creating a new one (or removing this one and starting from scratch)?
See the bottom of https://coq.inria.fr/opam-using.html for how to create new roots.
I had a lot of switches in my .opam so I have made a backup, but it looks like the update to 2.1 may have corrupted something as you say. I did a fresh .opam and everything works fine now!
Coq does indeed try to call git as to produce the
revision file, this is independent of Dune / make
In the sense that make was doing the exact same call, see
Alright I just ran into the same issue again
To reproduce create a switch install coq.dev
then create another switch and install coq.dev in that
the second one fails
Interesting! Likely an opam bug worth reporting, but I'll leave it to more expert opam users to confirm.
Indeed seems like something opam-specific
Is anyone else able to confirm?
As a workaround for now I am able to delete
I'd go ahead and file an opam bug report, but you could very easily do an opam package with does just generate the
revision file and see what happens
I've posted the bug here https://github.com/ocaml/opam/issues/4751
I am unable to produce this error now, and the only thing that has changed is the version of coq dev. This leads me to believe that it was a coq problem to begin with. I really tried debugging it with the opam devs but I couldn't work out what went wrong at the time. I'm not sure what has changed in master that could fix this behaviour...
Ali Caglayan has marked this topic as resolved.
Last updated: Jan 29 2023 at 05:03 UTC