[dune] [stdlib] Build the standard library natively with Dune.

This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?

1 files changed, 1 insertions, 20 deletions

diff --git a/dune b/dune
index d59346ed68..cf7221ce62 100644
--- a/dune
+++ b/dune
@@ -18,29 +18,10 @@
 ;
 ; (_ (flags :standard -rectypes)))
 
-; Rules for coq_dune
-(rule
- (targets .vfiles.d)
- (deps
-  (source_tree theories)
-  (source_tree plugins)
-  (source_tree user-contrib))
- (action
-  (with-stdout-to .vfiles.d
-   (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \
-          `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \
-          `find theories user-contrib -type f -name *.v`"))))
-
-(alias
- (name vodeps)
- (deps tools/coq_dune.exe .vfiles.d))
-  ; (action (run coq_dune .vfiles.d))))
-
 (install
  (section lib)
  (package coq)
- (files
-   revision))
+ (files revision))
 
 (rule
  (targets revision)