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 /Makefile.build | |
| 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 'Makefile.build')
| -rw-r--r-- | Makefile.build | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index ea356d5f8e..e348b2b9b8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -316,11 +316,21 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh - kernel/byterun/make_jumptbl.sh $< $@ +kernel/genOpcodeFiles.exe: kernel/genOpcodeFiles.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -o $@ $< + +kernel/byterun/coq_instruct.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< enum > $@ -kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes - kernel/make_opcodes.sh $< $@ +kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< jump > $@ + +kernel/copcodes.ml: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< copml > $@ %.o: %.c $(SHOW)'OCAMLC $<' |