Finalisation du mecanisme de creation du rpm coqide

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

2 files changed, 61 insertions, 7 deletions

diff --git a/distrib/Makefile b/distrib/Makefile
index 31d2ac29ab..414ced6074 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -207,21 +207,21 @@ ${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz coq.spec
 	${RPM} -ba coq.spec
 	mv ${RPMTOPDIR}/SRPMS/${COQRPMPACKAGE}.src.rpm .
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm;\
+	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
 	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
 	fi)
 
-${COQIDERPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz coqide.spec
+${COQIDERPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coqide.spec
 	${MAKE} rpm-config
 	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
-	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES/${COQIDEPACKAGE}
+	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 coqide.spec
+	${RPM} -ba RH/coqide.spec
 	mv ${RPMTOPDIR}/SRPMS/${COQIDERPMPACKAGE}.src.rpm .
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm;\
+	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
 	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
 	fi)
 
@@ -232,7 +232,7 @@ ${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	${RPM} --rebuild ${COQRPMPACKAGE}.src.rpm
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm;\
+	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
 	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
 	fi)
 
@@ -242,7 +242,7 @@ ${COQIDERPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQIDERPMPACKAGE}.src.rpm
 	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
 	${RPM} --rebuild ${COQIDERPMPACKAGE}.src.rpm
 	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm;\
+	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
 	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
 	fi)
 
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
new file mode 100644
index 0000000000..763b2cc6d6
--- /dev/null
+++ b/distrib/RH/coqide.spec
@@ -0,0 +1,54 @@
+Name: coqide
+Version: 8.0beta
+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
+Icon: petit-coq.gif
+Requires: coq = 8.0beta
+
+%description
+The Coq Integrated Development Interface is a graphical interface for the 
+Coq proof assistant 
+
+%prep
+%setup -n coq-8.0beta
+
+%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
+
+%clean
+make clean
+
+%install
+make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install-ide
+# 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
+%defattr(-,root,root)
+/usr/bin/coqide.byte
+/usr/bin/coqide.opt
+/usr/bin/coqide
+/usr/lib/coq/ide/utf8.vo
+/usr/lib/coq/ide/coq.png
+/usr/lib/coq/ide/.coqide-gtk2rc
+/usr/lib/coq/ide/FAQ