diff options
| author | herbelin | 2003-09-12 22:35:35 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 22:35:35 +0000 |
| commit | ca1ac8b00547240a75ead61b32f7f726acd36404 (patch) | |
| tree | 05f5c4b974fcc6a299b2d464fdb33fcb49dbfc33 | |
| parent | 8efaddd7df1603091fa27a10ad7c184b4241bebb (diff) | |
Retour à des cibles plus explicites: world7 et world8, install7 et install8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4394 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 23 |
1 files changed, 14 insertions, 9 deletions
@@ -329,15 +329,18 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ coqbinaries:: ${COQBINARIES} -world: coqbinaries coqlib8 tools coqide # coqlib7-clean coqlib7 +newworld: world8 -world7: coqbinaries coqlib7 tools coqide +oldworld: world7 + +world: world7 -coqlib7-clean: - rm -f theories/*/*.vo contrib/*/*.vo +world8: coqbinaries coqlib8-source coqlib8 tools coqide + +world7: coqbinaries coqlib7 tools coqide coqlib7: states theories contrib - # TODO: compile in an other directory since + # TODO: compile in an other directory since for world8 # theories and contrib contains the .vo for the translator coqlight: coqbinaries states theories-light tools @@ -874,7 +877,9 @@ FULLCOQLIB=$(COQINSTALLPREFIX)$(COQLIB) FULLMANDIR=$(COQINSTALLPREFIX)$(MANDIR) FULLEMACSLIB=$(COQINSTALLPREFIX)$(EMACSLIB) -install: install-$(BEST) install-binaries install-library install-manpages +install: install7 + +install8: install-$(BEST) install-binaries install-library install-manpages install7: install-$(BEST) install-binaries install-library7 install-manpages @@ -1288,9 +1293,9 @@ devel: # Entries for new syntax ############################################################################ -coqlib8: translation movenew newworld - # 1. Translate the old syntax files and build new syntax theories hierarchy +coqlib8-source: translation movenew + translation:: $(BESTCOQTOP) @$(MAKE) SYNTAX="-translate -no-strict" coqlib7 @$(MAKE) movenew @@ -1305,7 +1310,7 @@ movenew:: done # 2. Compile theories -newworld:: $(BESTCOQTOP) newinit newtheories newcontrib +coqlib8:: newinit newtheories newcontrib NEWINITVO=$(INITVO:%.vo=new%.vo) NEWTHEORIESVO=$(THEORIESVO:%.vo=new%.vo) |
