aboutsummaryrefslogtreecommitdiff
path: root/kernel/dune
blob: 1f2d696a3645a308624a153662b17de4d1321784 (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
27
28
29
30
31
(library
 (name kernel)
 (synopsis "The Coq Kernel")
 (public_name coq.kernel)
 (wrapped false)
 (modules (:standard \ uint63_x86 uint63_amd64 write_uint63))
 (libraries lib byterun))

(rule
 (targets copcodes.ml)
 (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh)
 (action (bash "./make_opcodes.sh %{h-file} %{targets}")))

(executable
  (name write_uint63)
  (modules write_uint63)
  (libraries unix))

(rule
 (targets uint63.ml)
 (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml)
 (action (run %{gen})))

(documentation
 (package coq))

; In dev profile, we check the kernel against a more strict set of
; warnings.
(env
 (dev (flags :standard -w +a-4-44-50)))
 ; (ocaml408 (flags :standard -w +a-3-4-44-50)))