diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:24:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:24:26 +0000 |
| commit | aad98c46631f3acb3c71ff7a7f6ae9887627baa8 (patch) | |
| tree | 8a08ec5262a77b38766f04ff26841bfc8e334465 | |
| parent | d1cd53c161f8534a6756b92ca3072155b726f531 (diff) | |
Option -v8 à coqtop lance coqtopnew
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4256 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 24 |
1 files changed, 10 insertions, 14 deletions
@@ -1274,11 +1274,7 @@ devel: # 1. Translate the old syntax files and build new syntax theories hierarchy translation:: - @$(MAKE) COQ_XML=-ftranslate world - @$(MAKE) movenew - -translation2:: - @$(MAKE) COQ_XML=-ftranslate2 world + @$(MAKE) COQ_XML="-ftranslate -no-strict" world @$(MAKE) movenew movenew:: @@ -1291,36 +1287,36 @@ movenew:: done # 2. Build new syntax images and compile theories -newworld:: $(COQTOPNEW) newinit newtheories newcontrib +newworld:: $(BESTCOQTOPNEW) newinit newtheories newcontrib newinit:: $(INITVO:%.vo=new%.vo) newtheories:: $(THEORIESVO:%.vo=new%.vo) newcontrib:: $(CONTRIBVO:%.vo=new%.vo) $(CONTRIBCMO) -COQTOPNEW=bin/coqtopnew.$(BEST)$(EXE) +BESTCOQTOPNEW=bin/coqtopnew.$(BEST)$(EXE) NEWCMX=$(HIGHPARSINGNEW:.cmo=.cmx) -NEWOPTS=-boot $(GLOB) -v8 -R newtheories Coq -R newcontrib Coq -NEWCOQBARE=$(COQTOPNEW) $(NEWOPTS) -nois -NEWCOQ=$(COQTOPNEW) $(NEWOPTS) -is states/initialnew.coq +NEWOPTS=-boot $(GLOB) -v8 +NEWCOQBARE=$(BESTCOQTOP) $(NEWOPTS) -nois +NEWCOQ=$(BESTCOQTOP) $(NEWOPTS) bin/coqtopnew.opt$(EXE): $(COQMKTOP) $(CMX) $(USERTACCMX) $(NEWCMX) $(COQMKTOP) -opt $(OPTFLAGS) $(NEWCMX) -o $@ bin/coqtopnew.byte$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(HIGHPARSINGNEW) - $(COQMKTOP) -top $(OPTFLAGS) $(HIGHPARSINGNEW) -o $@ + $(COQMKTOP) -g -top $(OPTFLAGS) $(HIGHPARSINGNEW) -o $@ -newtheories/Init/%.vo: $(COQTOPNEW) newtheories/Init/%.v +newtheories/Init/%.vo: $(BESTCOQTOPNEW) newtheories/Init/%.v $(NEWCOQBARE) -compile $* states/initialnew.coq: states/MakeInitialNew.v $(INITVO:%.vo=new%.vo) $(NEWCOQBARE) -batch -silent -load-vernac-source states/MakeInitialNew.v -outputstate states/initialnew.coq newcontrib/%.vo: newcontrib/%.v states/initialnew.coq - $(NEWCOQ) -compile $* + $(NEWCOQ) -compile newcontrib/$* newtheories/%.vo: newtheories/%.v states/initialnew.coq - $(NEWCOQ) -compile $* + $(NEWCOQ) -compile newtheories/$* # Dependencies .depend.newcoq: .depend.coq Makefile |