From 5db591257070734439dd5550995d6d3f497256c0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 22 Mar 2019 06:33:49 +0100 Subject: [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? --- plugins/btauto/dune | 7 +++++++ plugins/btauto/plugin_base.dune | 5 ----- plugins/cc/dune | 7 +++++++ plugins/cc/plugin_base.dune | 5 ----- plugins/derive/dune | 7 +++++++ plugins/derive/plugin_base.dune | 5 ----- plugins/extraction/dune | 7 +++++++ plugins/extraction/plugin_base.dune | 5 ----- plugins/firstorder/dune | 7 +++++++ plugins/firstorder/plugin_base.dune | 5 ----- plugins/funind/dune | 7 +++++++ plugins/funind/plugin_base.dune | 5 ----- plugins/ltac/dune | 15 +++++++++++++++ plugins/ltac/plugin_base.dune | 13 ------------- plugins/micromega/dune | 24 ++++++++++++++++++++++++ plugins/micromega/plugin_base.dune | 22 ---------------------- plugins/nsatz/dune | 7 +++++++ plugins/nsatz/plugin_base.dune | 5 ----- plugins/omega/dune | 7 +++++++ plugins/omega/plugin_base.dune | 5 ----- plugins/rtauto/dune | 7 +++++++ plugins/rtauto/plugin_base.dune | 5 ----- plugins/setoid_ring/dune | 7 +++++++ plugins/setoid_ring/plugin_base.dune | 5 ----- plugins/ssr/dune | 9 +++++++++ plugins/ssr/plugin_base.dune | 7 ------- plugins/ssrmatching/dune | 7 +++++++ plugins/ssrmatching/plugin_base.dune | 5 ----- plugins/syntax/dune | 36 ++++++++++++++++++++++++++++++++++++ plugins/syntax/plugin_base.dune | 34 ---------------------------------- 30 files changed, 161 insertions(+), 131 deletions(-) create mode 100644 plugins/btauto/dune delete mode 100644 plugins/btauto/plugin_base.dune create mode 100644 plugins/cc/dune delete mode 100644 plugins/cc/plugin_base.dune create mode 100644 plugins/derive/dune delete mode 100644 plugins/derive/plugin_base.dune create mode 100644 plugins/extraction/dune delete mode 100644 plugins/extraction/plugin_base.dune create mode 100644 plugins/firstorder/dune delete mode 100644 plugins/firstorder/plugin_base.dune create mode 100644 plugins/funind/dune delete mode 100644 plugins/funind/plugin_base.dune create mode 100644 plugins/ltac/dune delete mode 100644 plugins/ltac/plugin_base.dune create mode 100644 plugins/micromega/dune delete mode 100644 plugins/micromega/plugin_base.dune create mode 100644 plugins/nsatz/dune delete mode 100644 plugins/nsatz/plugin_base.dune create mode 100644 plugins/omega/dune delete mode 100644 plugins/omega/plugin_base.dune create mode 100644 plugins/rtauto/dune delete mode 100644 plugins/rtauto/plugin_base.dune create mode 100644 plugins/setoid_ring/dune delete mode 100644 plugins/setoid_ring/plugin_base.dune create mode 100644 plugins/ssr/dune delete mode 100644 plugins/ssr/plugin_base.dune create mode 100644 plugins/ssrmatching/dune delete mode 100644 plugins/ssrmatching/plugin_base.dune create mode 100644 plugins/syntax/dune delete mode 100644 plugins/syntax/plugin_base.dune (limited to 'plugins') diff --git a/plugins/btauto/dune b/plugins/btauto/dune new file mode 100644 index 0000000000..d2f5b65980 --- /dev/null +++ b/plugins/btauto/dune @@ -0,0 +1,7 @@ +(library + (name btauto_plugin) + (public_name coq.plugins.btauto) + (synopsis "Coq's btauto plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_btauto)) diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune deleted file mode 100644 index 6a024358c3..0000000000 --- a/plugins/btauto/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name btauto_plugin) - (public_name coq.plugins.btauto) - (synopsis "Coq's btauto plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/cc/dune b/plugins/cc/dune new file mode 100644 index 0000000000..f7fa3adb56 --- /dev/null +++ b/plugins/cc/dune @@ -0,0 +1,7 @@ +(library + (name cc_plugin) + (public_name coq.plugins.cc) + (synopsis "Coq's congruence closure plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_congruence)) diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune deleted file mode 100644 index 2a92996d2a..0000000000 --- a/plugins/cc/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name cc_plugin) - (public_name coq.plugins.cc) - (synopsis "Coq's congruence closure plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/derive/dune b/plugins/derive/dune new file mode 100644 index 0000000000..1931339471 --- /dev/null +++ b/plugins/derive/dune @@ -0,0 +1,7 @@ +(library + (name derive_plugin) + (public_name coq.plugins.derive) + (synopsis "Coq's derive plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_derive)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune deleted file mode 100644 index ba9cd595ce..0000000000 --- a/plugins/derive/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name derive_plugin) - (public_name coq.plugins.derive) - (synopsis "Coq's derive plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/extraction/dune b/plugins/extraction/dune new file mode 100644 index 0000000000..0c01dcd488 --- /dev/null +++ b/plugins/extraction/dune @@ -0,0 +1,7 @@ +(library + (name extraction_plugin) + (public_name coq.plugins.extraction) + (synopsis "Coq's extraction plugin") + (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_extraction)) diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune deleted file mode 100644 index 037b0d5053..0000000000 --- a/plugins/extraction/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name extraction_plugin) - (public_name coq.plugins.extraction) - (synopsis "Coq's extraction plugin") - (libraries num coq.plugins.ltac)) diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune new file mode 100644 index 0000000000..1b05452d8f --- /dev/null +++ b/plugins/firstorder/dune @@ -0,0 +1,7 @@ +(library + (name ground_plugin) + (public_name coq.plugins.firstorder) + (synopsis "Coq's first order logic solver plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ground)) diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune deleted file mode 100644 index d88daa23fc..0000000000 --- a/plugins/firstorder/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name ground_plugin) - (public_name coq.plugins.firstorder) - (synopsis "Coq's first order logic solver plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/funind/dune b/plugins/funind/dune new file mode 100644 index 0000000000..e594ffbd02 --- /dev/null +++ b/plugins/funind/dune @@ -0,0 +1,7 @@ +(library + (name recdef_plugin) + (public_name coq.plugins.funind) + (synopsis "Coq's functional induction plugin") + (libraries coq.plugins.extraction)) + +(coq.pp (modules g_indfun)) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune deleted file mode 100644 index 6ccf15df29..0000000000 --- a/plugins/funind/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name recdef_plugin) - (public_name coq.plugins.funind) - (synopsis "Coq's functional induction plugin") - (libraries coq.plugins.extraction)) diff --git a/plugins/ltac/dune b/plugins/ltac/dune new file mode 100644 index 0000000000..6558ecbfe8 --- /dev/null +++ b/plugins/ltac/dune @@ -0,0 +1,15 @@ +(library + (name ltac_plugin) + (public_name coq.plugins.ltac) + (synopsis "Coq's LTAC tactic language") + (modules :standard \ tauto) + (libraries coq.stm)) + +(library + (name tauto_plugin) + (public_name coq.plugins.tauto) + (synopsis "Coq's tauto tactic") + (modules tauto) + (libraries coq.plugins.ltac)) + +(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune deleted file mode 100644 index 5611f5ba16..0000000000 --- a/plugins/ltac/plugin_base.dune +++ /dev/null @@ -1,13 +0,0 @@ -(library - (name ltac_plugin) - (public_name coq.plugins.ltac) - (synopsis "Coq's LTAC tactic language") - (modules :standard \ tauto) - (libraries coq.stm)) - -(library - (name tauto_plugin) - (public_name coq.plugins.tauto) - (synopsis "Coq's tauto tactic") - (modules tauto) - (libraries coq.plugins.ltac)) diff --git a/plugins/micromega/dune b/plugins/micromega/dune new file mode 100644 index 0000000000..33ad3a0138 --- /dev/null +++ b/plugins/micromega/dune @@ -0,0 +1,24 @@ +(library + (name micromega_plugin) + (public_name coq.plugins.micromega) + ; be careful not to link the executable to the plugin! + (modules (:standard \ csdpcert g_zify zify)) + (synopsis "Coq's micromega plugin") + (libraries num coq.plugins.ltac)) + +(executable + (name csdpcert) + (public_name csdpcert) + (package coq) + (modules csdpcert) + (flags :standard -open Micromega_plugin) + (libraries coq.plugins.micromega)) + +(library + (name zify_plugin) + (public_name coq.plugins.zify) + (modules g_zify zify) + (synopsis "Coq's zify plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune deleted file mode 100644 index 4153d06161..0000000000 --- a/plugins/micromega/plugin_base.dune +++ /dev/null @@ -1,22 +0,0 @@ -(library - (name micromega_plugin) - (public_name coq.plugins.micromega) - ; be careful not to link the executable to the plugin! - (modules (:standard \ csdpcert g_zify zify)) - (synopsis "Coq's micromega plugin") - (libraries num coq.plugins.ltac)) - -(executable - (name csdpcert) - (public_name csdpcert) - (package coq) - (modules csdpcert) - (flags :standard -open Micromega_plugin) - (libraries coq.plugins.micromega)) - -(library - (name zify_plugin) - (public_name coq.plugins.zify) - (modules g_zify zify) - (synopsis "Coq's zify plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune new file mode 100644 index 0000000000..b921c9c408 --- /dev/null +++ b/plugins/nsatz/dune @@ -0,0 +1,7 @@ +(library + (name nsatz_plugin) + (public_name coq.plugins.nsatz) + (synopsis "Coq's nsatz solver plugin") + (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_nsatz)) diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune deleted file mode 100644 index 9da5b39972..0000000000 --- a/plugins/nsatz/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name nsatz_plugin) - (public_name coq.plugins.nsatz) - (synopsis "Coq's nsatz solver plugin") - (libraries num coq.plugins.ltac)) diff --git a/plugins/omega/dune b/plugins/omega/dune new file mode 100644 index 0000000000..0db71ed6fb --- /dev/null +++ b/plugins/omega/dune @@ -0,0 +1,7 @@ +(library + (name omega_plugin) + (public_name coq.plugins.omega) + (synopsis "Coq's omega plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_omega)) diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune deleted file mode 100644 index f512501c78..0000000000 --- a/plugins/omega/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name omega_plugin) - (public_name coq.plugins.omega) - (synopsis "Coq's omega plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune new file mode 100644 index 0000000000..43efa0eca5 --- /dev/null +++ b/plugins/rtauto/dune @@ -0,0 +1,7 @@ +(library + (name rtauto_plugin) + (public_name coq.plugins.rtauto) + (synopsis "Coq's rtauto plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_rtauto)) diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune deleted file mode 100644 index 233845ae0f..0000000000 --- a/plugins/rtauto/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name rtauto_plugin) - (public_name coq.plugins.rtauto) - (synopsis "Coq's rtauto plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/setoid_ring/dune b/plugins/setoid_ring/dune new file mode 100644 index 0000000000..60522cd3f5 --- /dev/null +++ b/plugins/setoid_ring/dune @@ -0,0 +1,7 @@ +(library + (name newring_plugin) + (public_name coq.plugins.setoid_ring) + (synopsis "Coq's setoid ring plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_newring)) diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune deleted file mode 100644 index d83857edad..0000000000 --- a/plugins/setoid_ring/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name newring_plugin) - (public_name coq.plugins.setoid_ring) - (synopsis "Coq's setoid ring plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/ssr/dune b/plugins/ssr/dune new file mode 100644 index 0000000000..a117d09a16 --- /dev/null +++ b/plugins/ssr/dune @@ -0,0 +1,9 @@ +(library + (name ssreflect_plugin) + (public_name coq.plugins.ssreflect) + (synopsis "Coq's ssreflect plugin") + (modules_without_implementation ssrast) + (flags :standard -open Gramlib) + (libraries coq.plugins.ssrmatching)) + +(coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune deleted file mode 100644 index a13524bb52..0000000000 --- a/plugins/ssr/plugin_base.dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name ssreflect_plugin) - (public_name coq.plugins.ssreflect) - (synopsis "Coq's ssreflect plugin") - (modules_without_implementation ssrast) - (flags :standard -open Gramlib) - (libraries coq.plugins.ssrmatching)) diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune new file mode 100644 index 0000000000..629d723816 --- /dev/null +++ b/plugins/ssrmatching/dune @@ -0,0 +1,7 @@ +(library + (name ssrmatching_plugin) + (public_name coq.plugins.ssrmatching) + (synopsis "Coq ssrmatching plugin") + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ssrmatching)) diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune deleted file mode 100644 index 06f67c3774..0000000000 --- a/plugins/ssrmatching/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name ssrmatching_plugin) - (public_name coq.plugins.ssrmatching) - (synopsis "Coq ssrmatching plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/syntax/dune b/plugins/syntax/dune new file mode 100644 index 0000000000..b395695c8a --- /dev/null +++ b/plugins/syntax/dune @@ -0,0 +1,36 @@ +(library + (name numeral_notation_plugin) + (public_name coq.plugins.numeral_notation) + (synopsis "Coq numeral notation plugin") + (modules g_numeral numeral) + (libraries coq.vernac)) + +(library + (name string_notation_plugin) + (public_name coq.plugins.string_notation) + (synopsis "Coq string notation plugin") + (modules g_string string_notation) + (libraries coq.vernac)) + +(library + (name r_syntax_plugin) + (public_name coq.plugins.r_syntax) + (synopsis "Coq syntax plugin: reals") + (modules r_syntax) + (libraries coq.vernac)) + +(library + (name int63_syntax_plugin) + (public_name coq.plugins.int63_syntax) + (synopsis "Coq syntax plugin: int63") + (modules int63_syntax) + (libraries coq.vernac)) + +(library + (name float_syntax_plugin) + (public_name coq.plugins.float_syntax) + (synopsis "Coq syntax plugin: float") + (modules float_syntax) + (libraries coq.vernac)) + +(coq.pp (modules g_numeral g_string)) diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune deleted file mode 100644 index 512752135d..0000000000 --- a/plugins/syntax/plugin_base.dune +++ /dev/null @@ -1,34 +0,0 @@ -(library - (name numeral_notation_plugin) - (public_name coq.plugins.numeral_notation) - (synopsis "Coq numeral notation plugin") - (modules g_numeral numeral) - (libraries coq.vernac)) - -(library - (name string_notation_plugin) - (public_name coq.plugins.string_notation) - (synopsis "Coq string notation plugin") - (modules g_string string_notation) - (libraries coq.vernac)) - -(library - (name r_syntax_plugin) - (public_name coq.plugins.r_syntax) - (synopsis "Coq syntax plugin: reals") - (modules r_syntax) - (libraries coq.vernac)) - -(library - (name int63_syntax_plugin) - (public_name coq.plugins.int63_syntax) - (synopsis "Coq syntax plugin: int63") - (modules int63_syntax) - (libraries coq.vernac)) - -(library - (name float_syntax_plugin) - (public_name coq.plugins.float_syntax) - (synopsis "Coq syntax plugin: float") - (modules float_syntax) - (libraries coq.vernac)) -- cgit v1.2.3