blob: d0145176ead68d280d73ec70d9954604f10f3b63 (
plain)
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
|
; Dune doesn't use configure's output, but it is still necessary for
; some Coq files to work; will be fixed in the future.
(rule
(targets dune.c_flags)
(mode fallback)
(deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
(action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
(env
(dev (c_flags (:include dune.c_flags)))
(release (c_flags (:include dune.c_flags)))
(ireport (c_flags (:include dune.c_flags))))
(library
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq.vm)
(c_names coq_fix_code coq_memory coq_values coq_interp))
(rule
(targets coq_instruct.h)
(action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))
(rule
(targets coq_jumptbl.h)
(action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
|
