Use rocq pp-mlg for rocq-runtime files, move coqpp back to `coq-c…

…ore`

Not sure if `chdir %{project_root}` is correct or if it should be
`%{workspace_root}` (this only matters for error messages).

coqpp/dune

@@ -7,11 +7,9 @@
  (modules :standard \ coqpp)
  (modules_without_implementation coqpp_ast))
 
-; dune's coq.pp uses this,
-; so if we put it in coq-core we can't use coq.pp for rocq-runtime
 (executable
  (public_name coqpp)
  (empty_module_interface_if_absent)
- (package rocq-runtime)
+ (package coq-core)
  (libraries coqpp)
  (modules coqpp))

doc/plugin_tutorial/tuto0/src/dune

@@ -3,4 +3,7 @@
  (public_name rocq-runtime.plugins.tutorial.p0)
  (libraries rocq-runtime.plugins.ltac))
 
-(coq.pp (modules g_tuto0))
+(rule
+ (targets g_tuto0.ml)
+ (deps (:mlg g_tuto0.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

doc/plugin_tutorial/tuto1/src/dune

@@ -3,4 +3,7 @@
  (public_name rocq-runtime.plugins.tutorial.p1)
  (libraries rocq-runtime.plugins.ltac))
 
-(coq.pp (modules g_tuto1))
+(rule
+ (targets g_tuto1.ml)
+ (deps (:mlg g_tuto1.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

doc/plugin_tutorial/tuto2/src/dune

@@ -3,4 +3,7 @@
  (public_name rocq-runtime.plugins.tutorial.p2)
  (libraries rocq-runtime.plugins.ltac))
 
-(coq.pp (modules g_tuto2))
+(rule
+ (targets g_tuto2.ml)
+ (deps (:mlg g_tuto2.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

doc/plugin_tutorial/tuto3/src/dune

@@ -4,4 +4,7 @@
  (flags :standard -warn-error -3)
  (libraries rocq-runtime.plugins.ltac))
 
-(coq.pp (modules g_tuto3))
+(rule
+ (targets g_tuto3.ml)
+ (deps (:mlg g_tuto3.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

dune-project

@@ -4,7 +4,7 @@
 ; We use directory targets in documentation
 (using directory-targets 0.1)
 
-; We need this due to `(coq.pp )` declarations
+; We need this for when we use the dune.disabled files instead of our rule_gen
 (using coq 0.8)
 
 (formatting

parsing/dune

@@ -9,4 +9,12 @@
  (old_public_name coq-core.parsing)
  (new_public_name rocq-runtime.parsing))
 
-(coq.pp (modules g_prim g_constr))
+(rule
+ (targets g_prim.ml)
+ (deps (:mlg g_prim.mlg))
+ (action (chdir %{project_root} (chdir %{project_root} (run rocq pp-mlg %{deps})))))
+
+(rule
+ (targets g_constr.ml)
+ (deps (:mlg g_constr.mlg))
+ (action (chdir %{project_root} (chdir %{project_root} (run rocq pp-mlg %{deps})))))

plugins/btauto/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.btauto)
  (new_public_name rocq-runtime.plugins.btauto))
 
-(coq.pp (modules g_btauto))
+(rule
+ (targets g_btauto.ml)
+ (deps (:mlg g_btauto.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/cc/dune

@@ -21,4 +21,7 @@
  (old_public_name coq-core.plugins.cc)
  (new_public_name rocq-runtime.plugins.cc))
 
-(coq.pp (modules g_congruence))
+(rule
+ (targets g_congruence.ml)
+ (deps (:mlg g_congruence.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/derive/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.derive)
  (new_public_name rocq-runtime.plugins.derive))
 
-(coq.pp (modules g_derive))
+(rule
+ (targets g_derive.ml)
+ (deps (:mlg g_derive.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/extraction/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.extraction)
  (new_public_name rocq-runtime.plugins.extraction))
 
-(coq.pp (modules g_extraction))
+(rule
+ (targets g_extraction.ml)
+ (deps (:mlg g_extraction.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/firstorder/dune

@@ -21,4 +21,7 @@
  (old_public_name coq-core.plugins.firstorder)
  (new_public_name rocq-runtime.plugins.firstorder))
 
-(coq.pp (modules g_ground))
+(rule
+ (targets g_ground.ml)
+ (deps (:mlg g_ground.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/funind/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.funind)
  (new_public_name rocq-runtime.plugins.funind))
 
-(coq.pp (modules g_indfun))
+(rule
+ (targets g_indfun.ml)
+ (deps (:mlg g_indfun.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ltac/dune

@@ -21,4 +21,57 @@
  (old_public_name coq-core.plugins.tauto)
  (new_public_name rocq-runtime.plugins.tauto))
 
-(coq.pp (modules extratactics g_tactic  g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
+(rule
+ (targets extratactics.ml)
+ (deps (:mlg extratactics.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_tactic.ml)
+ (deps (:mlg g_tactic.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_rewrite.ml)
+ (deps (:mlg g_rewrite.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_eqdecide.ml)
+ (deps (:mlg g_eqdecide.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_auto.ml)
+ (deps (:mlg g_auto.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_obligations.ml)
+ (deps (:mlg g_obligations.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_ltac.ml)
+ (deps (:mlg g_ltac.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets profile_ltac_tactics.ml)
+ (deps (:mlg profile_ltac_tactics.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets coretactics.ml)
+ (deps (:mlg coretactics.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_class.ml)
+ (deps (:mlg g_class.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets extraargs.ml)
+ (deps (:mlg extraargs.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ltac2/dune

@@ -9,4 +9,7 @@
  (old_public_name coq-core.plugins.ltac2)
  (new_public_name rocq-runtime.plugins.ltac2))
 
-(coq.pp (modules g_ltac2))
+(rule
+ (targets g_ltac2.ml)
+ (deps (:mlg g_ltac2.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ltac2_ltac1/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.ltac2_ltac1)
  (new_public_name rocq-runtime.plugins.ltac2_ltac1))
 
-(coq.pp (modules g_ltac2_ltac1))
+(rule
+ (targets g_ltac2_ltac1.ml)
+ (deps (:mlg g_ltac2_ltac1.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/micromega/dune

@@ -41,4 +41,12 @@
  (old_public_name coq-core.plugins.zify)
  (new_public_name rocq-runtime.plugins.zify))
 
-(coq.pp (modules g_micromega g_zify))
+(rule
+ (targets g_micromega.ml)
+ (deps (:mlg g_micromega.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_zify.ml)
+ (deps (:mlg g_zify.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/nsatz/dune

@@ -21,4 +21,7 @@
  (old_public_name coq-core.plugins.nsatz)
  (new_public_name rocq-runtime.plugins.nsatz))
 
-(coq.pp (modules g_nsatz))
+(rule
+ (targets g_nsatz.ml)
+ (deps (:mlg g_nsatz.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ring/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.ring)
  (new_public_name rocq-runtime.plugins.ring))
 
-(coq.pp (modules g_ring))
+(rule
+ (targets g_ring.ml)
+ (deps (:mlg g_ring.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/rtauto/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.rtauto)
  (new_public_name rocq-runtime.plugins.rtauto))
 
-(coq.pp (modules g_rtauto))
+(rule
+ (targets g_rtauto.ml)
+ (deps (:mlg g_rtauto.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ssr/dune

@@ -10,4 +10,17 @@
  (old_public_name coq-core.plugins.ssreflect)
  (new_public_name rocq-runtime.plugins.ssreflect))
 
-(coq.pp (modules ssrvernac ssrparser ssrtacs))
+(rule
+ (targets ssrvernac.ml)
+ (deps (:mlg ssrvernac.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets ssrparser.ml)
+ (deps (:mlg ssrparser.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets ssrtacs.ml)
+ (deps (:mlg ssrtacs.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/ssrmatching/dune

@@ -8,4 +8,7 @@
  (old_public_name coq-core.plugins.ssrmatching)
  (new_public_name rocq-runtime.plugins.ssrmatching))
 
-(coq.pp (modules g_ssrmatching))
+(rule
+ (targets g_ssrmatching.ml)
+ (deps (:mlg g_ssrmatching.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

plugins/syntax/dune

@@ -9,4 +9,7 @@
  (old_public_name coq-core.plugins.number_string_notation)
  (new_public_name rocq-runtime.plugins.number_string_notation))
 
-(coq.pp (modules g_number_string))
+(rule
+ (targets g_number_string.ml)
+ (deps (:mlg g_number_string.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

stdlib/dune-project

@@ -4,7 +4,6 @@
 ; We use directory targets in documentation
 (using directory-targets 0.1)
 
-; We need this due to `(coq.pp )` declarations
 (using coq 0.8)
 
 (formatting

toplevel/dune

@@ -17,4 +17,7 @@
 ; Interp provides the `zarith` library to plugins, we could also use
 ; -linkall in the plugins file, to be discussed.
 
-(coq.pp (modules g_toplevel))
+(rule
+ (targets g_toplevel.ml)
+ (deps (:mlg g_toplevel.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))

vernac/dune

@@ -12,4 +12,17 @@
  (old_public_name coq-core.vernac)
  (new_public_name rocq-runtime.vernac))
 
-(coq.pp (modules g_proofs g_vernac g_redexpr))
+(rule
+ (targets g_proofs.ml)
+ (deps (:mlg g_proofs.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_vernac.ml)
+ (deps (:mlg g_vernac.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))
+
+(rule
+ (targets g_redexpr.ml)
+ (deps (:mlg g_redexpr.mlg))
+ (action (chdir %{project_root} (run rocq pp-mlg %{deps}))))