Quelle dune Sprache: HTML

(library
(name dev)
(public_name rocq-runtime.dev)
(synopsis "Rocq's Debug Printers")
(wrapped false)
(modules top_printers vm_printers)
; NB currently we have no "install_printer" using ltac2,
; but we still want to load_printer ltac2
; so that its genarg printers are present in the debugger's printer process
(libraries rocq-runtime.vernac rocq-runtime.plugins.ltac rocq-runtime.plugins.ltac2))

(library
(name debugger_support)
(public_name rocq-runtime.debugger_support)
(synopsis "Rocq Support for ocamldebug")
(wrapped false)
(modules debugger_support)
(libraries rocq-runtime.dev))

(rule
  (targets dune-dbg)
  (deps
    dune-dbg.in
    ../checker/coqchk.bc
    ../topbin/rocqworker.bc
    ../topbin/rocqnative.bc
    ; We require all the OCaml libs to be in place and searchable
    ; by OCamlfind, this is a bit of a hack but until Dune gets
    ; proper ocamldebug support we have to live with that.
    %{lib:rocq-runtime.config:config.cma}
    %{lib:rocq-runtime.clib:clib.cma}
    %{lib:rocq-runtime.lib:lib.cma}
    %{lib:rocq-runtime.kernel:kernel.cma}
    %{lib:rocq-runtime.vm:coqrun.cma}
    %{lib:rocq-runtime.vm:../../stublibs/dllcoqrun_stubs.so}
    %{lib:rocq-runtime.library:library.cma}
    %{lib:rocq-runtime.engine:engine.cma}
    %{lib:rocq-runtime.pretyping:pretyping.cma}
    %{lib:rocq-runtime.gramlib:gramlib.cma}
    %{lib:rocq-runtime.interp:interp.cma}
    %{lib:rocq-runtime.proofs:proofs.cma}
    %{lib:rocq-runtime.parsing:parsing.cma}
    %{lib:rocq-runtime.printing:printing.cma}
    %{lib:rocq-runtime.tactics:tactics.cma}
    %{lib:rocq-runtime.vernac:vernac.cma}
    %{lib:rocq-runtime.plugins.ltac:ltac_plugin.cma}
    %{lib:rocq-runtime.plugins.ltac2:ltac2_plugin.cma}
    %{lib:rocq-runtime.dev:dev.cma}
    %{lib:rocq-runtime.debugger_support:debugger_support.cmi}
    %{lib:rocq-runtime.debugger_support:debugger_support.cma}
    %{lib:rocq-runtime.debugger_support:../META})
  (action (copy dune-dbg.in dune-dbg)))

(alias
(name ml_toplevel_files)
(deps (glob_files ml_toplevel/**)))

(install
(section lib)
(package rocq-runtime)
(files
  (ml_toplevel/include as dev/ml_toplevel/include)
  (ml_toplevel/include_directories as dev/ml_toplevel/include_directories)
  (ml_toplevel/include_printers as dev/ml_toplevel/include_printers)
  (ml_toplevel/include_utilities as dev/ml_toplevel/include_utilities)))
; TODO: the above can be written as follow:
;         (files (glob_files (ml_toplevel/** with_prefix dev)))
;       , but this is only possible with dune language 3.11 or later

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.