coq
coq copied to clipboard
[dune] dune exec dev/shim/coqc-prelude on a fresh checkout
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
Yup, very unfortunately you need to do make dunestrap for now.
I remember hearing that a future dune version would let us remove the manual bootstrap, is that still expected someday?
@SkySkimmer that's PR https://github.com/ocaml/dune/pull/5009 , yes, it'd be very helpful for it to land soon.