diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-01 12:37:36 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-01 12:37:36 +0000 |
| commit | d18371174552ed29069a34d81d60530df431ac0f (patch) | |
| tree | 91a8d71e3b428f02e2fdbf76977f3a750204fc22 /Makefile | |
| parent | 3a2533890c9c275c38d620f4bcfa4aa76eab19a6 (diff) | |
Use "-as" to put CompCert modules in a compcert.xxx namespace.
Simplified the scripts "coq" and "pg".
Updated deps.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 23 |
1 files changed, 16 insertions, 7 deletions
@@ -13,22 +13,28 @@ include Makefile.config DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/Appli + flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight -INCLUDES=$(patsubst %,-I %, $(DIRS)) +RECDIRS=lib common backend cfrontend driver flocq exportclight -COQC=coqc -q $(INCLUDES) -COQDEP=coqdep $(INCLUDES) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) \ + -I $(ARCH)/$(VARIANT) -as compcert.$(ARCH).$(VARIANT) \ + -I $(ARCH) -as compcert.$(ARCH) + +CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction -I cparser + +COQC=coqc -q $(COQINCLUDES) +COQDEP=coqdep $(COQINCLUDES) COQDOC=coqdoc -COQEXEC=coqtop $(INCLUDES) -batch -load-vernac-source -COQCHK=coqchk $(INCLUDES) +COQEXEC=coqtop $(COQINCLUDES) -batch -load-vernac-source +COQCHK=coqchk $(COQINCLUDES) OCAMLBUILD=ocamlbuild OCB_OPTIONS=\ -j 2 \ -no-hygiene \ -no-links \ - -I extraction -I cparser $(INCLUDES) + $(CAMLINCLUDES) OCB_OPTIONS_CHECKLINK=\ $(OCB_OPTIONS) \ -I checklink \ @@ -251,6 +257,9 @@ check-admitted: $(FILES) check-proof: $(FILES) $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements +print-includes: + @echo $(COQINCLUDES) + include .depend FORCE: |