Quelle  dune

(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