[dev] Autogenerate OCaml dev files.

For now we only copy the templates, but we could do more fancy stuff.

This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579

1 files changed, 555 insertions, 0 deletions

diff --git a/META.coq.in b/META.coq.in
new file mode 100644
index 000000000..a7c8da163
--- /dev/null
+++ b/META.coq.in
@@ -0,0 +1,555 @@
+# TODO: Generate automatically with Dune
+
+description = "The Coq Proof Assistant Plugin API"
+version = "8.9"
+
+directory = ""
+requires = "camlp5"
+
+package "grammar" (
+
+  description = "Coq Camlp5 Grammar Extensions for Plugins"
+  version     = "8.9"
+
+  requires    = "camlp5.gramlib"
+  directory   = "grammar"
+
+  archive(byte)   = "grammar.cma"
+  archive(native) = "grammar.cmxa"
+)
+
+package "config" (
+
+  description = "Coq Configuration Variables"
+  version     = "8.9"
+
+  directory   = "config"
+
+)
+
+package "clib" (
+  description = "Base General Coq Library"
+  version     = "8.9"
+
+  directory   = "clib"
+  requires    = "num, str, unix, threads"
+
+  archive(byte)    = "clib.cma"
+  archive(native)  = "clib.cmxa"
+)
+
+package "lib" (
+
+  description = "Base Coq-Specific Library"
+  version     = "8.9"
+
+  directory   = "lib"
+
+  requires    = "coq.clib, coq.config"
+
+  archive(byte)   = "lib.cma"
+  archive(native) = "lib.cmxa"
+
+)
+
+package "vm" (
+
+  description = "Coq VM"
+  version     = "8.9"
+
+  directory        = "kernel/byterun"
+
+# We could generate this file at configure time for the share byte
+# build path to work properly.
+#
+# Enable this setting for local byte builds if you want dynamic linking:
+#
+#  linkopts(byte)   = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"
+
+# We currently prefer static linking of the VM.
+  archive(byte)    = "libcoqrun.a"
+  linkopts(byte)   = "-custom"
+)
+
+package "kernel" (
+
+  description = "Coq's Kernel"
+  version     = "8.9"
+
+  directory   = "kernel"
+
+  requires    = "dynlink, coq.lib, coq.vm"
+
+  archive(byte)    = "kernel.cma"
+  archive(native)  = "kernel.cmxa"
+
+)
+
+package "library" (
+
+  description = "Coq Libraries (vo) support"
+  version     = "8.9"
+
+  requires    = "coq.kernel"
+
+  directory   = "library"
+
+  archive(byte)    = "library.cma"
+  archive(native)  = "library.cmxa"
+
+)
+
+package "engine" (
+
+  description = "Coq Tactic Engine"
+  version     = "8.9"
+
+  requires    = "coq.library"
+  directory   = "engine"
+
+  archive(byte)    = "engine.cma"
+  archive(native)  = "engine.cmxa"
+
+)
+
+package "pretyping" (
+
+  description = "Coq Pretyper"
+  version     = "8.9"
+
+  requires    = "coq.engine"
+  directory   = "pretyping"
+
+  archive(byte)    = "pretyping.cma"
+  archive(native)  = "pretyping.cmxa"
+
+)
+
+package "interp" (
+
+  description = "Coq Term Interpretation"
+  version     = "8.9"
+
+  requires    = "coq.pretyping"
+  directory   = "interp"
+
+  archive(byte)    = "interp.cma"
+  archive(native)  = "interp.cmxa"
+
+)
+
+package "proofs" (
+
+  description = "Coq Proof Engine"
+  version     = "8.9"
+
+  requires    = "coq.interp"
+  directory   = "proofs"
+
+  archive(byte)    = "proofs.cma"
+  archive(native)  = "proofs.cmxa"
+
+)
+
+package "parsing" (
+
+  description = "Coq Parsing Engine"
+  version     = "8.9"
+
+  requires    = "camlp5.gramlib, coq.proofs"
+  directory   = "parsing"
+
+  archive(byte)    = "parsing.cma"
+  archive(native)  = "parsing.cmxa"
+
+)
+
+package "printing" (
+
+  description = "Coq Printing Engine"
+  version     = "8.9"
+
+  requires    = "coq.parsing"
+  directory   = "printing"
+
+  archive(byte)    = "printing.cma"
+  archive(native)  = "printing.cmxa"
+
+)
+
+package "tactics" (
+
+  description = "Coq Basic Tactics"
+  version     = "8.9"
+
+  requires    = "coq.printing"
+  directory   = "tactics"
+
+  archive(byte)    = "tactics.cma"
+  archive(native)  = "tactics.cmxa"
+
+)
+
+package "vernac" (
+
+  description = "Coq Vernacular Interpreter"
+  version     = "8.9"
+
+  requires    = "coq.tactics"
+  directory   = "vernac"
+
+  archive(byte)    = "vernac.cma"
+  archive(native)  = "vernac.cmxa"
+
+)
+
+package "stm" (
+
+  description = "Coq State Transactional Machine"
+  version     = "8.9"
+
+  requires    = "coq.vernac"
+  directory   = "stm"
+
+  archive(byte)    = "stm.cma"
+  archive(native)  = "stm.cmxa"
+
+)
+
+package "toplevel" (
+
+  description = "Coq Toplevel"
+  version     = "8.9"
+
+  requires    = "coq.stm"
+  directory   = "toplevel"
+
+  archive(byte)    = "toplevel.cma"
+  archive(native)  = "toplevel.cmxa"
+
+)
+
+package "idetop" (
+
+  description = "Coq IDE Libraries"
+  version     = "8.9"
+
+  requires    = "coq.toplevel"
+  directory   = "ide"
+
+  archive(byte)    = "coqidetop.cma"
+  archive(native)  = "coqidetop.cmxa"
+
+)
+
+# XXX Depends on way less than toplevel
+package "ide" (
+
+  description = "Coq IDE Libraries"
+  version     = "8.9"
+
+# XXX Add GTK
+  requires    = "coq.toplevel"
+  directory   = "ide"
+
+  archive(byte)    = "ide.cma"
+  archive(native)  = "ide.cmxa"
+
+)
+
+package "plugins" (
+
+  description = "Coq built-in plugins"
+  version     = "8.9"
+
+  directory   = "plugins"
+
+  package "ltac" (
+
+    description = "Coq LTAC Plugin"
+    version     = "8.9"
+
+    requires    = "coq.stm"
+    directory   = "ltac"
+
+    archive(byte)    = "ltac_plugin.cmo"
+    archive(native)  = "ltac_plugin.cmx"
+
+  )
+
+  package "tauto" (
+
+    description = "Coq tauto plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "ltac"
+
+    archive(byte)    = "tauto_plugin.cmo"
+    archive(native)  = "tauto_plugin.cmx"
+  )
+
+  package "omega" (
+
+    description = "Coq omega plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "omega"
+
+    archive(byte)    = "omega_plugin.cmo"
+    archive(native)  = "omega_plugin.cmx"
+  )
+
+  package "romega" (
+
+    description = "Coq romega plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.omega"
+    directory   = "romega"
+
+    archive(byte)    = "romega_plugin.cmo"
+    archive(native)  = "romega_plugin.cmx"
+  )
+
+  package "micromega" (
+
+    description = "Coq micromega plugin"
+    version     = "8.9"
+
+    requires    = "num,coq.plugins.ltac"
+    directory   = "micromega"
+
+    archive(byte)    = "micromega_plugin.cmo"
+    archive(native)  = "micromega_plugin.cmx"
+  )
+
+  package "quote" (
+
+    description = "Coq quote plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "quote"
+
+    archive(byte)    = "quote_plugin.cmo"
+    archive(native)  = "quote_plugin.cmx"
+  )
+
+  package "newring" (
+
+    description = "Coq newring plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.quote"
+    directory   = "setoid_ring"
+
+    archive(byte)    = "newring_plugin.cmo"
+    archive(native)  = "newring_plugin.cmx"
+  )
+
+  package "fourier" (
+
+    description = "Coq fourier plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "fourier"
+
+    archive(byte)    = "fourier_plugin.cmo"
+    archive(native)  = "fourier_plugin.cmx"
+  )
+
+  package "extraction" (
+
+    description = "Coq extraction plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "extraction"
+
+    archive(byte)    = "extraction_plugin.cmo"
+    archive(native)  = "extraction_plugin.cmx"
+  )
+
+  package "cc" (
+
+    description = "Coq cc plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "cc"
+
+    archive(byte)    = "cc_plugin.cmo"
+    archive(native)  = "cc_plugin.cmx"
+  )
+
+  package "ground" (
+
+    description = "Coq ground plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "firstorder"
+
+    archive(byte)    = "ground_plugin.cmo"
+    archive(native)  = "ground_plugin.cmx"
+  )
+
+  package "rtauto" (
+
+    description = "Coq rtauto plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "rtauto"
+
+    archive(byte)    = "rtauto_plugin.cmo"
+    archive(native)  = "rtauto_plugin.cmx"
+  )
+
+  package "btauto" (
+
+    description = "Coq btauto plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "btauto"
+
+    archive(byte)    = "btauto_plugin.cmo"
+    archive(native)  = "btauto_plugin.cmx"
+  )
+
+  package "recdef" (
+
+    description = "Coq recdef plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.extraction"
+    directory   = "funind"
+
+    archive(byte)    = "recdef_plugin.cmo"
+    archive(native)  = "recdef_plugin.cmx"
+  )
+
+  package "nsatz" (
+
+    description = "Coq nsatz plugin"
+    version     = "8.9"
+
+    requires    = "num,coq.plugins.ltac"
+    directory   = "nsatz"
+
+    archive(byte)    = "nsatz_plugin.cmo"
+    archive(native)  = "nsatz_plugin.cmx"
+  )
+
+  package "natsyntax" (
+
+    description = "Coq natsyntax plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "nat_syntax_plugin.cmo"
+    archive(native)  = "nat_syntax_plugin.cmx"
+  )
+
+  package "zsyntax" (
+
+    description = "Coq zsyntax plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "z_syntax_plugin.cmo"
+    archive(native)  = "z_syntax_plugin.cmx"
+  )
+
+  package "rsyntax" (
+
+    description = "Coq rsyntax plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "r_syntax_plugin.cmo"
+    archive(native)  = "r_syntax_plugin.cmx"
+  )
+
+  package "int31syntax" (
+
+    description = "Coq int31syntax plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "int31_syntax_plugin.cmo"
+    archive(native)  = "int31_syntax_plugin.cmx"
+  )
+
+  package "asciisyntax" (
+
+    description = "Coq asciisyntax plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "ascii_syntax_plugin.cmo"
+    archive(native)  = "ascii_syntax_plugin.cmx"
+  )
+
+  package "stringsyntax" (
+
+    description = "Coq stringsyntax plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.asciisyntax"
+    directory   = "syntax"
+
+    archive(byte)    = "string_syntax_plugin.cmo"
+    archive(native)  = "string_syntax_plugin.cmx"
+  )
+
+  package "derive" (
+
+    description = "Coq derive plugin"
+    version     = "8.9"
+
+    requires    = ""
+    directory   = "derive"
+
+    archive(byte)    = "derive_plugin.cmo"
+    archive(native)  = "derive_plugin.cmx"
+  )
+
+  package "ssrmatching" (
+
+    description = "Coq ssrmatching plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "ssrmatching"
+
+    archive(byte)    = "ssrmatching_plugin.cmo"
+    archive(native)  = "ssrmatching_plugin.cmx"
+  )
+
+  package "ssreflect" (
+
+    description = "Coq ssreflect plugin"
+    version     = "8.9"
+
+    requires    = "coq.plugins.ssrmatching"
+    directory   = "ssr"
+
+    archive(byte)    = "ssreflect_plugin.cmo"
+    archive(native)  = "ssreflect_plugin.cmx"
+  )
+)