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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
;
; Shims for running coq binaries with minimal dependencies
;
; coqtop
(alias
(name coqtop-prelude)
(deps
%{bin:coqtop}
; XXX: bug, we are missing the dep on the _install meta file...
%{project_root}/theories/Init/Prelude.vo))
(rule
(targets coqtop)
(deps (alias coqtop-prelude))
(action
(with-stdout-to %{targets}
(progn
(echo "#!/bin/bash\n")
(bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
(run chmod +x %{targets})))))
; coqc
(alias
(name coqc-prelude)
(deps
%{bin:coqc}
%{bin:coqworker.opt}
%{project_root}/theories/Init/Prelude.vo))
(rule
(targets coqc)
(deps (alias coqc-prelude))
(action
(with-stdout-to %{targets}
(progn
(echo "#!/bin/bash\n")
(bash "echo '\"$(dirname \"$0\")\"/%{bin:coqc} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} -nI \"$(dirname \"$0\")\"/%{project_root}/kernel/.kernel.objs/byte \"$@\"'")
(run chmod +x %{targets})))))
; coqtop.byte
(alias
(name coqtop.byte-prelude)
(deps
%{project_root}/theories/Init/Prelude.vo
%{bin:coqtop.byte}
%{lib:coq-core.config:config.cma}
%{lib:coq-core.clib:clib.cma}
%{lib:coq-core.lib:lib.cma}
%{lib:coq-core.kernel:kernel.cma}
%{lib:coq-core.vm:coqrun.cma}
%{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so}
%{lib:coq-core.library:library.cma}
%{lib:coq-core.engine:engine.cma}
%{lib:coq-core.pretyping:pretyping.cma}
%{lib:coq-core.gramlib:gramlib.cma}
%{lib:coq-core.interp:interp.cma}
%{lib:coq-core.proofs:proofs.cma}
%{lib:coq-core.parsing:parsing.cma}
%{lib:coq-core.printing:printing.cma}
%{lib:coq-core.tactics:tactics.cma}
%{lib:coq-core.vernac:vernac.cma}
%{lib:coq-core.stm:stm.cma}
%{lib:coq-core.sysinit:sysinit.cma}
%{lib:coq-core.toplevel:toplevel.cma}
%{lib:coq-core.plugins.number_string_notation:number_string_notation_plugin.cma}
%{lib:coq-core.plugins.tauto:tauto_plugin.cma}
%{lib:coq-core.plugins.cc:cc_plugin.cma}
%{lib:coq-core.plugins.firstorder:firstorder_plugin.cma}
%{lib:coq-core.plugins.ltac:ltac_plugin.cma}
(alias %{project_root}/dev/ml_toplevel_files)))
(rule
(targets coqtop.byte)
(deps (alias coqtop.byte-prelude))
(action
(with-stdout-to %{targets}
(progn
(echo "#!/bin/bash\n")
(bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
(run chmod +x %{targets})))))
; coqide
(alias
(name coqide-prelude)
(deps
; without this if the gtk libs are not available dune can try to use
; coqide from PATH instead of giving a nice error
; there is no problem with the other shims since they don't depend on optional build products
%{project_root}/ide/coqide/coqide_main.exe
%{bin:coqworker.opt}
%{project_root}/theories/Init/Prelude.vo
%{project_root}/coqide-server.install
%{project_root}/coqide.install))
(rule
(targets coqide)
(deps (alias coqide-prelude))
(action
(with-stdout-to %{targets}
(progn
(echo "#!/bin/bash\n")
(bash "echo '\"$(dirname \"$0\")\"/%{bin:coqide} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'")
(run chmod +x %{targets})))))
|
