summaryrefslogtreecommitdiff
path: root/META.coq.in
diff options
context:
space:
mode:
Diffstat (limited to 'META.coq.in')
-rw-r--r--META.coq.in543
1 files changed, 543 insertions, 0 deletions
diff --git a/META.coq.in b/META.coq.in
new file mode 100644
index 00000000..b2924e32
--- /dev/null
+++ b/META.coq.in
@@ -0,0 +1,543 @@
+# 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 "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"
+ )
+)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 19:06:00 +0000