Quelle META.rocq-plugin-tutorial Sprache: unbekannt

# Comments in META start with # and end with newline

# our plugin is called rocq-plugin-tutorial.tuto1
# rocq-plugin-tutorial from the META filename
# tuto1 from this "package" name
package "tuto1" (
    # the plugin files are in "src"
    directory = "src"

    version = "dev"
    description = "A tuto1 plugin"

    # we define ltac1 tactics so we depend on ltac
    # otherwise we would depend only on rocq-runtime.vernac
    # (it contains the APIs for declaring new commands)
    # (ltac depends on vernac so if we depend on ltac, vernac is also implicitly depended on)
    requires = "rocq-runtime.plugins.ltac"

    # the compiled plugin files (rocq makefile bases these filenames on the .mlpack filename)
    # (only the "plugin" keys are used by rocq,
    # "archive" is for packages which depend on this package)
    archive(byte) = "tuto1_plugin.cma"
    archive(native) = "tuto1_plugin.cmxa"
    plugin(byte) = "tuto1_plugin.cma"
    plugin(native) = "tuto1_plugin.cmxs"
)

# paths in this file are relative to this directory
directory = "."

Quelle META.rocq-plugin-tutorial Sprache: unbekannt

[ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ]