install de pcoq incorrect + spec rpm

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

7 files changed, 95 insertions, 17 deletions

diff --git a/Makefile b/Makefile
index 981ec78820..1c494ce062 100644
--- a/Makefile
+++ b/Makefile
@@ -696,7 +696,9 @@ clean::
 	rm -f bin/parser$(EXE) bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE)
 
 # install targets
-install-pcoq::
+install-pcoq:: install-pcoq-binaries install-pcoq-manpages
+
+install-pcoq-binaries::
 	$(MKDIR) $(FULLBINDIR)
 	cp  $(COQINTERFACE) $(FULLBINDIR)
 
diff --git a/distrib/Makefile b/distrib/Makefile
index 79dcdae715..4c4cbbad06 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -32,6 +32,7 @@ noarguments:
 	@echo "make arch-rpm     to prepare a rpm 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"
 	@echo "make deb          to build a debian package"
 	@echo "make win          to build a windows package"
 	@echo "make macosx       to build a MacOS-X package on a disk image"
@@ -150,7 +151,7 @@ arch-image: $(TARGZ)
 	 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;\
 	 $(MAKECOQ) coq check;\
-	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) BASETEXDIR=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
 	@echo " .... done"
 
 arch-tar-gz-final:
@@ -171,6 +172,7 @@ cleanall::
 
 rpm: src-rpm arch-rpm
 ide-rpm: ide-src-rpm ide-arch-rpm
+pcoq-rpm: pcoq-src-rpm pcoq-arch-rpm
 
 RPMTOPDIR=$(DISTRIBDIR)/RH/src
 RPMTMPPATHDIR=$(RPMTOPDIR)/admin
@@ -186,10 +188,13 @@ 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)
 COQSRCRPM=$(COQRPMPACKAGE).src.rpm
 COQRPM=$(COQRPMPACKAGE).$(ARCH).rpm
 COQIDESRCRPM=$(COQIDERPMPACKAGE).src.rpm
 COQIDERPM=$(COQIDERPMPACKAGE).$(ARCH).rpm
+PCOQSRCRPM=$(PCOQRPMPACKAGE).src.rpm
+PCOQRPM=$(PCOQRPMPACKAGE).$(ARCH).rpm
 
 RPMLOG=$(DISTRIBDIR)/RH/rpm.log
 RPMFILESLOG=$(DISTRIBDIR)/RH/coqfiles.log
@@ -200,6 +205,9 @@ arch-rpm: $(COQRPM)
 ide-src-rpm: $(COQIDESRCRPM)
 ide-arch-rpm: $(COQIDERPM)
 
+pcoq-src-rpm: $(PCOQSRCRPM)
+pcoq-arch-rpm: $(PCOQRPM)
+
 $(RPMTOPDIR):
 	@mkdir -p $(RPMTOPDIR)/BUILD
 	@mkdir -p $(RPMTOPDIR)/RPMS
@@ -256,18 +264,49 @@ $(COQIDERPM): $(COQIDESRCRPM)
 	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQIDERPM) .
 	chmod g+w $(COQIDERPM)
 
+$(PCOQSRCRPM): $(RPMTOPDIR) RH/coq_ext_for_pcoq.spec RH/coq-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
+	mv $(RPMTOPDIR)/SRPMS/$(PCOQSRCRPM) .
+	chmod g+w $(PCOQSRCRPM)
+	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coq-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)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(PCOQRPM) .
+	chmod g+w $(PCOQRPM)
+	rm -f $(RPMTOPDIR)/coq-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 install-coq >> $(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
 
+RH/coq-pcoq.list: $(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
+
 clean::
 	rm -fr $(RPMTOPDIR) RH/coq.list RH/$(COQPACKAGE) RH/build RH/rpmmacros RH/rpmrc
 
@@ -296,7 +335,7 @@ $(COQWINZIP): $(TARGZ)
 	 cd $(COQPACKAGE);\
 	 ./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
 	 $(MAKECOQ) coq;\
-	 $(MAKECOQ) -e COQINSTALLPREFIX=$(WININSTALL) install-coq) > win.log
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(WININSTALL) BASETEXDIR=$(WININSTALL) install-coq) > win.log
 	mv $(WINBUILDROOT)/$(COQPACKAGE)/INSTALL.win $(WININSTALL)
 	cd $(WININSTALL); zip -A -r $(DISTRIBDIR)/$(COQWINZIP) *
 
diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
index 69db2eae63..89536cb831 100644
--- a/distrib/RH/coq.spec
+++ b/distrib/RH/coq.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-8.0.tar.gz
+Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0cdrom.tar.gz
 Icon: petit-coq.gif
 
 %description
@@ -26,15 +26,15 @@ Coq is a proof assistant which:
 %setup
 
 %build
-./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 coq      # Use native coq to compile theories
+./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
 
 
 %clean
 make clean
 
 %install
-make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-coq
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT/ install-coq
 # To install only locally the binaries compiled with absolute paths
 
 %post
@@ -52,7 +52,7 @@ if [ -L /usr/local/lib/ocaml ]; then
   rm /usr/local/lib/ocaml
 fi
 
-# the spec file is moved to distrib/RH/src/coqX.Y but coq.list is in distrib/RH
+# the spec file is moved to distrib/RH/src/SPECS but coq.list is in distrib/RH
 %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
new file mode 100644
index 0000000000..ebdea5ad07
--- /dev/null
+++ b/distrib/RH/coq_ext_for_pcoq.spec
@@ -0,0 +1,35 @@
+Name: coq_ext_for_pcoq
+Version: 8.0cdrom
+Release: 1
+Summary: The Coq Extension for Pcoq
+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
+Icon: petit-coq.gif
+Requires: coq = 8.0cdrom
+
+%description
+The Coq Extension for Pcoq provides all facilities to interface Coq with
+Pcoq
+
+%prep
+%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 pcoq                   # Use native coq to compile theories
+
+
+%clean
+make clean
+
+%install
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$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
+%defattr(-,root,root)
+
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
index 515393690a..b618fdafa0 100644
--- a/distrib/RH/coqide.spec
+++ b/distrib/RH/coqide.spec
@@ -1,31 +1,31 @@
 Name: coqide
-Version: 8.0beta
+Version: 8.0cdrom
 Release: 1
 Summary: The Coq Integrated Development Interface
 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.0beta/coq-8.0cdrom.tar.gz
 Icon: petit-coq.gif
-Requires: coq = 8.0beta
+Requires: coq = 8.0cdrom
 
 %description
 The Coq Integrated Development Interface is a graphical interface for the 
 Coq proof assistant 
 
 %prep
-%setup -n coq-8.0beta
+%setup -n coq-8.0cdrom
 
 %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
+./configure -prefix /usr -emacs emacs -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/ install-coqide
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ BASETEXDIR=$RPM_BUILD_ROOT install-coqide
 # To install only locally the binaries compiled with absolute paths
 
 %post
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index 0b12ccba9e..53abb84575 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 coq      # Use native coq to compile theories
+./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
diff --git a/distrib/RH/do_build_pcoq b/distrib/RH/do_build_pcoq
new file mode 100755
index 0000000000..87ce91d552
--- /dev/null
+++ b/distrib/RH/do_build_pcoq
@@ -0,0 +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