From 8541a43c053d659196992f4e990ec317cd199af8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 21 Feb 2019 16:45:12 +0000
Subject: [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.
---
 kernel/dune | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel/dune')

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)
-- 
cgit v1.2.3