From 6bc3229ac5a4785880c8af87528722aab80cbb95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 9 Dec 2024 15:45:35 +0100 Subject: [PATCH] Use `rocq pp-mlg` for rocq-runtime files, move `coqpp` back to `coq-core` Not sure if `chdir %{project_root}` is correct or if it should be `%{workspace_root}` (this only matters for error messages). --- coqpp/dune | 4 +-- doc/plugin_tutorial/tuto0/src/dune | 5 ++- doc/plugin_tutorial/tuto1/src/dune | 5 ++- doc/plugin_tutorial/tuto2/src/dune | 5 ++- doc/plugin_tutorial/tuto3/src/dune | 5 ++- dune-project | 2 +- parsing/dune | 10 +++++- plugins/btauto/dune | 5 ++- plugins/cc/dune | 5 ++- plugins/derive/dune | 5 ++- plugins/extraction/dune | 5 ++- plugins/firstorder/dune | 5 ++- plugins/funind/dune | 5 ++- plugins/ltac/dune | 55 +++++++++++++++++++++++++++++- plugins/ltac2/dune | 5 ++- plugins/ltac2_ltac1/dune | 5 ++- plugins/micromega/dune | 10 +++++- plugins/nsatz/dune | 5 ++- plugins/ring/dune | 5 ++- plugins/rtauto/dune | 5 ++- plugins/ssr/dune | 15 +++++++- plugins/ssrmatching/dune | 5 ++- plugins/syntax/dune | 5 ++- stdlib/dune-project | 1 - toplevel/dune | 5 ++- vernac/dune | 15 +++++++- 26 files changed, 174 insertions(+), 28 deletions(-) diff --git a/coqpp/dune b/coqpp/dune index 6a1204d66be9..fc10b18b18a2 100644 --- a/coqpp/dune +++ b/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)) diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune index 32a15ea4710a..d4a882e5c94f 100644 --- a/doc/plugin_tutorial/tuto0/src/dune +++ b/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})))) diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune index 0754ae6b1034..a0deeffd411e 100644 --- a/doc/plugin_tutorial/tuto1/src/dune +++ b/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})))) diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index 11153897f500..43877b2e3e4f 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/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})))) diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune index c1cb39e518e6..b310191d6a62 100644 --- a/doc/plugin_tutorial/tuto3/src/dune +++ b/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})))) diff --git a/dune-project b/dune-project index 21109897ec75..8d7684cc59d1 100644 --- a/dune-project +++ b/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 diff --git a/parsing/dune b/parsing/dune index 8f3ae8639a70..eba467d73945 100644 --- a/parsing/dune +++ b/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}))))) diff --git a/plugins/btauto/dune b/plugins/btauto/dune index 4ed87eb8dae8..76fa2d7b2d7b 100644 --- a/plugins/btauto/dune +++ b/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})))) diff --git a/plugins/cc/dune b/plugins/cc/dune index e4ae27c4a83e..974e7c558adb 100644 --- a/plugins/cc/dune +++ b/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})))) diff --git a/plugins/derive/dune b/plugins/derive/dune index ce2fac8d320c..8482dea0f071 100644 --- a/plugins/derive/dune +++ b/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})))) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index 03650e691e4a..c2bc727e9977 100644 --- a/plugins/extraction/dune +++ b/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})))) diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune index 087e5234b27f..9da3d2ffae69 100644 --- a/plugins/firstorder/dune +++ b/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})))) diff --git a/plugins/funind/dune b/plugins/funind/dune index e3eb56362370..8a170e4a77a0 100644 --- a/plugins/funind/dune +++ b/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})))) diff --git a/plugins/ltac/dune b/plugins/ltac/dune index d7ab8215bdfb..885f9b00ec78 100644 --- a/plugins/ltac/dune +++ b/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})))) diff --git a/plugins/ltac2/dune b/plugins/ltac2/dune index 1163e7fbe7bb..d812d2990fad 100644 --- a/plugins/ltac2/dune +++ b/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})))) diff --git a/plugins/ltac2_ltac1/dune b/plugins/ltac2_ltac1/dune index d87100b3bcb5..1572d8f8fd10 100644 --- a/plugins/ltac2_ltac1/dune +++ b/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})))) diff --git a/plugins/micromega/dune b/plugins/micromega/dune index 7b7df2cfe3d6..9c995f2f22aa 100644 --- a/plugins/micromega/dune +++ b/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})))) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index 1970f64c12d7..a5ff46814122 100644 --- a/plugins/nsatz/dune +++ b/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})))) diff --git a/plugins/ring/dune b/plugins/ring/dune index e263d21fe8fd..10ad5dfef3f9 100644 --- a/plugins/ring/dune +++ b/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})))) diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune index 79a00a53d3a4..bccf74b584c5 100644 --- a/plugins/rtauto/dune +++ b/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})))) diff --git a/plugins/ssr/dune b/plugins/ssr/dune index 1f549f96e374..1e1b9c2ed181 100644 --- a/plugins/ssr/dune +++ b/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})))) diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune index a3eea1d4799d..f4d547b9b036 100644 --- a/plugins/ssrmatching/dune +++ b/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})))) diff --git a/plugins/syntax/dune b/plugins/syntax/dune index 72959e88cadf..333b0f6ad992 100644 --- a/plugins/syntax/dune +++ b/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})))) diff --git a/stdlib/dune-project b/stdlib/dune-project index 0a1760cae7db..189cf5f50819 100644 --- a/stdlib/dune-project +++ b/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 diff --git a/toplevel/dune b/toplevel/dune index 1fe1b5fa6c31..683859eb8ca4 100644 --- a/toplevel/dune +++ b/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})))) diff --git a/vernac/dune b/vernac/dune index 49e32c9046d0..0e35dccdd18a 100644 --- a/vernac/dune +++ b/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}))))