[coq] Overlay for coq/coq#18385

[ejgallego]

No description provided.

[Alizter]

Are we missing the plugins field for the coq.theory stanzas?

[Alizter]

When I add the plugins field:

diff --git a/theories/dune b/theories/dune
index 7e3073666..4139942ab 100644
--- a/theories/dune
+++ b/theories/dune
@@ -6,4 +6,5 @@
 
 (coq.theory
  (name HoTT)
+ (plugins coq-core.plugins.ltac coq-core.plugins.number_string_notation)
  (package coq-hott))

I get:

Error: path outside the workspace:       
../../../../../../nix/store/yb1h6vdd03mr0mlzznsx9yfd183f0n2x-coq-8.19.1/lib/ocaml/4.14.2/site-lib/coq-core/META
from default/theories
-> required by _build/default/theories/Basics.glob
-> required by alias theories/all
-> required by alias default in dune:44

So it seems there is some bad interaction with the plugin loading and noinit.

[ejgallego]

That's an interesting bug due in Coq due to the workaround for ocaml/dune#5833 that was implemented in coqdep (cc: coq/coq#18165 )

So indeed, coqdep path normalization works fine for example in Coq's CI, however in build setups where Coq lives outside the build path, the normalization returns a path that is a bit non-sensical as it is relativized up to root.

We need to think a bit more how to handle this, best would be to solve Dune's bug.

[SkySkimmer]

seems to work better (more backwards compat) with the semi-legacy loading syntax

[SkySkimmer]

(after coq/coq#18385 the legacy part is ignored and prints a deprecation warning)

[Alizter]

Nice fix! I'm happy with this now.