diff options
| -rw-r--r-- | INSTALL | 3 | ||||
| -rw-r--r-- | distrib/.cvsignore | 1 | ||||
| -rw-r--r-- | distrib/Makefile | 34 | ||||
| -rw-r--r-- | distrib/RELEASE | 7 | ||||
| -rw-r--r-- | distrib/RH/.cvsignore | 2 | ||||
| -rw-r--r-- | distrib/RH/coq.spec.tpl | 78 | ||||
| -rw-r--r-- | distrib/RH/do_build | 2 | ||||
| -rw-r--r-- | distrib/debian/coq.emacsen-startup | 6 |
8 files changed, 110 insertions, 23 deletions
@@ -109,8 +109,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). to compile Coq in Objective Caml bytecode (and native-code if supported). This will compile the entire system. This phase can take more or less time, - depending on your architecture (about 30 minutes for both compilations - on a Pentium Pro 150), and is fairly verbose. + depending on your architecture and is fairly verbose. 6- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at diff --git a/distrib/.cvsignore b/distrib/.cvsignore index da1304664..8f38c5ecd 100644 --- a/distrib/.cvsignore +++ b/distrib/.cvsignore @@ -12,3 +12,4 @@ config.distrib coq-* contrib-* patch-* +deb_build diff --git a/distrib/Makefile b/distrib/Makefile index 9fa9044e9..78149f730 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -70,7 +70,7 @@ tar-gz: @echo done @echo -n Building the tar.gz source package @tar cvf ${COQPACKAGE}.tar ${COQPACKAGE} - @gzip ${COQPACKAGE}.tar + @gzip --best ${COQPACKAGE}.tar @echo done @echo Checking release parameters ./check-list @@ -107,12 +107,12 @@ release-bin: @echo @read tar -cvf $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar --files-from $(COQLIB)/COQFILES - gzip $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar + gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar arch-tar-gz-final: (cd ${ARCHBUILDROOT}/buildroot;\ tar -cvf ${DISTRIBDIR}/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *) - gzip $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar + gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar arch-tar-gz: ${COQPACKAGE}.tar.gz @echo "Building $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz to be installed in /usr/local/" @@ -157,7 +157,7 @@ ${COQPACKAGE}.tar.gz: ${MAKE} tar-gz # rpm 3.0 met dans LOCALARCH mais rpm 2.5 dans ARCH... -${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz +${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz coq.spec ${MAKE} rpm-config cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES @@ -182,6 +182,16 @@ ${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\ fi) +RH/coq.list: ${COQPACKAGE}.tar.gz Makefile config.distrib + rm -rf RH/${COQPACKAGE} RH/build + cd RH ; tar xzf ../${COQPACKAGE}.tar.gz + cd RH/${COQPACKAGE} ; sh ../do_build + cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install + cd RH/build ; find . '!' -type d > ../coq.list + +coq.spec: RH/coq.list RH/coq.spec.tpl + cd RH ; m4 -P coq.spec.tpl > ../coq.spec + ########## contrib-tag: @dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\ @@ -198,7 +208,7 @@ contrib-tar-gz: - rm contrib-${VERSION}.tar.gz @echo -n Building the tar.gz contrib package @tar cvf contrib-${VERSION}.tar contrib-${VERSION} - @gzip contrib-${VERSION}.tar + @gzip --best contrib-${VERSION}.tar @echo done ########## @@ -210,7 +220,7 @@ patch: rm -rf ${COQPACKAGE} gunzip -c ${COQPACKAGE}.tar.gz | tar x diff -rc coq-$(PREVIOUSVERSION) ${COQPACKAGE} > patch-${VERSION}-$(PREVIOUSVERSION) - gzip patch-${VERSION}-$(PREVIOUSVERSION) + gzip --best patch-${VERSION}-$(PREVIOUSVERSION) ########## clean: @@ -263,8 +273,10 @@ patch-ftp-install: prep-ftp-install chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz deb: ${COQPACKAGE}.tar.gz - tar xzf ${COQPACKAGE}.tar.gz - mv ${COQPACKAGE} ${COQPACKAGE}.orig - tar xzf ${COQPACKAGE}.tar.gz - cd ${COQPACKAGE} ; cp -a distrib/debian . - cd ${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us + rm -rf deb_build + mkdir -p deb_build + cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz + cd deb_build ; mv ${COQPACKAGE} ${COQPACKAGE}.orig + cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz + cd deb_build/${COQPACKAGE} ; cp -a distrib/debian . + cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us diff --git a/distrib/RELEASE b/distrib/RELEASE index 8290856dc..0efa6c2b7 100644 --- a/distrib/RELEASE +++ b/distrib/RELEASE @@ -22,17 +22,12 @@ A1) VÉRIFICATIONS - Changement des variables en tête du fichier "configure" et vérification du numéro de versions de OCaml et Camlp4 demandées - - Mise à jour des champs Version, Source et Require et vérifier la - liste des "%files" dans "distrib/coq.spec" + - Mise à jour des champs Version, Source et Require - Relecture des fichiers "README", "README.win", en particulier, vérification du numéro de version, des adresses internet et des coordonnées de Coq - Relecture des fichiers "INSTALL", "INSTALL.win" en particulier numéro de version de coq et numéros des versions de OCaml et Camlp4 demandées - - - S'assurer après un "make cleanall" que "make world" et "make - world-opt" commutent # Caduc pour la V7 - - Mise à jour/nettoyage du fichier CHANGES et du fichier ANNONCE EN CAS DE MODIFICATION DE L'ARCHIVE, REPRENDRE EN A3 diff --git a/distrib/RH/.cvsignore b/distrib/RH/.cvsignore new file mode 100644 index 000000000..bfec41c5e --- /dev/null +++ b/distrib/RH/.cvsignore @@ -0,0 +1,2 @@ +build +coq.list diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl new file mode 100644 index 000000000..44a14c7ea --- /dev/null +++ b/distrib/RH/coq.spec.tpl @@ -0,0 +1,78 @@ +Name: coq +Version: 7.0 +Release: 1 +Summary: The Coq Proof Assistant +Copyright: freely redistributable +Group: Applications/Math +Vendor: INRIA Rocquencourt +URL: http://coq.inria.fr +Source: ftp://ftp.inria.fr/INRIA/coq/V7.0/coq-7.0.tar.gz +Icon: petit-coq.gif + +%description +Coq is a proof assistant which: + - allows to handle calculus assertions, + - check mechanically proofs of these assertions, + - helps to find formal proofs, + - 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.01 + + +%prep +%setup + +%build +m4_include(coq.list) + +%clean +make clean + +%install +make -e COQINSTALLPREFIX=$RPM_BUILD_ROOT/ install +# 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 +/usr/bin/coqc +/usr/bin/coqtop +/usr/bin/coqtop.byte +/usr/bin/coqtop.opt +/usr/bin/coq-tex +/usr/bin/coqdep +/usr/bin/gallina +/usr/bin/coq_makefile +/usr/bin/coq-interface +/usr/bin/parser +#/usr/bin/coq_searchisos.out +/usr/bin/coqmktop +#/usr/bin/coq2html +#/usr/bin/coq2latex +/usr/lib/coq +#/usr/man/man1/coqc.1 +#/usr/man/man1/coqtop.1 +#/usr/man/man1/coqmktop.1 +/usr/man/man1/coqdep.1 +/usr/man/man1/gallina.1 +/usr/man/man1/coq-tex.1 +#/usr/man/man1/coq2latex.1 +#/usr/man/man1/coq2html.1 +/usr/share/emacs/site-lisp/coq.el +/usr/share/emacs/site-lisp/coq.elc diff --git a/distrib/RH/do_build b/distrib/RH/do_build new file mode 100644 index 000000000..b504dd070 --- /dev/null +++ b/distrib/RH/do_build @@ -0,0 +1,2 @@ +./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt # Need ocamlc.opt and ocamlopt.opt +make world # Use native coq to compile theories diff --git a/distrib/debian/coq.emacsen-startup b/distrib/debian/coq.emacsen-startup index d5cd0ae1f..91b569152 100644 --- a/distrib/debian/coq.emacsen-startup +++ b/distrib/debian/coq.emacsen-startup @@ -16,8 +16,6 @@ (symbol-name flavor) "/site-lisp/coq") load-path)) -(autoload 'coq-mode "coq" "Coq major mode" t) +(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) -(setq-default auto-mode-alist - (cons '("\\.v" . coq-mode) - auto-mode-alist)) |