blob: ac162db78518801a86de66eb1ff626c81c25d36c (
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 CoqList.ml
@mv list.mli CoqList.mli
@mv string.ml CoqString.ml
@mv string.mli CoqString.mli
@mv int.ml CoqInt.ml
@mv int.mli CoqInt.mli
@echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..."
@./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
|
