aboutsummaryrefslogtreecommitdiff
path: root/META.coq-core.in
diff options
context:
space:
mode:
Diffstat (limited to 'META.coq-core.in')
-rw-r--r--META.coq-core.in591
1 files changed, 591 insertions, 0 deletions
diff --git a/META.coq-core.in b/META.coq-core.in
new file mode 100644
index 0000000000..c58513979d
--- /dev/null
+++ b/META.coq-core.in
@@ -0,0 +1,591 @@
+# TODO: Generate automatically with Dune
+
+description = "The Coq Proof Assistant Plugin API"
+version = "8.14"
+
+directory = ""
+requires = ""
+
+package "config" (
+
+ description = "Coq Configuration Variables"
+ version = "8.14"
+
+ directory = "config"
+
+ archive(byte) = "config.cma"
+ archive(native) = "config.cmxa"
+)
+
+package "clib" (
+ description = "Base General Coq Library"
+ version = "8.14"
+
+ directory = "clib"
+ requires = "str, unix, threads"
+
+ archive(byte) = "clib.cma"
+ archive(native) = "clib.cmxa"
+)
+
+package "lib" (
+
+ description = "Base Coq-Specific Library"
+ version = "8.14"
+
+ directory = "lib"
+
+ requires = "coq-core.clib, coq-core.config, dynlink"
+
+ archive(byte) = "lib.cma"
+ archive(native) = "lib.cmxa"
+
+)
+
+package "vm" (
+
+ description = "Coq VM"
+ version = "8.14"
+
+ 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.14"
+
+ directory = "kernel"
+
+ requires = "coq-core.lib, coq-core.vm"
+
+ archive(byte) = "kernel.cma"
+ archive(native) = "kernel.cmxa"
+
+)
+
+package "library" (
+
+ description = "Coq Libraries (vo) support"
+ version = "8.14"
+
+ requires = "coq-core.kernel"
+
+ directory = "library"
+
+ archive(byte) = "library.cma"
+ archive(native) = "library.cmxa"
+
+)
+
+package "engine" (
+
+ description = "Coq Tactic Engine"
+ version = "8.14"
+
+ requires = "coq-core.library"
+ directory = "engine"
+
+ archive(byte) = "engine.cma"
+ archive(native) = "engine.cmxa"
+
+)
+
+package "pretyping" (
+
+ description = "Coq Pretyper"
+ version = "8.14"
+
+ requires = "coq-core.engine"
+ directory = "pretyping"
+
+ archive(byte) = "pretyping.cma"
+ archive(native) = "pretyping.cmxa"
+
+)
+
+package "interp" (
+
+ description = "Coq Term Interpretation"
+ version = "8.14"
+
+ requires = "zarith, coq-core.pretyping"
+ directory = "interp"
+
+ archive(byte) = "interp.cma"
+ archive(native) = "interp.cmxa"
+
+)
+
+package "proofs" (
+
+ description = "Coq Proof Engine"
+ version = "8.14"
+
+ requires = "coq-core.interp"
+ directory = "proofs"
+
+ archive(byte) = "proofs.cma"
+ archive(native) = "proofs.cmxa"
+
+)
+
+package "gramlib" (
+
+ description = "Coq Grammar Engine"
+ version = "8.14"
+
+ requires = "coq-core.lib"
+ directory = "gramlib/.pack"
+
+ archive(byte) = "gramlib.cma"
+ archive(native) = "gramlib.cmxa"
+)
+
+package "parsing" (
+
+ description = "Coq Parsing Engine"
+ version = "8.14"
+
+ requires = "coq-core.gramlib, coq-core.proofs"
+ directory = "parsing"
+
+ archive(byte) = "parsing.cma"
+ archive(native) = "parsing.cmxa"
+
+)
+
+package "printing" (
+
+ description = "Coq Printing Engine"
+ version = "8.14"
+
+ requires = "coq-core.parsing"
+ directory = "printing"
+
+ archive(byte) = "printing.cma"
+ archive(native) = "printing.cmxa"
+
+)
+
+package "tactics" (
+
+ description = "Coq Basic Tactics"
+ version = "8.14"
+
+ requires = "coq-core.printing"
+ directory = "tactics"
+
+ archive(byte) = "tactics.cma"
+ archive(native) = "tactics.cmxa"
+
+)
+
+package "vernac" (
+
+ description = "Coq Vernacular Interpreter"
+ version = "8.14"
+
+ requires = "coq-core.tactics"
+ directory = "vernac"
+
+ archive(byte) = "vernac.cma"
+ archive(native) = "vernac.cmxa"
+
+)
+
+package "stm" (
+
+ description = "Coq State Transaction Machine"
+ version = "8.14"
+
+ requires = "coq-core.sysinit"
+ directory = "stm"
+
+ archive(byte) = "stm.cma"
+ archive(native) = "stm.cmxa"
+
+)
+
+package "sysinit" (
+
+ description = "Coq initialization"
+ version = "8.14"
+
+ requires = "coq-core.vernac"
+ directory = "sysinit"
+
+ archive(byte) = "sysinit.cma"
+ archive(native) = "sysinit.cmxa"
+
+)
+
+package "toplevel" (
+
+ description = "Coq Toplevel"
+ version = "8.14"
+
+ requires = "coq-core.stm"
+ directory = "toplevel"
+
+ archive(byte) = "toplevel.cma"
+ archive(native) = "toplevel.cmxa"
+
+)
+
+package "idetop" (
+
+ description = "Coq IDE Libraries"
+ version = "8.14"
+
+ requires = "coq-core.toplevel"
+ directory = "ide"
+
+ archive(byte) = "coqidetop.cma"
+ archive(native) = "coqidetop.cmxa"
+
+)
+
+package "ide" (
+
+ description = "Coq IDE Libraries"
+ version = "8.14"
+
+ requires = "coq-core.lib, coq-core.ideprotocol, lablgtk3, lablgtk3-sourceview3"
+ directory = "ide"
+
+ archive(byte) = "ide.cma"
+ archive(native) = "ide.cmxa"
+
+)
+
+package "ideprotocol" (
+
+ description = "Coq IDE protocol"
+ version = "8.14"
+
+ requires = "coq-core.toplevel"
+ directory = "ide/protocol"
+
+ archive(byte) = "ideprotocol.cma"
+ archive(native) = "ideprotocol.cmxa"
+
+)
+
+package "plugins" (
+
+ description = "Coq built-in plugins"
+ version = "8.14"
+
+ directory = "plugins"
+
+ package "ltac" (
+
+ description = "Coq LTAC Plugin"
+ version = "8.14"
+
+ requires = "coq-core.stm"
+ directory = "ltac"
+
+ archive(byte) = "ltac_plugin.cmo"
+ archive(native) = "ltac_plugin.cmx"
+
+ plugin(byte) = "ltac_plugin.cmo"
+ plugin(native) = "ltac_plugin.cmxs"
+ )
+
+ package "tauto" (
+
+ description = "Coq tauto plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "ltac"
+
+ archive(byte) = "tauto_plugin.cmo"
+ archive(native) = "tauto_plugin.cmx"
+
+ plugin(byte) = "tauto_plugin.cmo"
+ plugin(native) = "tauto_plugin.cmxs"
+ )
+
+ package "omega" (
+
+ description = "Coq omega plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "omega"
+
+ archive(byte) = "omega_plugin.cmo"
+ archive(native) = "omega_plugin.cmx"
+
+ plugin(byte) = "omega_plugin.cmo"
+ plugin(native) = "omega_plugin.cmxs"
+ )
+
+ package "micromega" (
+
+ description = "Coq micromega plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "micromega"
+
+ archive(byte) = "micromega_plugin.cmo"
+ archive(native) = "micromega_plugin.cmx"
+
+ plugin(byte) = "micromega_plugin.cmo"
+ plugin(native) = "micromega_plugin.cmxs"
+ )
+
+ package "zify" (
+
+ description = "Coq Zify plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "micromega"
+
+ archive(byte) = "zify_plugin.cmo"
+ archive(native) = "zify_plugin.cmx"
+
+ plugin(byte) = "zify_plugin.cmo"
+ plugin(native) = "zify_plugin.cmxs"
+ )
+
+ package "ring" (
+
+ description = "Coq ring plugin"
+ version = "8.14"
+
+ requires = ""
+ directory = "ring"
+
+ archive(byte) = "ring_plugin.cmo"
+ archive(native) = "ring_plugin.cmx"
+
+ plugin(byte) = "ring_plugin.cmo"
+ plugin(native) = "ring_plugin.cmxs"
+ )
+
+ package "extraction" (
+
+ description = "Coq extraction plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "extraction"
+
+ archive(byte) = "extraction_plugin.cmo"
+ archive(native) = "extraction_plugin.cmx"
+
+ plugin(byte) = "extraction_plugin.cmo"
+ plugin(native) = "extraction_plugin.cmxs"
+ )
+
+ package "cc" (
+
+ description = "Coq cc plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "cc"
+
+ archive(byte) = "cc_plugin.cmo"
+ archive(native) = "cc_plugin.cmx"
+
+ plugin(byte) = "cc_plugin.cmo"
+ plugin(native) = "cc_plugin.cmxs"
+ )
+
+ package "firstorder" (
+
+ description = "Coq ground plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "firstorder"
+
+ archive(byte) = "ground_plugin.cmo"
+ archive(native) = "ground_plugin.cmx"
+
+ plugin(byte) = "ground_plugin.cmo"
+ plugin(native) = "ground_plugin.cmxs"
+ )
+
+ package "rtauto" (
+
+ description = "Coq rtauto plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "rtauto"
+
+ archive(byte) = "rtauto_plugin.cmo"
+ archive(native) = "rtauto_plugin.cmx"
+
+ plugin(byte) = "rtauto_plugin.cmo"
+ plugin(native) = "rtauto_plugin.cmxs"
+ )
+
+ package "btauto" (
+
+ description = "Coq btauto plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "btauto"
+
+ archive(byte) = "btauto_plugin.cmo"
+ archive(native) = "btauto_plugin.cmx"
+
+ plugin(byte) = "btauto_plugin.cmo"
+ plugin(native) = "btauto_plugin.cmxs"
+ )
+
+ package "funind" (
+
+ description = "Coq recdef plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.extraction"
+ directory = "funind"
+
+ archive(byte) = "recdef_plugin.cmo"
+ archive(native) = "recdef_plugin.cmx"
+
+ plugin(byte) = "recdef_plugin.cmo"
+ plugin(native) = "recdef_plugin.cmxs"
+ )
+
+ package "nsatz" (
+
+ description = "Coq nsatz plugin"
+ version = "8.14"
+
+ requires = "zarith, coq-core.plugins.ltac"
+ directory = "nsatz"
+
+ archive(byte) = "nsatz_plugin.cmo"
+ archive(native) = "nsatz_plugin.cmx"
+
+ plugin(byte) = "nsatz_plugin.cmo"
+ plugin(native) = "nsatz_plugin.cmxs"
+ )
+
+ package "rsyntax" (
+
+ description = "Coq rsyntax plugin"
+ version = "8.14"
+
+ requires = ""
+ directory = "syntax"
+
+ archive(byte) = "r_syntax_plugin.cmo"
+ archive(native) = "r_syntax_plugin.cmx"
+
+ plugin(byte) = "r_syntax_plugin.cmo"
+ plugin(native) = "r_syntax_plugin.cmxs"
+ )
+
+ package "string_notation" (
+
+ description = "Coq string_notation plugin"
+ version = "8.14"
+
+ requires = "coq-core.vernac"
+ directory = "syntax"
+
+ archive(byte) = "string_notation_plugin.cmo"
+ archive(native) = "string_notation_plugin.cmx"
+
+ plugin(byte) = "string_notation_plugin.cmo"
+ plugin(native) = "string_notation_plugin.cmxs"
+ )
+
+ package "numeral_notation" (
+ description = "Coq numeral notation plugin"
+ version = "8.14"
+
+ requires = "coq-core.vernac"
+ directory = "numeral_notation"
+
+ archive(byte) = "numeral_notation_plugin.cmo"
+ archive(native) = "numeral_notation_plugin.cmx"
+
+ plugin(byte) = "numeral_notation_plugin.cmo"
+ plugin(native) = "numeral_notation_plugin.cmxs"
+ )
+
+ package "derive" (
+
+ description = "Coq derive plugin"
+ version = "8.14"
+
+ requires = ""
+ directory = "derive"
+
+ archive(byte) = "derive_plugin.cmo"
+ archive(native) = "derive_plugin.cmx"
+
+ plugin(byte) = "derive_plugin.cmo"
+ plugin(native) = "derive_plugin.cmxs"
+ )
+
+ package "ssrmatching" (
+
+ description = "Coq ssrmatching plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "ssrmatching"
+
+ archive(byte) = "ssrmatching_plugin.cmo"
+ archive(native) = "ssrmatching_plugin.cmx"
+
+ plugin(byte) = "ssrmatching_plugin.cmo"
+ plugin(native) = "ssrmatching_plugin.cmxs"
+ )
+
+ package "ssreflect" (
+
+ description = "Coq ssreflect plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ssrmatching"
+ directory = "ssr"
+
+ archive(byte) = "ssreflect_plugin.cmo"
+ archive(native) = "ssreflect_plugin.cmx"
+
+ plugin(byte) = "ssreflect_plugin.cmo"
+ plugin(native) = "ssreflect_plugin.cmxs"
+ )
+
+ package "ltac2" (
+
+ description = "Coq Ltac2 Plugin"
+ version = "8.14"
+
+ requires = "coq-core.plugins.ltac"
+ directory = "../user-contrib/Ltac2"
+
+ archive(byte) = "ltac2_plugin.cmo"
+ archive(native) = "ltac2_plugin.cmx"
+
+ plugin(byte) = "ltac2_plugin.cmo"
+ plugin(native) = "ltac2_plugin.cmxs"
+ )
+)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:58:21 +0000