Merge PR #6857: [build] Preliminary support for building with `dune`.

19 files changed, 131 insertions, 4 deletions

diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune
new file mode 100644
index 0000000000..6a024358c3
--- /dev/null
+++ b/plugins/btauto/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name btauto_plugin)
+ (public_name coq.plugins.btauto)
+ (synopsis "Coq's btauto plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune
new file mode 100644
index 0000000000..2a92996d2a
--- /dev/null
+++ b/plugins/cc/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name cc_plugin)
+ (public_name coq.plugins.cc)
+ (synopsis "Coq's congruence closure plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune
new file mode 100644
index 0000000000..ba9cd595ce
--- /dev/null
+++ b/plugins/derive/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name derive_plugin)
+ (public_name coq.plugins.derive)
+ (synopsis "Coq's derive plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune
new file mode 100644
index 0000000000..037b0d5053
--- /dev/null
+++ b/plugins/extraction/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name extraction_plugin)
+ (public_name coq.plugins.extraction)
+ (synopsis "Coq's extraction plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
new file mode 100644
index 0000000000..bcbb99d9fc
--- /dev/null
+++ b/plugins/firstorder/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ground_plugin)
+ (public_name coq.plugins.ground)
+ (synopsis "Coq's first order logic solver plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune
new file mode 100644
index 0000000000..8cc76f6f9e
--- /dev/null
+++ b/plugins/fourier/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name fourier_plugin)
+ (public_name coq.plugins.fourier)
+ (synopsis "Coq's fourier plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
new file mode 100644
index 0000000000..002eb28eea
--- /dev/null
+++ b/plugins/funind/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name recdef_plugin)
+ (public_name coq.plugins.recdef)
+ (synopsis "Coq's functional induction plugin")
+ (libraries coq.plugins.extraction))
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
new file mode 100644
index 0000000000..5611f5ba16
--- /dev/null
+++ b/plugins/ltac/plugin_base.dune
@@ -0,0 +1,13 @@
+(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/plugin_base.dune b/plugins/micromega/plugin_base.dune
new file mode 100644
index 0000000000..0ae0e6855d
--- /dev/null
+++ b/plugins/micromega/plugin_base.dune
@@ -0,0 +1,7 @@
+(library
+ (name micromega_plugin)
+ (public_name coq.plugins.micromega)
+ ; be careful not to link the executable to the plugin!
+ (modules (:standard \ csdpcert))
+ (synopsis "Coq's micromega plugin")
+ (libraries num coq.plugins.ltac))
diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune
new file mode 100644
index 0000000000..9da5b39972
--- /dev/null
+++ b/plugins/nsatz/plugin_base.dune
@@ -0,0 +1,5 @@
+(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/plugin_base.dune b/plugins/omega/plugin_base.dune
new file mode 100644
index 0000000000..f512501c78
--- /dev/null
+++ b/plugins/omega/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name omega_plugin)
+ (public_name coq.plugins.omega)
+ (synopsis "Coq's omega plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune
new file mode 100644
index 0000000000..323906acb2
--- /dev/null
+++ b/plugins/quote/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name quote_plugin)
+ (public_name coq.plugins.quote)
+ (synopsis "Coq's quote plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune
new file mode 100644
index 0000000000..49b0e10edf
--- /dev/null
+++ b/plugins/romega/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name romega_plugin)
+ (public_name coq.plugins.romega)
+ (synopsis "Coq's romega plugin")
+ (libraries coq.plugins.omega))
diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune
new file mode 100644
index 0000000000..233845ae0f
--- /dev/null
+++ b/plugins/rtauto/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name rtauto_plugin)
+ (public_name coq.plugins.rtauto)
+ (synopsis "Coq's rtauto plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
new file mode 100644
index 0000000000..101246e28f
--- /dev/null
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name newring_plugin)
+ (public_name coq.plugins.setoid_ring)
+ (synopsis "Coq's setoid ring plugin")
+ (libraries coq.plugins.quote))
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune
new file mode 100644
index 0000000000..de9053f1a0
--- /dev/null
+++ b/plugins/ssr/plugin_base.dune
@@ -0,0 +1,6 @@
+(library
+ (name ssreflect_plugin)
+ (public_name coq.plugins.ssreflect)
+ (synopsis "Coq's ssreflect plugin")
+ (modules_without_implementation ssrast)
+ (libraries coq.plugins.ssrmatching))
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
new file mode 100644
index 0000000000..06f67c3774
--- /dev/null
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ssrmatching_plugin)
+ (public_name coq.plugins.ssrmatching)
+ (synopsis "Coq ssrmatching plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
new file mode 100644
index 0000000000..bfdd480fe9
--- /dev/null
+++ b/plugins/syntax/plugin_base.dune
@@ -0,0 +1,35 @@
+(library
+ (name numeral_notation_plugin)
+ (public_name coq.plugins.numeral_notation)
+ (synopsis "Coq numeral notation plugin")
+ (modules g_numeral numeral)
+ (libraries coq.plugins.ltac))
+
+(library
+ (name r_syntax_plugin)
+ (public_name coq.plugins.r_syntax)
+ (synopsis "Coq syntax plugin: reals")
+ (modules r_syntax)
+ (libraries coq.vernac))
+
+(library
+ (name ascii_syntax_plugin)
+ (public_name coq.plugins.ascii_syntax)
+ (synopsis "Coq syntax plugin: ASCII")
+ (modules ascii_syntax)
+ (libraries coq.vernac))
+
+(library
+ (name string_syntax_plugin)
+ (public_name coq.plugins.string_syntax)
+ (synopsis "Coq syntax plugin: strings")
+ (modules string_syntax)
+ (libraries coq.plugins.ascii_syntax))
+
+(library
+ (name int31_syntax_plugin)
+ (public_name coq.plugins.int31_syntax)
+ (synopsis "Coq syntax plugin: int31")
+ (modules int31_syntax)
+ (libraries coq.vernac))
+
diff --git a/plugins/xml/README b/plugins/xml/README
deleted file mode 100644
index 3128189929..0000000000
--- a/plugins/xml/README
+++ /dev/null
@@ -1,4 +0,0 @@
-The xml export plugin for Coq has been removed from the sources.
-A backward compatible plug-in will be provided as a third-party plugin.
-For more informations, contact
-Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>.