diff options
| author | Vincent Laporte | 2019-02-21 16:45:12 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-01 14:01:23 +0000 |
| commit | 8541a43c053d659196992f4e990ec317cd199af8 (patch) | |
| tree | 6ea182cefc82d7a2d8edeaad6d61a152b85b4121 /kernel/dune | |
| parent | 9e858cae7d40459142409e793133eb939a0ffc47 (diff) | |
[Kernel] Simpler generation of opcode files
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/dune b/kernel/dune index 1f2d696a36..a8a87a3e95 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,13 +3,16 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) +(executable + (name genOpcodeFiles) + (modules genOpcodeFiles)) + (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) - (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (executable (name write_uint63) |