diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 22 |
1 files changed, 11 insertions, 11 deletions
@@ -23,9 +23,10 @@ endif DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ - exportclight cparser cparser/MenhirLib + exportclight MenhirLib cparser -RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser +RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ + MenhirLib cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) @@ -103,16 +104,16 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v -# LR(1) parser validator - -PARSERVALIDATOR=Alphabet.v Interpreter_complete.v Interpreter.v \ - Validator_complete.v Automaton.v Interpreter_correct.v Main.v \ - Validator_safe.v Grammar.v Interpreter_safe.v Tuples.v - # Parser PARSER=Cabs.v Parser.v +# MenhirLib + +MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \ + Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \ + Validator_safe.v Validator_classes.v + # Putting everything together (in driver/) DRIVER=Compopts.v Compiler.v Complements.v @@ -120,7 +121,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ - $(PARSERVALIDATOR) $(PARSER) + $(MENHIRLIB) $(PARSER) # Generated source files @@ -141,7 +142,6 @@ ifeq ($(CLIGHTGEN),true) $(MAKE) clightgen endif - proof: $(FILES:.v=.vo) # Turn off some warnings for compiling Flocq @@ -225,7 +225,7 @@ driver/Version.ml: VERSION cparser/Parser.v: cparser/Parser.vy @rm -f $@ - $(MENHIR) $(MENHIR_FLAGS) --coq cparser/Parser.vy + $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy @chmod a-w $@ depend: $(GENERATED) depend1 |