META.coq.in

# TODO: Generate automatically with Dune

description = "The Coq Proof Assistant Plugin API"
version = "8.12"

directory = ""
requires = ""

package "config" (

  description = "Coq Configuration Variables"
  version     = "8.12"

  directory   = "config"

  archive(byte)    = "config.cma"
  archive(native)  = "config.cmxa"
)

package "clib" (
  description = "Base General Coq Library"
  version     = "8.12"

  directory   = "clib"
  requires    = "str, unix, threads"

  archive(byte)    = "clib.cma"
  archive(native)  = "clib.cmxa"
)

package "lib" (

  description = "Base Coq-Specific Library"
  version     = "8.12"

  directory   = "lib"

  requires    = "coq.clib, coq.config, dynlink"

  archive(byte)   = "lib.cma"
  archive(native) = "lib.cmxa"

)

package "vm" (

  description = "Coq VM"
  version     = "8.12"

  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.12"

  directory   = "kernel"

  requires    = "coq.lib, coq.vm"

  archive(byte)    = "kernel.cma"
  archive(native)  = "kernel.cmxa"

)

package "library" (

  description = "Coq Libraries (vo) support"
  version     = "8.12"

  requires    = "coq.kernel"

  directory   = "library"

  archive(byte)    = "library.cma"
  archive(native)  = "library.cmxa"

)

package "engine" (

  description = "Coq Tactic Engine"
  version     = "8.12"

  requires    = "coq.library"
  directory   = "engine"

  archive(byte)    = "engine.cma"
  archive(native)  = "engine.cmxa"

)

package "pretyping" (

  description = "Coq Pretyper"
  version     = "8.12"

  requires    = "coq.engine"
  directory   = "pretyping"

  archive(byte)    = "pretyping.cma"
  archive(native)  = "pretyping.cmxa"

)

package "interp" (

  description = "Coq Term Interpretation"
  version     = "8.12"

  requires    = "coq.pretyping"
  directory   = "interp"

  archive(byte)    = "interp.cma"
  archive(native)  = "interp.cmxa"

)

package "proofs" (

  description = "Coq Proof Engine"
  version     = "8.12"

  requires    = "coq.interp"
  directory   = "proofs"

  archive(byte)    = "proofs.cma"
  archive(native)  = "proofs.cmxa"

)

package "gramlib" (

  description = "Coq Grammar Engine"
  version     = "8.12"

  requires    = "coq.lib"
  directory   = "gramlib/.pack"

  archive(byte)    = "gramlib.cma"
  archive(native)  = "gramlib.cmxa"
)

package "parsing" (

  description = "Coq Parsing Engine"
  version     = "8.12"

  requires    = "coq.gramlib, coq.proofs"
  directory   = "parsing"

  archive(byte)    = "parsing.cma"
  archive(native)  = "parsing.cmxa"

)

package "printing" (

  description = "Coq Printing Engine"
  version     = "8.12"

  requires    = "coq.parsing"
  directory   = "printing"

  archive(byte)    = "printing.cma"
  archive(native)  = "printing.cmxa"

)

package "tactics" (

  description = "Coq Basic Tactics"
  version     = "8.12"

  requires    = "coq.printing"
  directory   = "tactics"

  archive(byte)    = "tactics.cma"
  archive(native)  = "tactics.cmxa"

)

package "vernac" (

  description = "Coq Vernacular Interpreter"
  version     = "8.12"

  requires    = "coq.tactics"
  directory   = "vernac"

  archive(byte)    = "vernac.cma"
  archive(native)  = "vernac.cmxa"

)

package "stm" (

  description = "Coq State Transactional Machine"
  version     = "8.12"

  requires    = "coq.vernac"
  directory   = "stm"

  archive(byte)    = "stm.cma"
  archive(native)  = "stm.cmxa"

)

package "toplevel" (

  description = "Coq Toplevel"
  version     = "8.12"

  requires    = "num, coq.stm"
  directory   = "toplevel"

  archive(byte)    = "toplevel.cma"
  archive(native)  = "toplevel.cmxa"

)

package "idetop" (

  description = "Coq IDE Libraries"
  version     = "8.12"

  requires    = "coq.toplevel"
  directory   = "ide"

  archive(byte)    = "coqidetop.cma"
  archive(native)  = "coqidetop.cmxa"

)

package "ide" (

  description = "Coq IDE Libraries"
  version     = "8.12"

  requires    = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3"
  directory   = "ide"

  archive(byte)    = "ide.cma"
  archive(native)  = "ide.cmxa"

)

package "ideprotocol" (

  description = "Coq IDE protocol"
  version     = "8.12"

  requires    = "coq.toplevel"
  directory   = "ide/protocol"

  archive(byte)    = "ideprotocol.cma"
  archive(native)  = "ideprotocol.cmxa"

)

package "plugins" (

  description = "Coq built-in plugins"
  version     = "8.12"

  directory   = "plugins"

  package "ltac" (

    description = "Coq LTAC Plugin"
    version     = "8.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "num,coq.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.12"

    requires    = "coq.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 "setoid_ring" (

    description = "Coq newring plugin"
    version     = "8.12"

    requires    = ""
    directory   = "setoid_ring"

    archive(byte)    = "newring_plugin.cmo"
    archive(native)  = "newring_plugin.cmx"

    plugin(byte)    = "newring_plugin.cmo"
    plugin(native)  = "newring_plugin.cmxs"
  )

  package "extraction" (

    description = "Coq extraction plugin"
    version     = "8.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "num,coq.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.12"

    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 "int63syntax" (

    description = "Coq int63syntax plugin"
    version     = "8.12"

    requires    = ""
    directory   = "syntax"

    archive(byte)    = "int63_syntax_plugin.cmo"
    archive(native)  = "int63_syntax_plugin.cmx"

    plugin(byte)    = "int63_syntax_plugin.cmo"
    plugin(native)  = "int63_syntax_plugin.cmxs"
  )

  package "string_notation" (

    description = "Coq string_notation plugin"
    version     = "8.12"

    requires    = ""
    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 "derive" (

    description = "Coq derive plugin"
    version     = "8.12"

    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.12"

    requires    = "coq.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.12"

    requires    = "coq.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.12"

    requires    = "coq.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"
  )
)