Stream: Coq users

Topic: ✔ Unable to install coq dev with opam


view this post on Zulip Ali Caglayan (Jul 05 2021 at 13:31):

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[1]: *** [install-dune] Error 1
# make[1]: 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?

view this post on Zulip Ali Caglayan (Jul 05 2021 at 13:33):

Can anyone else check if coq dev is working?

view this post on Zulip Christian Doczkal (Jul 05 2021 at 14:09):

Installing coq.dev works just fine for me as of a couple of minutes ago.

view this post on Zulip Ali Caglayan (Jul 05 2021 at 14:23):

Hmm

view this post on Zulip Ali Caglayan (Jul 05 2021 at 14:23):

I wonder if it's because my .opam is syslinked to an external drive

view this post on Zulip Ali Caglayan (Jul 05 2021 at 14:47):

I also tried 8.14.dev and that hasn't worked

view this post on Zulip Ali Caglayan (Jul 05 2021 at 14:47):

I am getting the same error

view this post on Zulip Ali Caglayan (Jul 05 2021 at 16:56):

Looks like I messed up the opam switch. I created a new one and everything works fine now.

view this post on Zulip Ali Caglayan (Jul 05 2021 at 17:14):

hmm I take that back

view this post on Zulip Ali Caglayan (Jul 05 2021 at 17:14):

I didn't notice that the build actually failed the same way

view this post on Zulip Ali Caglayan (Jul 05 2021 at 23:19):

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

view this post on Zulip Ali Caglayan (Jul 05 2021 at 23:20):

Why does dune need to do anything with git at all?

view this post on Zulip Ali Caglayan (Jul 05 2021 at 23:20):

Or is this an opam problem?

view this post on Zulip Ali Caglayan (Jul 05 2021 at 23:20):

I am running opam 2.1

view this post on Zulip Théo Zimmermann (Jul 06 2021 at 08:18):

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)?

view this post on Zulip Théo Zimmermann (Jul 06 2021 at 08:19):

See the bottom of https://coq.inria.fr/opam-using.html for how to create new roots.

view this post on Zulip Ali Caglayan (Jul 06 2021 at 11:16):

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!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2021 at 14:27):

Coq does indeed try to call git as to produce the revision file, this is independent of Dune / make

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2021 at 14:27):

In the sense that make was doing the exact same call, see

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2021 at 14:27):

dev/tools/make_git_revision.sh

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:28):

Alright I just ran into the same issue again

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:28):

To reproduce create a switch install coq.dev

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:28):

then create another switch and install coq.dev in that

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:28):

the second one fails

view this post on Zulip Théo Zimmermann (Jul 06 2021 at 16:29):

Interesting! Likely an opam bug worth reporting, but I'll leave it to more expert opam users to confirm.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2021 at 16:33):

Indeed seems like something opam-specific

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:35):

Is anyone else able to confirm?

view this post on Zulip Ali Caglayan (Jul 06 2021 at 16:53):

As a workaround for now I am able to delete ~/.opam/dev/.opam-switch/sources/coq.dev/

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2021 at 17:06):

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

view this post on Zulip Ali Caglayan (Jul 15 2021 at 10:51):

I've posted the bug here https://github.com/ocaml/opam/issues/4751

view this post on Zulip Ali Caglayan (Jul 19 2021 at 12:56):

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...

view this post on Zulip Notification Bot (Jul 19 2021 at 12:56):

Ali Caglayan has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC