aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2003-09-12 22:35:35 +0000
committerherbelin2003-09-12 22:35:35 +0000
commitca1ac8b00547240a75ead61b32f7f726acd36404 (patch)
tree05f5c4b974fcc6a299b2d464fdb33fcb49dbfc33
parent8efaddd7df1603091fa27a10ad7c184b4241bebb (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--Makefile23
1 files changed, 14 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 7f2755eb68..7fac3b0a63 100644
--- a/Makefile
+++ b/Makefile
@@ -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)