Suppression du répertoire distrib: il fait désormais partie du projet coq-dev-tools sur GForge

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

10 files changed, 0 insertions, 367 deletions

diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian
deleted file mode 100644
index bb65ad1979..0000000000
--- a/distrib/debian/README.Debian
+++ /dev/null
@@ -1,27 +0,0 @@
-Coq package for Debian
-----------------------
-
-Note that all bytecode files in this package need to be left
-'unstripped' after compiling. The reason is the following:
-
-  It is possible to strip the .out corresponding to ocaml code compiled in
-  native code (and it is done in Coq (coqopt.out) When compiling in
-  byte-code, the Coq system uses the -custom option in order to get an
-  autonomous executable (running independently of an ocaml implementation on
-  your computer). The way it works is that the .out file is composed of the
-  executable of the byte-code interpreter plus the byte-code for your own
-  program which is stored in the symbol table zone...  stripping such an
-  executable, just remove your byte-code and consequentely cannot run
-  properly.
-
-Moreover the bytecode version is installed even on platforms having a
-native version as the dynamic loading of tactics works only with the
-bytecode version.
-
-For interactive use of coqtop, we suggest
-- either the Debian cle package
-- or the Proof-General (x)emacs mode, provided in the proofgeneral-coq
-  Debian package.
-
-
-
diff --git a/distrib/debian/changelog b/distrib/debian/changelog
deleted file mode 100644
index 727d5264c4..0000000000
--- a/distrib/debian/changelog
+++ /dev/null
@@ -1,132 +0,0 @@
-coq (7.4-1) unstable; urgency=low
-
-  * New upstream version.
-  * Should now build native on ppc (ocaml bug being fixed)
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 25 Jun 2003 09:49:06 +0200
-
-coq (7.3.1-1) unstable; urgency=low
-
-  * New bugfix upstream version.
-  * Proof General is now Recommended since he has been freed (closes:
-    Bug#162894).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Mon,  7 Oct 2002 12:34:03 +0200
-
-coq (7.3-1) unstable; urgency=low
-
-  * New upstream version.
- 
- -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 22 May 2002 14:48:21 +0200
-
-coq (7.2-9) unstable; urgency=low
-  * ocamlc.opt completely broken on powerpc. Added a special case in
-    "rules" for using only bytecode.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri, 15 Feb 2002 09:17:20 +0100
-
-coq (7.2-8) unstable; urgency=low
-
-  * "timeout" time is now 5300s (< 90 min).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Thu, 14 Feb 2002 17:38:06 +0100
-
-coq (7.2-7) unstable; urgency=low
-
-  * Build now uses ocamlc.opt and ocamlopt.opt if available.
-  * Dependency forced on ocaml >= 3.04 (dependency ocaml >=3.04 | camlp4
-    does not make buildd happy. See http://buildd.debian.org/fetch.php?
-    &pkg=coq&ver=7.2-5&arch=arm&stamp=1013388706&file=log&as=raw).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Tue, 12 Feb 2002 09:10:01 +0100
-
-coq (7.2-6) unstable; urgency=low
-
-  * Typo in rules, which made the build process always build in
-    bytecode. Fixed.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Mon, 11 Feb 2002 11:22:21 +0100
-
-coq (7.2-5) unstable; urgency=low
-
-  * Pb with timeout, used in 7.2-4 (bug 132927) making the build process
-    fail when compilation in native mode fails. Workaround in rules: after
-    a "timeout ... make ..." we try a "make -q" to check that everything
-    has been done correctly.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  8 Feb 2002 10:08:10 +0100
-
-coq (7.2-4) unstable; urgency=low
-  * Native code compilation failed on sparc; coqtop built by ocamlopt
-    entered an infinite loop on powerpc. Fixed (using timeout for powerpc:
-    if coqtop loops, it is rebuild using the bytecode compiler)
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  1 Feb 2002 11:04:25 +0100
-
-coq (7.2-3) unstable; urgency=low
-  * Workaround for problems with buildd/apt trying to install camlp4
-    (closes: Bug#130046).
-  
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Mon, 21 Jan 2002 09:46:16 +0100
-
-coq (7.2-2) unstable; urgency=low
-
-  * Build-Depends now requires camlp4 instead of camlp4 (>=3.01) since
-    camlp4 is a virtual package provided by ocaml >=3.04.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Fri, 11 Jan 2002 11:08:03 +0100
-
-coq (7.2-1) unstable; urgency=low
-  * New upstream version.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Wed,  9 Jan 2002 14:02:42 +0100
-
-coq (7.1-2) unstable; urgency=low
-
-  * Fixed policy problem (conf files).
-  * Trying to compile in bytecode if native code compilation fails
-    (closes: Bug#119714)
-  * Errors raised by the Simpl tactic is an upstream bug and should
-    have been fixed in 7.0 (closes: Bug#74518).
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue, 11 Dec 2001 13:33:15 +0100
-
-coq (7.1-1) unstable; urgency=low
-  * New upstream version.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  25 Sep 2001 16:27:04 +0200
-
-coq (7.0-1) unstable; urgency=low
-  * New maintainer Judicaël Courant <Judicael.Courant@lri.fr>.
-  * New upstream version.
-  * Added Build-Depends (closes: Bug#70273).
-  * Cleaned up dependencies.
-  * Emacs mode installation now follows Emacs policy.
-  * Made compilation non-interactive (closes: Bug#92461).
-  * Added Suggests cle.
-  
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  17 Apr 2001 19:24:34 +0200
-
-coq (6.3.1-3) unstable; urgency=low
-
-  * Patched to allow use of ocaml3.
-
- -- Fernando Sanchez <fer@debian.org>  Fri,  7 Jul 2000 08:05:47 +0200
-
-coq (6.3.1-2) unstable; urgency=low
-
-  * Some changes to allow successful porting of this package:
-  * Added checking for ocamlopt.opt before running ./configure with -opt,
-    and configure without it if it is not present for this architecture.
-  * Added checking for ocamlopt before making world-opt.
-
- -- Fernando Sanchez <fer@debian.org>  Sat, 18 Dec 1999 16:45:01 +0100
-
-coq (6.3.1-1) unstable; urgency=low
-
-  * Initial Release.
-
- -- Fernando Sanchez <fer@debian.org>  Fri,  3 Dec 1999 22:06:04 +0100
-
-
diff --git a/distrib/debian/control b/distrib/debian/control
deleted file mode 100644
index cb5c43578f..0000000000
--- a/distrib/debian/control
+++ /dev/null
@@ -1,18 +0,0 @@
-Source: coq
-Section: devel
-Priority: optional
-Maintainer: Judicaël Courant <Judicael.Courant@lri.fr>
-Standards-Version: 3.5.3
-Build-Depends: debhelper (>= 3), timeout, ocaml (>= 3.06)
-
-Package: coq
-Architecture: any
-Depends: ${shlibs:Depends}
-Suggests: coq-doc, ocaml (>= 3.06), cle, ledit
-Recommends: coq-doc, proofgeneral-coq
-Description: a proof assistant for higher-order logic.
- Coq is a proof assistant for higher-order logic, which allows the
- development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
- For more information, see <http://coq.inria.fr/>.
-
diff --git a/distrib/debian/copyright b/distrib/debian/copyright
deleted file mode 100644
index b5d9eadf4c..0000000000
--- a/distrib/debian/copyright
+++ /dev/null
@@ -1,14 +0,0 @@
-This package was debianized by Fernando Sanchez <fer@debian.org>
-
-The "Coq proof assistant" was developed conjointly by
-        INRIA (since 1985),
-        Laboratoire de l'Informatique du Parallelisme LIP
-        associated to CNRS and ENS Lyon (sept.89-sept.97),
-        Laboratoire de Recherche en Informatique
-        associated to CNRS and Paris 11 (since sept. 97).
-
-The complete list of developpers and contributors can be found in /usr/share/doc/doc/CREDITS.gz
-
-Copyright: the Coq Proof Assistant is distributed under the terms of the GNU Lesser General Public Licence, version 2.1.
-
-See /usr/share/common-licenses/LGPL-2.1
diff --git a/distrib/debian/coq.emacsen-install b/distrib/debian/coq.emacsen-install
deleted file mode 100644
index 1ed8fe4388..0000000000
--- a/distrib/debian/coq.emacsen-install
+++ /dev/null
@@ -1,45 +0,0 @@
-#! /bin/sh -e
-# /usr/lib/emacsen-common/packages/install/coq
-
-# Written by Jim Van Zandt <jrv@vanzandt.mv.com>, borrowing heavily
-# from the install scripts for gettext by Santiago Vila
-# <sanvila@ctv.es> and octave by Dirk Eddelbuettel <edd@debian.org>.
-
-FLAVOR=$1
-PACKAGE=coq
-
-if [ ${FLAVOR} = emacs ]; then exit 0; fi
-
-echo install/${PACKAGE}: Handling install for emacsen flavor ${FLAVOR}
-
-#FLAVORTEST=`echo $FLAVOR | cut -c-6`
-#if [ ${FLAVORTEST} = xemacs ] ; then
-#    SITEFLAG="-no-site-file"
-#else
-#    SITEFLAG="--no-site-file"
-#fi
-FLAGS="${SITEFLAG} -q -batch -l path.el -f batch-byte-compile"
-
-ELDIR=/usr/share/emacs/site-lisp/${PACKAGE}
-ELCDIR=/usr/share/${FLAVOR}/site-lisp/${PACKAGE}
-
-# Install-info-altdir does not actually exist. 
-# Maybe somebody will write it.
-if test -x /usr/sbin/install-info-altdir; then
-    echo install/${PACKAGE}: install Info links for ${FLAVOR}
-    install-info-altdir --quiet --section "" "" --dirname=${FLAVOR} /usr/info/${PACKAGE}.info.gz
-fi
-
-install -m 755 -d ${ELCDIR}
-cd ${ELDIR}
-FILES=`echo *.el`
-cp ${FILES} ${ELCDIR}
-cd ${ELCDIR}
-
-cat << EOF > path.el
-(setq load-path (cons "." load-path) byte-compile-warnings nil)
-EOF
-${FLAVOR} ${FLAGS} ${FILES}
-rm -f *.el path.el
-
-exit 0
diff --git a/distrib/debian/coq.emacsen-remove b/distrib/debian/coq.emacsen-remove
deleted file mode 100644
index 02b6392ce2..0000000000
--- a/distrib/debian/coq.emacsen-remove
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/sh -e
-# /usr/lib/emacsen-common/packages/remove/coq
-
-FLAVOR=$1
-PACKAGE=coq
-
-if [ ${FLAVOR} != emacs ]; then
-    if test -x /usr/sbin/install-info-altdir; then
-        echo remove/${PACKAGE}: removing Info links for ${FLAVOR}
-        install-info-altdir --quiet --remove --dirname=${FLAVOR} /usr/info/coq.info.gz
-    fi
-
-    echo remove/${PACKAGE}: purging byte-compiled files for ${FLAVOR}
-    rm -rf /usr/share/${FLAVOR}/site-lisp/${PACKAGE}
-fi
diff --git a/distrib/debian/coq.emacsen-startup b/distrib/debian/coq.emacsen-startup
deleted file mode 100644
index 91b5691522..0000000000
--- a/distrib/debian/coq.emacsen-startup
+++ /dev/null
@@ -1,21 +0,0 @@
-;; -*-emacs-lisp-*-
-;;
-;; Emacs startup file for the Debian GNU/Linux coq package
-;;
-;; Originally contributed by Nils Naumann <naumann@unileoben.ac.at>
-;; Modified by Dirk Eddelbuettel <edd@debian.org>
-;; Adapted for dh-make by Jim Van Zandt <jrv@vanzandt.mv.com>
-
-;; The coq package follows the Debian/GNU Linux 'emacsen' policy and
-;; byte-compiles its elisp files for each 'emacs flavor' (emacs19,
-;; xemacs19, emacs20, xemacs20...).  The compiled code is then
-;; installed in a subdirectory of the respective site-lisp directory.
-;; We have to add this to the load-path:
-
-(setq load-path (cons (concat "/usr/share/"
-                              (symbol-name flavor)
-			      "/site-lisp/coq") load-path))
-
-(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
-
diff --git a/distrib/debian/dirs b/distrib/debian/dirs
deleted file mode 100644
index 38a404b552..0000000000
--- a/distrib/debian/dirs
+++ /dev/null
@@ -1,3 +0,0 @@
-usr/bin
-usr/lib
-usr/lib/coq
diff --git a/distrib/debian/docs b/distrib/debian/docs
deleted file mode 100644
index 62998f27c7..0000000000
--- a/distrib/debian/docs
+++ /dev/null
@@ -1,3 +0,0 @@
-README
-CREDITS
-CHANGES
diff --git a/distrib/debian/rules b/distrib/debian/rules
deleted file mode 100755
index d4e1d33768..0000000000
--- a/distrib/debian/rules
+++ /dev/null
@@ -1,89 +0,0 @@
-#!/usr/bin/make -f
-
-export DH_COMPAT=3
-
-COQPREF=$(CURDIR)/debian/coq
-ADDPREF=COQINSTALLPREFIX=${COQPREF}
-
-# in version 3.04, ocamlopt has several bugs: on some arches, it produces
-# executables that sometimes fail mysteriously or loop.
-# We use a workaround to detect this kind of situations:
-# - we try to make Coq with timeouts (TMAKE)
-# - once this is done, we check make succeeded (timeout does not
-# return the exit status of MAKE)
-#
-TMAKE=timeout 5300 ${MAKE}
-MAKEQ=${MAKE} -q
-
-CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all
-
-configure: configure-stamp
-configure-stamp:
-	dh_testdir
-	./configure -opt ${CONFIGUREOPTS} || ./configure ${CONFIGUREOPTS}
-	touch configure-stamp
-
-build: configure-stamp build-stamp
-build-stamp:
-	dh_testdir
-	if grep -q BEST=opt config/Makefile; \
-	then (${TMAKE} bin/coqmktop bin/coqc bin/coqtop.byte \
-	      && ${MAKEQ} bin/coqmktop bin/coqc bin/coqtop.byte \
-	      && ${TMAKE} bin/coqtop.opt bin/coqtop \
-	      && ${MAKEQ} bin/coqtop.opt bin/coqtop \
-	      && ${TMAKE} states \
-	      && ${MAKEQ} states \
-	      && ${TMAKE} world \
-	      && ${MAKEQ} world) \
-          ||  (echo WARNING: NATIVE CODE COMPILATION FAILED \
-	    && echo Trying to build coq in bytecode \
-	    && ${MAKE} archclean clean \
-	    && ${MAKE} BEST=byte world \
-	    && echo NATIVE CODE COMPILATION FAILED \
-	    && echo Coq was built in bytecode instead); \
-	else ${MAKE} world; \
-	fi
-	${MAKE} check
-	touch build-stamp
-
-clean:
-	dh_testdir
-	dh_testroot
-	rm -f build-stamp configure-stamp
-
-	-$(MAKE) clean
-	-$(MAKE) archclean
-
-	dh_clean
-
-install: build
-	dh_testdir
-	dh_testroot
-	dh_clean -k
-	dh_installdirs
-
-	$(MAKE) ${ADDPREF} install || $(MAKE) BEST=byte ${ADDPREF} install
-	-strip -R .note -R .comment ${COQPREF}/usr/bin/coqtop.opt
-
-# Build architecture-independent files here.
-binary-indep: build install
-# We have nothing to do by default.
-
-# Build architecture-dependent files here.
-binary-arch: build install
-	dh_testdir
-	dh_testroot
-	dh_installdocs
-	dh_installemacsen
-	dh_installchangelogs CHANGES
-	dh_link
-	dh_compress
-	dh_fixperms
-	dh_installdeb
-	dh_shlibdeps
-	dh_gencontrol
-	dh_md5sums
-	dh_builddeb
-
-binary: binary-indep binary-arch
-.PHONY: build clean binary-indep binary-arch binary install configure