meilleure separation de compil et install de coq, coqide et coq-interface

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5256 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 30 insertions, 17 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 414ced6074..869130f6df 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -59,7 +59,7 @@ noarguments:
 
 ################## Main targets
 
-distrib: tag tar-gz
+distrib: tag export tar-gz
 rpm: src-rpm arch-rpm
 ide-rpm: ide-src-rpm ide-arch-rpm
 
@@ -68,11 +68,19 @@ tag:
 	echo -n "Tagging the archive with version number $(DASHEDVERSION)...";\
 	cvs rtag -F $(DASHEDVERSION) $(MAJORVERSION)
 
-tar-gz: 
+export:
 	@echo -n Exporting a fresh copy of the archive...
 	@- rm -rf ${COQPACKAGE}
 	@cvs export -d $(COQPACKAGE) -r $(DASHEDVERSION) $(MAJORVERSION)
 	@echo done
+
+export-from-local:
+	@- rm -rf ${COQPACKAGE}
+	mkdir ${COQPACKAGE}
+	cd .. ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` distrib/${COQPACKAGE}/
+	cd ${COQPACKAGE}/ ; $(MAKE) clean
+
+tar-gz: 
 	@echo -n Removing the maintenance files and doc...
 #	@rm -rf ${COQPACKAGE}/doc     # doc is implementation doc
 	@rm -rf ${COQPACKAGE}/distrib
@@ -194,17 +202,18 @@ rpm-config: rpm-dirs
 # Les cibles suivantes ne sont pas acceptées sur DEC (car paramétrées)
 
 ${COQPACKAGE}.tar.gz:
-	${MAKE} tar-gz
+	${MAKE} export tar-gz
 
 # rpm 3.0 met dans LOCALARCH mais rpm 2.5 dans ARCH...
-${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz coq.spec
+${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coq.spec
 	${MAKE} rpm-config
 	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
 	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
 	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
 	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	${RPM} -ba coq.spec
+	- rm -fr $(RPMBUILDROOT)
+	${RPM} -ba RH/coq.spec
 	mv ${RPMTOPDIR}/SRPMS/${COQRPMPACKAGE}.src.rpm .
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
 	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
@@ -218,6 +227,7 @@ ${COQIDERPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coqide.spec
 	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
 	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
+	- rm -fr $(RPMBUILDROOT)
 	${RPM} -ba RH/coqide.spec
 	mv ${RPMTOPDIR}/SRPMS/${COQIDERPMPACKAGE}.src.rpm .
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
@@ -230,6 +240,7 @@ ${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm
 	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
 	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
+	#- rm -fr $(RPMBUILDROOT)
 	${RPM} --rebuild ${COQRPMPACKAGE}.src.rpm
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
 	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
@@ -240,6 +251,7 @@ ${COQIDERPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQIDERPMPACKAGE}.src.rpm
 	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
 	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
+	#- rm -fr $(RPMBUILDROOT)
 	${RPM} --rebuild ${COQIDERPMPACKAGE}.src.rpm
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
 	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
@@ -250,15 +262,15 @@ RH/coq.list: ${COQPACKAGE}.tar.gz Makefile config.distrib
 	rm -rf RH/${COQPACKAGE} RH/build
 	cd RH ; tar xzf ../${COQPACKAGE}.tar.gz
 	cd RH/${COQPACKAGE} ; sh ../do_build
-	cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install
+	cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install-coq
 	echo "# This file has been generated" > RH/coq.list
 	echo "# Do not edit" >>RH/coq.list
-	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g' -e '/coqide/d' >> ../coq.list
+	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g' >> ../coq.list
 
-coq.spec: RH/coq.list RH/coq.spec.tpl
-	echo "# This file has been generated from RH/coq.spec.tpl" > coq.spec
-	echo "# Do not edit" >> coq.spec
-	cd RH ; m4 -P coq.spec.tpl >> ../coq.spec
+RH/coq.spec: RH/coq.list RH/coq.spec.tpl
+	echo "# This file has been generated from RH/coq.spec.tpl" > RH/coq.spec
+	echo "# Do not edit" >> RH/coq.spec
+	cd RH ; m4 -P coq.spec.tpl >> coq.spec
 
 ##########
 contrib-tag:
diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl
index b466401d65..fa52d635d1 100644
--- a/distrib/RH/coq.spec.tpl
+++ b/distrib/RH/coq.spec.tpl
@@ -1,12 +1,12 @@
 Name: coq
-Version: 8.0beta
+Version: 8.0
 Release: 1
 Summary: The Coq Proof Assistant
 Copyright: freely redistributable
 Group: Applications/Math
 Vendor: INRIA & LRI
 URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0beta/coq-8.0beta.tar.gz
+Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
 Icon: petit-coq.gif
 
 %description
@@ -32,7 +32,7 @@ m4_include(do_build)
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
 # To install only locally the binaries compiled with absolute paths
 
 %post
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
index 763b2cc6d6..515393690a 100644
--- a/distrib/RH/coqide.spec
+++ b/distrib/RH/coqide.spec
@@ -19,13 +19,13 @@ Coq proof assistant
 
 %build
 ./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all # Need ocamlc.opt and ocamlopt.opt
-make ide  # Use native coq to compile theories
+make coqide  # Use native coq to compile theories
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-ide
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coqide
 # To install only locally the binaries compiled with absolute paths
 
 %post
@@ -48,6 +48,7 @@ fi
 /usr/bin/coqide.byte
 /usr/bin/coqide.opt
 /usr/bin/coqide
+/usr/lib/coq/ide/utf8.v
 /usr/lib/coq/ide/utf8.vo
 /usr/lib/coq/ide/coq.png
 /usr/lib/coq/ide/.coqide-gtk2rc
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index db8fa10354..0b12ccba9e 100644
--- a/distrib/RH/do_build
+++ b/distrib/RH/do_build
@@ -1,2 +1,2 @@
 ./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make world      # Use native coq to compile theories
+make coq      # Use native coq to compile theories