diff options
| -rw-r--r-- | distrib/.cvsignore | 5 | ||||
| -rw-r--r-- | distrib/Makefile | 84 | ||||
| -rw-r--r-- | distrib/RH/.cvsignore | 8 | ||||
| -rw-r--r-- | distrib/RH/coq.spec | 9 | ||||
| -rw-r--r-- | distrib/RH/coq_ext_for_pcoq.spec | 15 | ||||
| -rw-r--r-- | distrib/RH/coqide.spec | 31 | ||||
| -rw-r--r-- | distrib/RH/do_build | 4 | ||||
| -rwxr-xr-x | distrib/RH/do_build_pcoq | 4 |
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 |