amelioration des specs RPM

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

5 files changed, 79 insertions, 134 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index d49aa27f81..16c4264b41 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -28,8 +28,9 @@ noarguments:
 	@echo "make tag          to tag the current archive with the release number"
 	@echo "make tar-gz       to build a tar.gz of sources"
 	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
-	@echo "make rpm          to prepare a src.rpm and a rpm for the current arch"
-	@echo "make arch-rpm     to prepare a rpm for the current arch from the src.rpm"
+	@echo "make rpm          to prepare source and arch rpms"
+	@echo "make src-rpm      to prepare source rpms from the tar.gz"
+	@echo "make arch-rpm     to prepare binary rpms for the current arch from the src.rpm"
 	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
 	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
 	@echo "make pcoq-rpm     to build a src.rpm and a rpm for pcoq on this arch"
@@ -167,10 +168,13 @@ cleanall::
 	rm -f $(COQPACKAGE) $(TARGZ) $(ARCHTARGZ) arch-image.log test.log
 
 ###################################################################
-# RPM (Coq and CoqIde are separated)
+# RPM (Coq, CoqIde and Pcoq are separated)
 #
-
 rpm: src-rpm arch-rpm
+src-rpm: coq-src-rpm ide-src-rpm pcoq-src-rpm
+arch-rpm: coq-arch-rpm ide-arch-rpm pcoq-arch-rpm
+
+coq-rpm: coq-src-rpm coq-arch-rpm
 ide-rpm: ide-src-rpm ide-arch-rpm
 pcoq-rpm: pcoq-src-rpm pcoq-arch-rpm
 
@@ -186,9 +190,10 @@ RPMVERSION=`$(RAWRPM) --version | sed -e "s/RPM version \(.\).*/\1/"`
 RPM=$(RAWRPM) --buildroot $(RPMBUILDROOT) --target $(ARCH) --rcfile RH/rpmrc
 
 # rpm files
-COQRPMPACKAGE=coq-$(VERSION)-$(RELEASENUM)
-COQIDERPMPACKAGE=coqide-$(VERSION)-$(RELEASENUM)
-PCOQRPMPACKAGE=coq_ext_for_pcoq-$(VERSION)-$(RELEASENUM)
+RPMEXT=$(VERSION)-$(RELEASENUM)
+COQRPMPACKAGE=coq-$(RPMEXT)
+COQIDERPMPACKAGE=coqide-$(RPMEXT)
+PCOQRPMPACKAGE=coq_ext_for_pcoq-$(RPMEXT)
 COQSRCRPM=$(COQRPMPACKAGE).src.rpm
 COQRPM=$(COQRPMPACKAGE).$(ARCH).rpm
 COQIDESRCRPM=$(COQIDERPMPACKAGE).src.rpm
@@ -199,8 +204,8 @@ PCOQRPM=$(PCOQRPMPACKAGE).$(ARCH).rpm
 RPMLOG=$(DISTRIBDIR)/RH/rpm.log
 RPMFILESLOG=$(DISTRIBDIR)/RH/coqfiles.log
 
-src-rpm: $(COQSRCRPM)
-arch-rpm: $(COQRPM)
+coq-src-rpm: $(COQSRCRPM)
+coq-arch-rpm: $(COQRPM)
 
 ide-src-rpm: $(COQIDESRCRPM)
 ide-arch-rpm: $(COQIDERPM)
@@ -229,95 +234,25 @@ RH/rpmrc: config.distrib
 	echo tmppath: $(RPMTMPPATHDIR) >> RH/rpmrc;\
 	fi)
 
-$(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)
-	@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
-
-$(COQRPM): $(COQSRCRPM)
-	@-rm -fr $(RPMBUILDROOT)
-	@mkdir -p $(RPMBUILDROOT)
-	@echo "Building the $(ARCH) rpm... (see RH/rpm.log)"
-	cp -f RH/coq.list $(RPMTOPDIR)
-	$(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 RH/coqide.list $(TARGZ) RH/rpmrc
+%-$(RPMEXT).src.rpm: RH/%.spec $(TARGZ) RH/rpmrc
 	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
 	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
-	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/* $(RPMTOPDIR)/coqide.list
-
-$(COQIDERPM): $(COQIDESRCRPM)
-	@-rm -fr $(RPMBUILDROOT)
-	@mkdir -p $(RPMBUILDROOT)
-	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) $(RPMTOPDIR)/coqide.list
+	$(RPM) -bs RH/$*.spec
+	mv $(RPMTOPDIR)/SRPMS/$@ .
+	chmod g+w $@
 
-$(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/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)/pcoq.list
-
-$(PCOQRPM): $(PCOQSRCRPM)
-	@-rm -fr $(RPMBUILDROOT)
+%.$(ARCH).rpm: %.src.rpm
 	@mkdir -p $(RPMBUILDROOT)
-	@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)/pcoq.list
-
-FILESDIR=$(DISTRIBDIR)/RH/build
-
-RH/$(COQPACKAGE)/config/Makefile: $(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) ; \
-	  ./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)/$*
+	@echo "Building the $(ARCH) rpm for $*... (see RH/rpm.log)"
+	$(RPM) --rebuild $< > $(RPMLOG)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$@ .
+	chmod g+w $@
 
 clean::
-	rm -fr $(RPMTOPDIR) RH/coq.list RH/coqide.list RH/pcoq.list RH/$(COQPACKAGE) $(FILESDIR) RH/rpmmacros RH/rpmrc
+	rm -fr $(RPMTOPDIR) RH/rpmmacros RH/rpmrc
 
 cleanall::
-	rm -f $(COQSRCRPM) $(COQRPM) $(COQIDESRCRPM) $(COQIDERPM) $(RPMLOG) $(RPMFILESLOG)
+	rm -f *.rpm $(RPMLOG) $(RPMFILESLOG)
 
 ###################################################################
 # Zip for Windows (package does not contain coqide)
diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore
index d7a4769a28..7e1d30b7b3 100644
--- a/distrib/RH/.cvsignore
+++ b/distrib/RH/.cvsignore
@@ -1,5 +1,3 @@
 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 f28177e03a..eb6c9631f4 100644
--- a/distrib/RH/coq.spec
+++ b/distrib/RH/coq.spec
@@ -8,6 +8,7 @@ Vendor: INRIA & LRI
 URL: http://coq.inria.fr
 Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
 Icon: petit-coq.gif
+BuildRoot: /var/tmp/coq
 
 %description
 Coq is a proof assistant which: 
@@ -17,43 +18,40 @@ Coq is a proof assistant which:
   - extracts a certified program from the constructive proof
     of its formal specification, 
 
-# Ocaml is required but it is better to install it not with rpm but by
-# hand in /usr/local
-# Requires: ocaml >= 3.06
-
+Requires: ocaml >= 3.06
 
+%define debug_package %{nil}
+                                                                               
 %prep
 %setup
 
 %build
-./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
+./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
+   -emacslib %{_datadir}/emacs/site-lisp \
+   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
+   -opt -reals all -coqide no
+make coq
 
 
 %clean
+rm -rf %{buildroot}
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
-# 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
-
-# the spec file is read from distrib/RH/src/SOURCES/coqX.Y
-# but coq.list is in distrib/RH/src
-%files -f ../../coq.list
+rm -rf %{buildroot}
+make -e COQINSTALLPREFIX=%{buildroot} install-coq
+
+%files
+%{_bindir}/*
+%{_libdir}/coq/theories
+%{_libdir}/coq/contrib
+%{_libdir}/coq/states
+%{_libdir}/coq/theories7
+%{_libdir}/coq/contrib7
+%{_libdir}/coq/states7
+%{_mandir}/man1/*
+%{_datadir}/emacs/site-lisp/*
+%{_datadir}/texmf/tex/latex/misc/*
+
 %defattr(-,root,root)
 
diff --git a/distrib/RH/coq_ext_for_pcoq.spec b/distrib/RH/coq_ext_for_pcoq.spec
index 61f738c892..29671985f8 100644
--- a/distrib/RH/coq_ext_for_pcoq.spec
+++ b/distrib/RH/coq_ext_for_pcoq.spec
@@ -9,28 +9,35 @@ URL: http://coq.inria.fr
 Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
 Icon: petit-coq.gif
 Requires: coq = 8.0
+BuildRoot: /var/tmp/pcoq
 
 %description
 The Coq Extension for Pcoq provides all facilities to interface Coq with
 Pcoq
 
+%define debug_package %{nil}
+
 %prep
 %setup -n coq-8.0
 
 %build
-./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
-
+./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
+   -emacslib %{_datadir}/emacs/site-lisp \
+   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
+   -opt -reals all -coqide no
+make pcoq
 
 %clean
+rm -rf %{buildroot}
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-pcoq
-# To install only locally the binaries compiled with absolute paths
+rm -rf %{buildroot}
+make -e COQINSTALLPREFIX=%{buildroot} install-pcoq
+
+%files
+%{_bindir}/*
+%{_mandir}/man1/*
 
-# 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 754583ec70..e6d606166f 100644
--- a/distrib/RH/coqide.spec
+++ b/distrib/RH/coqide.spec
@@ -9,26 +9,33 @@ URL: http://coq.inria.fr
 Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
 Icon: petit-coq.gif
 Requires: coq = 8.0
+BuildRoot: /var/tmp/coqide
 
 %description
 The Coq Integrated Development Interface is a graphical interface for the 
 Coq proof assistant 
 
+%define debug_package %{nil}
+
 %prep
 %setup -n coq-8.0
 
 %build
-./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
+./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
+   -emacslib %{_datadir}/emacs/site-lisp \
+   -coqdocdir %{_datadir}/texmf/tex/latex/misc -opt -reals all
+make coqide
 
 %clean
+rm -rf %{buildroot}
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coqide
-# To install only locally the binaries compiled with absolute paths
+rm -rf %{buildroot}
+make -e COQINSTALLPREFIX=%{buildroot} install-coqide
+
+%files
+%{_bindir}/*
+%{_libdir}/coq/ide
 
-# 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)