blob: d4163bb3b767f91bc32f74bbf82d5e20f3e4d142 (
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
#######################################################################
# #
# The Compcert verified compiler #
# #
# Xavier Leroy, INRIA Paris-Rocquencourt #
# #
# Copyright Institut National de Recherche en Informatique et en #
# Automatique. All rights reserved. This file is distributed #
# under the terms of the INRIA Non-Commercial License Agreement. #
# #
#######################################################################
include ../Makefile.config
DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver
COQINCL=$(patsubst %,-I ../%,$(DIRS))
COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source
all: Configuration.ml extraction
extraction:
rm -f [:lower:]*.mli [:lower:]*.ml
$(COQEXEC) extraction.v
@echo "Fixing file names..."
@mv list.ml CList.ml
@mv list.mli CList.mli
@mv string.ml CString.ml
@mv string.mli CString.mli
@mv int.ml CInt.ml
@mv int.mli CInt.mli
@echo "Conversion List -> CList, String -> CString, Int -> CInt..."
@./convert *.mli *.ml
@echo "Patching files..."
@for i in *.patch; do patch < $$i; done
Configuration.ml: ../Makefile.config
(echo 'let stdlib_path = "$(LIBDIR)"'; \
echo 'let prepro = "$(CPREPRO)"'; \
echo 'let asm = "$(CASM)"'; \
echo 'let linker = "$(CLINKER)"'; \
echo 'let arch = "$(ARCH)"'; \
echo 'let variant = "$(VARIANT)"') \
> Configuration.ml
clean:
rm -f *.mli *.ml
|
