Lasse Blaauwbroek (Oct 18 2023 at 22:40): Lasse Blaauwbroek (Oct 18 2023 at 22:40):Has anyone ever tried installing Coq 8.16 with Dune >= 3.8? I'm getting this error:
- File "./_build_vo/default//lib/coq/theories/Init/Prelude.v", line 11, characters 0-25:
- Error: Cannot find a physical path bound to logical path Notations.
With Dune 3.7.1 it all works out. This might be related to this dune issue.
If I'm right, we should probably put an upper bound on Dune for the Coq8.16 packages. (But I'd like someone else to reproduce, because I'm surprised that no-one found this problem before me.)
Karl Palmskog (Oct 19 2023 at 06:36):8.16 works fine here with various Dune versions >= 3.8, such as 3.8.2 and 3.11.1
Emilio Jesús Gallego Arias (Oct 19 2023 at 08:44):@Lasse Blaauwbroek this, is a known bug, but only happens when you are vendoring Coq.
Emilio Jesús Gallego Arias (Oct 19 2023 at 08:45):The right issue is this one https://github.com/ocaml/dune/issues/7909 I think
Karl Palmskog (Oct 19 2023 at 08:45):@Lasse Blaauwbroek generally, the first notice we get when a combination of Coq and some dependency breaks is in the Coq Docker images.
You can see here that the image for 8.16 uses Dune 3.9 by clicking on the first digest link: https://explore.ggcr.dev/?image=coqorg/coq:8.16
Lasse Blaauwbroek (Oct 19 2023 at 10:48):Mhm, that is strange. I'm not vendoring Coq. Just a regular Opam install in a fresh switch. I must have screwed something up then. Thanks.
Last updated: Oct 13 2024 at 01:02 UTC