summaryrefslogtreecommitdiff
path: root/extraction/Makefile
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