diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 8 insertions, 4 deletions
@@ -16,18 +16,20 @@ include Makefile.config ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) +ARCHDIRS?=$(ARCH) else -ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +ARCHDIRS?=$(ARCH)_$(BITSIZE) $(ARCH) endif +BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v + DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/MenhirLib RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser -COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d))) COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) @@ -95,7 +97,8 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v + Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ + $(BACKENDLIB) # C front-end modules (in cfrontend/) @@ -137,6 +140,7 @@ all: $(MAKE) proof $(MAKE) extraction $(MAKE) ccomp + $(MAKE) ccomp.byte ifeq ($(HAS_RUNTIME_LIB),true) $(MAKE) runtime endif |