coq icon indicating copy to clipboard operation
coq copied to clipboard

[dune] dune exec dev/shim/coqc-prelude on a fresh checkout

Open gares opened this issue 3 years ago • 3 comments

apparently the rules for the prelude are not generated:

File "dev/shim/dune", line 14, characters 0-384:
14 | (rule
15 |  (targets coqc-prelude)
16 |  (deps
17 |   %{bin:coqc}
18 |   %{project_root}/theories/Init/Prelude.vo)
19 |  (action
20 |   (with-stdout-to coqc-prelude
21 |    (progn
22 |     (echo "#!/usr/bin/env bash\n")
23 |     (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
24 |     (run chmod +x %{targets})))))
Error: No rule found for theories/Init/Prelude.vo

gares avatar Aug 04 '22 13:08 gares

Yup, very unfortunately you need to do make dunestrap for now.

ejgallego avatar Aug 04 '22 14:08 ejgallego

I remember hearing that a future dune version would let us remove the manual bootstrap, is that still expected someday?

SkySkimmer avatar Aug 29 '22 15:08 SkySkimmer

@SkySkimmer that's PR https://github.com/ocaml/dune/pull/5009 , yes, it'd be very helpful for it to land soon.

ejgallego avatar Aug 29 '22 16:08 ejgallego