*** empty log message ***

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

8 files changed, 74 insertions, 86 deletions

diff --git a/distrib/.cvsignore b/distrib/.cvsignore
index 33bde2667..46e8aed30 100644
--- a/distrib/.cvsignore
+++ b/distrib/.cvsignore
@@ -1,18 +1,17 @@
 rpmbuildroot
 i386
+tar-i386
 sun4
 alpha
 apx
 alpha
 ppc
 redhat
-rpmrc
-rpmmacros
 config.distrib
 coq-*
 contrib-*
 patch-*
 deb_build
-coq.spec
 coq_*
 sun4u
+*.rpm
diff --git a/distrib/Makefile b/distrib/Makefile
index ef7936f4a..4e0ab182b 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -149,7 +149,7 @@ arch-image: $(TARGZ)
 	(cd $(ARCHBUILDROOT);\
 	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
 	 cd $(COQPACKAGE);\
-	 ./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all -coqide no;\
+	 ./configure -prefix /usr -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all;\
 	 $(MAKECOQ) coq check;\
 	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) BASETEXDIR=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
 	@echo " .... done"
@@ -233,7 +233,8 @@ $(COQSRCRPM): $(RPMTOPDIR) RH/coq.spec RH/coq.list $(TARGZ) RH/rpmrc
 	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
 	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
 	cp -f RH/coq.list $(RPMTOPDIR)
-	$(RPM) -bs RH/coq.spec
+	@echo "Building the source rpm... (see RH/rpm.log)"
+	$(RPM) -bs RH/coq.spec > RH/rpm.log
 	mv $(RPMTOPDIR)/SRPMS/$(COQSRCRPM) .
 	chmod g+w $(COQSRCRPM)
 	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coq.list
@@ -241,74 +242,79 @@ $(COQSRCRPM): $(RPMTOPDIR) RH/coq.spec RH/coq.list $(TARGZ) RH/rpmrc
 $(COQRPM): $(COQSRCRPM)
 	@-rm -fr $(RPMBUILDROOT)
 	@mkdir -p $(RPMBUILDROOT)
-	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
+	@echo "Building the $(ARCH) rpm... (see RH/rpm.log)"
 	cp -f RH/coq.list $(RPMTOPDIR)
-	$(RPM) --rebuild $(COQSRCRPM)
+	$(RPM) --rebuild $(COQSRCRPM) > RH/rpm.log
 	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQRPM) .
 	chmod g+w $(COQRPM)
 	rm -f $(RPMTOPDIR)/coq.list
 
-$(COQIDESRCRPM): $(RPMTOPDIR) RH/coqide.spec $(TARGZ) RH/rpmrc
+$(COQIDESRCRPM): $(RPMTOPDIR) RH/coqide.spec RH/coqide.spec $(TARGZ) RH/rpmrc
 	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
 	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
-	$(RPM) -bs RH/coqide.spec
+	cp -f RH/coqide.list $(RPMTOPDIR)
+	@echo "Building the source rpm... (see RH/rpm.log)"
+	$(RPM) -bs RH/coqide.spec > RH/rpm.log
 	mv $(RPMTOPDIR)/SRPMS/$(COQIDESRCRPM) .
 	chmod g+w $(COQIDESRCRPM)
-	rm -fr $(RPMTOPDIR)/SOURCES/*
+	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coqide.list
 
 $(COQIDERPM): $(COQIDESRCRPM)
 	@-rm -fr $(RPMBUILDROOT)
 	@mkdir -p $(RPMBUILDROOT)
-	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
-	$(RPM) --rebuild $(COQIDESRCRPM)
+	cp -f RH/coqide.list $(RPMTOPDIR)
+	@echo "Building the $(ARCH) rpm... (see RH/rpm.log)"
+	$(RPM) --rebuild $(COQIDESRCRPM) > RH/rpm.log
 	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQIDERPM) .
-	chmod g+w $(COQIDERPM)
+	chmod g+w $(COQIDERPM) $(RPMTOPDIR)/coqide.list
 
-$(PCOQSRCRPM): $(RPMTOPDIR) RH/coq_ext_for_pcoq.spec RH/coq-pcoq.list $(TARGZ) RH/rpmrc
+$(PCOQSRCRPM): $(RPMTOPDIR) RH/coq_ext_for_pcoq.spec RH/pcoq.list $(TARGZ) RH/rpmrc
 	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
 	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
-	cp -f RH/coq-pcoq.list $(RPMTOPDIR)
-	$(RPM) -bs RH/coq_ext_for_pcoq.spec
+	cp -f RH/pcoq.list $(RPMTOPDIR)
+	@echo "Building the source rpm... (see RH/rpm.log)"
+	$(RPM) -bs RH/coq_ext_for_pcoq.spec > RH/rpm.log
 	mv $(RPMTOPDIR)/SRPMS/$(PCOQSRCRPM) .
 	chmod g+w $(PCOQSRCRPM)
-	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coq-pcoq.list
+	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/pcoq.list
 
 $(PCOQRPM): $(PCOQSRCRPM)
 	@-rm -fr $(RPMBUILDROOT)
 	@mkdir -p $(RPMBUILDROOT)
-	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
-	cp -f RH/coq-pcoq.list $(RPMTOPDIR)
-	$(RPM) --rebuild $(PCOQSRCRPM)
+	@echo "Building the $(ARCH) rpm... (see RH/rpm.log)"
+	cp -f RH/pcoq.list $(RPMTOPDIR)
+	$(RPM) --rebuild $(PCOQSRCRPM) > RH/rpm.log
 	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(PCOQRPM) .
 	chmod g+w $(PCOQRPM)
-	rm -f $(RPMTOPDIR)/coq-pcoq.list
+	rm -f $(RPMTOPDIR)/pcoq.list
 
-RH/coq.list: $(TARGZ) config.distrib
-	rm -rf RH/$(COQPACKAGE) RH/build
-	cd RH ; tar xzf ../$(TARGZ)
-	@echo "Building coq files list... (see RH/coqfiles.log)"
-	cd RH/$(COQPACKAGE) ; sh ../do_build > $(RPMFILESLOG)
-	cd RH/$(COQPACKAGE) ; $(MAKECOQ) COQINSTALLPREFIX=$(DISTRIBDIR)/RH/build BASETEXDIR=$(DISTRIBDIR)/RH/build install-coq >> $(RPMFILESLOG)
-	@echo " ... done"
-	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' >> ../coq.list
-	rm -rf RH/$(COQPACKAGE) RH/build
+FILESDIR=$(DISTRIBDIR)/RH/build
 
-RH/coq-pcoq.list: $(TARGZ) config.distrib
+RH/$(COQPACKAGE)/config/Makefile: $(TARGZ) config.distrib
 	rm -rf RH/$(COQPACKAGE) RH/build
 	cd RH ; tar xzf ../$(TARGZ)
-	@echo "Building pcoq files list... (see RH/coqfiles.log)"
-	cd RH/$(COQPACKAGE) ; sh ../do_build_pcoq > $(RPMFILESLOG)
-	cd RH/$(COQPACKAGE) ; $(MAKECOQ) COQINSTALLPREFIX=$(DISTRIBDIR)/RH/build BASETEXDIR=$(DISTRIBDIR)/RH/build install-pcoq >> $(RPMFILESLOG)
-	@echo " ... done"
-	echo "# This file has been generated" > RH/coq-pcoq.list
-	echo "# Do not edit" >>RH/coq-pcoq.list
-	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g' >> ../coq-pcoq.list
-	rm -rf RH/$(COQPACKAGE) RH/build
+	@echo "Building coq files list... (see RH/coqfiles.log)"
+	cd RH/$(COQPACKAGE) ; \
+	  ./configure -prefix /usr \
+	        -emacslib /usr/share/emacs/site-lisp -opt -reals all \
+	  > $(RPMFILESLOG)
+
+RH/pcoq.spec:
+	cd RH ; ln -s coq_ext_for_pcoq.spec pcoq.spec
+
+RH/%.list: RH/%.spec RH/$(COQPACKAGE)/config/Makefile
+	rm -rf $(FILESDIR)/$*
+	cd RH/$(COQPACKAGE) ;\
+	  $(MAKECOQ) COQINSTALLPREFIX=$(FILESDIR)/$* $* install-$* \
+	    >> $(RPMFILESLOG) 2>&1
+	echo "# This file has been generated. Do not edit" > $@
+	cd $(FILESDIR)/$* ; \
+	  find . '!' -type d | sed -e 's|^\./|/|g' >> $(DISTRIBDIR)/$@
+	@echo " ... $@ done"
+#	rm -rf $(FILESDIR)/$*
 
 clean::
-	rm -fr $(RPMTOPDIR) RH/coq.list RH/$(COQPACKAGE) RH/build RH/rpmmacros RH/rpmrc
+	rm -fr $(RPMTOPDIR) RH/coq.list RH/coqide.list RH/pcoq.list RH/$(COQPACKAGE) $(FILESDIR) RH/rpmmacros RH/rpmrc
 
 cleanall::
 	rm -f $(COQSRCRPM) $(COQRPM) $(COQIDESRCRPM) $(COQIDERPM) $(RPMLOG) $(RPMFILESLOG)
diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore
index 18eeb6844..d7a4769a2 100644
--- a/distrib/RH/.cvsignore
+++ b/distrib/RH/.cvsignore
@@ -1,3 +1,5 @@
-build
-coq.list
-coq-7.0
+build src
+coq.list pcoq.list coqide.list
+pcoq.spec
+rpmmacros rpmrc
+coq-*
diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
index 89536cb83..c8945b4fa 100644
--- a/distrib/RH/coq.spec
+++ b/distrib/RH/coq.spec
@@ -26,15 +26,15 @@ Coq is a proof assistant which:
 %setup
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq                    # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make coq       # Use native coq to compile theories
 
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT/ install-coq
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
 # To install only locally the binaries compiled with absolute paths
 
 %post
@@ -52,7 +52,8 @@ if [ -L /usr/local/lib/ocaml ]; then
   rm /usr/local/lib/ocaml
 fi
 
-# the spec file is moved to distrib/RH/src/SPECS but coq.list is in distrib/RH
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but coq.list is in distrib/RH/src
 %files -f ../../coq.list
 %defattr(-,root,root)
 
diff --git a/distrib/RH/coq_ext_for_pcoq.spec b/distrib/RH/coq_ext_for_pcoq.spec
index ebdea5ad0..f774372e6 100644
--- a/distrib/RH/coq_ext_for_pcoq.spec
+++ b/distrib/RH/coq_ext_for_pcoq.spec
@@ -6,7 +6,7 @@ Copyright: freely redistributable
 Group: Applications/Math
 Vendor: INRIA & LRI
 URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq_ext_for_pcoq-8.0cdrom.tar.gz
+Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0cdrom.tar.gz
 Icon: petit-coq.gif
 Requires: coq = 8.0cdrom
 
@@ -15,21 +15,22 @@ The Coq Extension for Pcoq provides all facilities to interface Coq with
 Pcoq
 
 %prep
-%setup
+%setup -n coq-8.0cdrom
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq                   # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make pcoq      # Use native coq to compile theories
 
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT/ install-pcoq
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-pcoq
 # To install only locally the binaries compiled with absolute paths
 
-%files -f ../../coq-pcoq.list
-# the spec file is moved to distrib/RH/src/SPECS but coq.list is in distrib/RH
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but pcoq.list is in distrib/RH/src
+%files -f ../../pcoq.list
 %defattr(-,root,root)
 
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
index b618fdafa..420589b26 100644
--- a/distrib/RH/coqide.spec
+++ b/distrib/RH/coqide.spec
@@ -18,38 +18,17 @@ Coq proof assistant
 %setup -n coq-8.0cdrom
 
 %build
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all   # Need ocamlc.opt and ocamlopt.opt
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all   # Need ocamlc.opt and ocamlopt.opt
 make coqide  # Use native coq to compile theories
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT install-coqide
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coqide
 # To install only locally the binaries compiled with absolute paths
 
-%post
-# This is a because the Coq Team usually build Coq with Ocaml in /usr/local
-# but ocaml is actually in /usr if coming from a rpm package
-# This works only if ocaml has been installed by rpm
-if [ ! -e /usr/local/lib/ocaml ]; then
-  ln -s /usr/lib/ocaml /usr/local/lib/ocaml || true
-fi
-
-%postun
-# This is because the Coq Team usually build Coq with Ocaml in /usr/local
-# but ocaml is actually in /usr if coming from a rpm package
-if [ -L /usr/local/lib/ocaml ]; then
-  rm /usr/local/lib/ocaml
-fi
-
-%files
+# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
+# but coqide.list is in distrib/RH/src
+%files -f ../../coqide.list
 %defattr(-,root,root)
-/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
-/usr/lib/coq/ide/FAQ
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index 53abb8457..103d4a880 100644
--- a/distrib/RH/do_build
+++ b/distrib/RH/do_build
@@ -1,2 +1,2 @@
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq                    # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make coq       # Use native coq to compile theories
diff --git a/distrib/RH/do_build_pcoq b/distrib/RH/do_build_pcoq
index 87ce91d55..0477d001b 100755
--- a/distrib/RH/do_build_pcoq
+++ b/distrib/RH/do_build_pcoq
@@ -1,2 +1,2 @@
-./configure -prefix /usr -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq                   # Use native coq to compile theories
+./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
+make pcoq      # Use native coq to compile theories