1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(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
|
