diff options
Diffstat (limited to 'META.coq')
| -rw-r--r-- | META.coq | 434 |
1 files changed, 378 insertions, 56 deletions
@@ -1,5 +1,7 @@ +# TODO: Generate automatically with Dune + description = "The Coq Proof Assistant Plugin API" -version = "8.6" +version = "8.8" directory = "" requires = "camlp5" @@ -7,61 +9,67 @@ requires = "camlp5" package "config" ( description = "Coq Configuration Variables" - version = "8.6" + version = "8.8" directory = "config" ) +package "clib" ( + description = "Base General Coq Library" + version = "8.8" + + directory = "clib" + requires = "num, str, unix, threads" + + archive(byte) = "clib.cma" + archive(native) = "clib.cmxa" +) + package "lib" ( - description = "Base Coq Library" - version = "8.6" + description = "Base Coq-Specific Library" + version = "8.8" directory = "lib" - requires = "coq.config" - - archive(byte) = "clib.cma" - archive(byte) += "lib.cma" + requires = "coq.clib, coq.config" - archive(native) = "clib.cmxa" - archive(native) += "lib.cmxa" + archive(byte) = "lib.cma" + archive(native) = "lib.cmxa" ) package "vm" ( description = "Coq VM" + version = "8.8" - version = "8.6" + directory = "kernel/byterun" -# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq -# install. In a local one we'll want kernel/byterun, in a non-local -# one we want to set it to coqlib. We should thus generate this file -# at configure time, but let's hear for some more feedback from -# experts. +# 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" -# Enable for local native & byte builds -# directory = "kernel/byterun" +# We currently prefer static linking of the VM. + archive(byte) = "libcoqrun.a" + linkopts(byte) = "-custom" -# Enable for local byte builds and set up properly -# linkopts(byte) = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun" - -# Disable for local byte builds - linkopts(byte) = "-dllib -lcoqrun" linkopts(native) = "-cclib -lcoqrun" ) package "kernel" ( - description = "The Coq's Kernel" - version = "8.6" + description = "Coq's Kernel" + version = "8.8" directory = "kernel" - requires = "coq.lib, coq.vm" + requires = "dynlink, coq.lib, coq.vm" archive(byte) = "kernel.cma" archive(native) = "kernel.cmxa" @@ -71,7 +79,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.6" + version = "8.8" requires = "coq.kernel" @@ -85,18 +93,20 @@ package "library" ( package "intf" ( description = "Coq Public Data Types" - version = "8.6" + version = "8.8" requires = "coq.library" directory = "intf" + archive(byte) = "intf.cma" + archive(native) = "intf.cmxa" ) package "engine" ( - description = "Coq Libraries (vo) support" - version = "8.6" + description = "Coq Tactic Engine" + version = "8.8" requires = "coq.library" directory = "engine" @@ -109,7 +119,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.6" + version = "8.8" requires = "coq.engine" directory = "pretyping" @@ -122,7 +132,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.6" + version = "8.8" requires = "coq.pretyping" directory = "interp" @@ -135,7 +145,7 @@ package "interp" ( package "grammar" ( description = "Coq Base Grammar" - version = "8.6" + version = "8.8" requires = "coq.interp" directory = "grammar" @@ -147,7 +157,7 @@ package "grammar" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.6" + version = "8.8" requires = "coq.interp" directory = "proofs" @@ -160,9 +170,9 @@ package "proofs" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.6" + version = "8.8" - requires = "coq.proofs" + requires = "camlp5.gramlib, coq.proofs" directory = "parsing" archive(byte) = "parsing.cma" @@ -172,8 +182,8 @@ package "parsing" ( package "printing" ( - description = "Coq Printing Libraries" - version = "8.6" + description = "Coq Printing Engine" + version = "8.8" requires = "coq.parsing" directory = "printing" @@ -185,8 +195,8 @@ package "printing" ( package "tactics" ( - description = "Coq Tactics" - version = "8.6" + description = "Coq Basic Tactics" + version = "8.8" requires = "coq.printing" directory = "tactics" @@ -196,12 +206,25 @@ package "tactics" ( ) +package "vernac" ( + + description = "Coq Vernacular Interpreter" + version = "8.8" + + requires = "coq.tactics" + directory = "vernac" + + archive(byte) = "vernac.cma" + archive(native) = "vernac.cmxa" + +) + package "stm" ( description = "Coq State Transactional Machine" - version = "8.6" + version = "8.8" - requires = "coq.tactics" + requires = "coq.vernac" directory = "stm" archive(byte) = "stm.cma" @@ -212,7 +235,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.6" + version = "8.8" requires = "coq.stm" directory = "toplevel" @@ -222,28 +245,327 @@ package "toplevel" ( ) -package "highparsing" ( +package "idetop" ( - description = "Coq Extra Parsing" - version = "8.6" + description = "Coq IDE Libraries" + version = "8.8" requires = "coq.toplevel" - directory = "parsing" + directory = "ide" - archive(byte) = "highparsing.cma" - archive(native) = "highparsing.cmxa" + archive(byte) = "coqidetop.cma" + archive(native) = "coqidetop.cmxa" ) -package "ltac" ( +# XXX Depends on way less than toplevel +package "ide" ( + + description = "Coq IDE Libraries" + version = "8.8" + +# 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.8" + + directory = "plugins" + + package "ltac" ( + + description = "Coq LTAC Plugin" + version = "8.8" + + requires = "coq.stm" + directory = "ltac" + + archive(byte) = "ltac_plugin.cmo" + archive(native) = "ltac_plugin.cmx" + + ) + + package "tauto" ( + + description = "Coq tauto plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "ltac" + + archive(byte) = "tauto_plugin.cmo" + archive(native) = "tauto_plugin.cmx" + ) + + package "omega" ( + + description = "Coq omega plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "omega" + + archive(byte) = "omega_plugin.cmo" + archive(native) = "omega_plugin.cmx" + ) + + package "romega" ( + + description = "Coq romega plugin" + version = "8.8" + + requires = "coq.plugins.omega" + directory = "romega" + + archive(byte) = "romega_plugin.cmo" + archive(native) = "romega_plugin.cmx" + ) + + package "micromega" ( + + description = "Coq micromega plugin" + version = "8.8" + + 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.8" + + requires = "coq.plugins.ltac" + directory = "quote" + + archive(byte) = "quote_plugin.cmo" + archive(native) = "quote_plugin.cmx" + ) + + package "newring" ( + + description = "Coq newring plugin" + version = "8.8" + + 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.8" + + requires = "coq.plugins.ltac" + directory = "fourier" + + archive(byte) = "fourier_plugin.cmo" + archive(native) = "fourier_plugin.cmx" + ) + + package "extraction" ( + + description = "Coq extraction plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "extraction" + + archive(byte) = "extraction_plugin.cmo" + archive(native) = "extraction_plugin.cmx" + ) + + package "cc" ( + + description = "Coq cc plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "cc" + + archive(byte) = "cc_plugin.cmo" + archive(native) = "cc_plugin.cmx" + ) + + package "ground" ( + + description = "Coq ground plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "firstorder" + + archive(byte) = "ground_plugin.cmo" + archive(native) = "ground_plugin.cmx" + ) + + package "rtauto" ( + + description = "Coq rtauto plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "rtauto" + + archive(byte) = "rtauto_plugin.cmo" + archive(native) = "rtauto_plugin.cmx" + ) + + package "btauto" ( + + description = "Coq btauto plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "btauto" + + archive(byte) = "btauto_plugin.cmo" + archive(native) = "btauto_plugin.cmx" + ) + + package "recdef" ( + + description = "Coq recdef plugin" + version = "8.8" + + requires = "coq.plugins.extraction" + directory = "funind" + + archive(byte) = "recdef_plugin.cmo" + archive(native) = "recdef_plugin.cmx" + ) + + package "nsatz" ( + + description = "Coq nsatz plugin" + version = "8.8" + + 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.8" + + requires = "" + directory = "syntax" + + archive(byte) = "nat_syntax_plugin.cmo" + archive(native) = "nat_syntax_plugin.cmx" + ) + + package "zsyntax" ( + + description = "Coq zsyntax plugin" + version = "8.8" + + requires = "" + directory = "syntax" + + archive(byte) = "z_syntax_plugin.cmo" + archive(native) = "z_syntax_plugin.cmx" + ) + + package "rsyntax" ( + + description = "Coq rsyntax plugin" + version = "8.8" + + requires = "" + directory = "syntax" + + archive(byte) = "r_syntax_plugin.cmo" + archive(native) = "r_syntax_plugin.cmx" + ) + + package "int31syntax" ( + + description = "Coq int31syntax plugin" + version = "8.8" + + requires = "" + directory = "syntax" + + archive(byte) = "int31_syntax_plugin.cmo" + archive(native) = "int31_syntax_plugin.cmx" + ) + + package "asciisyntax" ( + + description = "Coq asciisyntax plugin" + version = "8.8" + + requires = "" + directory = "syntax" + + archive(byte) = "ascii_syntax_plugin.cmo" + archive(native) = "ascii_syntax_plugin.cmx" + ) + + package "stringsyntax" ( + + description = "Coq stringsyntax plugin" + version = "8.8" + + 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.8" + + requires = "" + directory = "derive" + + archive(byte) = "derive_plugin.cmo" + archive(native) = "derive_plugin.cmx" + ) + + package "ssrmatching" ( + + description = "Coq ssrmatching plugin" + version = "8.8" + + requires = "coq.plugins.ltac" + directory = "ssrmatching" + + archive(byte) = "ssrmatching_plugin.cmo" + archive(native) = "ssrmatching_plugin.cmx" + ) - description = "Coq LTAC Plugin" - version = "8.6" + package "ssreflect" ( - requires = "coq.highparsing" - directory = "ltac" + description = "Coq ssreflect plugin" + version = "8.8" - archive(byte) = "ltac.cma" - archive(native) = "ltac.cmxa" + requires = "coq.plugins.ssrmatching" + directory = "ssr" + archive(byte) = "ssreflect_plugin.cmo" + archive(native) = "ssreflect_plugin.cmx" + ) ) |