diff options
Diffstat (limited to 'distrib/debian')
| -rw-r--r-- | distrib/debian/README.Debian | 16 | ||||
| -rw-r--r-- | distrib/debian/changelog | 34 | ||||
| -rw-r--r-- | distrib/debian/control | 15 | ||||
| -rw-r--r-- | distrib/debian/copyright | 72 | ||||
| -rw-r--r-- | distrib/debian/coq.emacsen-install | 45 | ||||
| -rw-r--r-- | distrib/debian/coq.emacsen-remove | 15 | ||||
| -rw-r--r-- | distrib/debian/coq.emacsen-startup | 18 | ||||
| -rw-r--r-- | distrib/debian/dirs | 3 | ||||
| -rw-r--r-- | distrib/debian/docs | 2 | ||||
| -rwxr-xr-x | distrib/debian/rules | 85 |
10 files changed, 305 insertions, 0 deletions
diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian new file mode 100644 index 000000000..7dc4ee03d --- /dev/null +++ b/distrib/debian/README.Debian @@ -0,0 +1,16 @@ +Coq package for Debian +---------------------- + +As an unusual thing, some files (*.out) in this package need to be left +'unstripped' after compiling. The reason, as explained by the authors, 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. diff --git a/distrib/debian/changelog b/distrib/debian/changelog new file mode 100644 index 000000000..789b524e6 --- /dev/null +++ b/distrib/debian/changelog @@ -0,0 +1,34 @@ +coq (7.0.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. + * Made compilation non-interactive (closes: Bug#92461). + + + -- 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 + +Local variables: +mode: debian-changelog +End: diff --git a/distrib/debian/control b/distrib/debian/control new file mode 100644 index 000000000..c36ceaa98 --- /dev/null +++ b/distrib/debian/control @@ -0,0 +1,15 @@ +Source: coq +Section: devel +Priority: optional +Maintainer: Judicaël Courant <Judicael.Courant@lri.fr> +Standards-Version: 3.0.1 +Build-Depends: debhelper (>= 2), ocaml (>= 3.00-1), camlp4 (>= 3.00-1) + +Package: coq +Architecture: any +Depends: ${shlibs:Depends} +Suggests: coq-doc, ocaml (>= 3.00-1), camlp4 (>= 3.00-1) +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. diff --git a/distrib/debian/copyright b/distrib/debian/copyright new file mode 100644 index 000000000..88eafcc0b --- /dev/null +++ b/distrib/debian/copyright @@ -0,0 +1,72 @@ +This package was debianized by Fernando Sanchez <fer@debian.org> on +Fri, 3 Dec 1999 22:06:04 +0100. + +It was downloaded from ftp://ftp.inria.fr/INRIA/coq + +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 following people have contributed to the core of the system +during the indicated time : + + Bruno Barras, (INRIA, 1995-1999) + Cristina Cornes, (INRIA, 1993-1996) + David Delahaye, (INRIA, 1997-1999) + Daniel de Rauglaudre, (INRIA, 1996-1998) + Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-1999) + Eduardo Giménez, (ENS Lyon, 1993-1996, INRIA, 1997-1998) + Hugo Herbelin, (INRIA, 1996-1999) + Gérard Huet, (INRIA, 1985-1997) + César Muñoz, (INRIA, 1994-1995) + Chetan Murthy, (INRIA, 1992-1994) + Catherine Parent-Vigouroux, (ENS Lyon 1992-1995) + Patrick Loiseleur, (Paris 11, 1997-1999) + Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) + (Paris 11, 1997-1999) + Amokrane Saïbi, (INRIA, 1993-1998) + +The following directories contain independent contributions: +tactics/contrib/eqdecide + developed by Eduardo Gimenez (INRIA, 1997-1998) +tactics/contrib/extraction + developed by Benjamin Werner (INRIA, 1989) + and Jean-Christophe Filliatre (ENS Lyon, 1994-1997) +tactics/contrib/linear + developed by Jean-Christophe Filliatre (ENS Lyon, 1994-1997) +tactics/contrib/natural + developed by Yann Coscoy (INRIA, 1996) +tactics/contrib/omega + developed by Pierre Cregut (CNET-France Telecom, 1996) +tactics/contrib/pcoq + developed by Yves Bertot (INRIA, 1996-1999) +tactics/contrib/polynom + developed by Samuel Boutin (INRIA, 1996) + and Patrick Loiseleur (LRI, 1997-1999) +tactics/programs + developed by Jean-Christophe Filliatre (LRI, 1997-1999) +theories/REALS + developed by Micaela Mayero (INRIA, 1997-1999) +*************************************************************************** +INRIA refers to : + Institute National de la Recherche en Informatique et Automatique +CNRS refers to : + Centre National de la Recherche Scientifique +Paris 11 refers to : + Universite Paris Sud +ENS Lyon refers to : + Ecole Normale Superieure de Lyon +**************************************************************************** + + +Copyright: + +All files of the "Coq proof assistant" in directories or sub-directories of + src, tactics, theories, tools +are distributed under the terms of the GNU Lesser General Public License +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 new file mode 100644 index 000000000..1ed8fe438 --- /dev/null +++ b/distrib/debian/coq.emacsen-install @@ -0,0 +1,45 @@ +#! /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 new file mode 100644 index 000000000..02b6392ce --- /dev/null +++ b/distrib/debian/coq.emacsen-remove @@ -0,0 +1,15 @@ +#!/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 new file mode 100644 index 000000000..d1369ae6c --- /dev/null +++ b/distrib/debian/coq.emacsen-startup @@ -0,0 +1,18 @@ +;; -*-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)) + + diff --git a/distrib/debian/dirs b/distrib/debian/dirs new file mode 100644 index 000000000..38a404b55 --- /dev/null +++ b/distrib/debian/dirs @@ -0,0 +1,3 @@ +usr/bin +usr/lib +usr/lib/coq diff --git a/distrib/debian/docs b/distrib/debian/docs new file mode 100644 index 000000000..9737d93a4 --- /dev/null +++ b/distrib/debian/docs @@ -0,0 +1,2 @@ +INSTALL +README diff --git a/distrib/debian/rules b/distrib/debian/rules new file mode 100755 index 000000000..06927dc3f --- /dev/null +++ b/distrib/debian/rules @@ -0,0 +1,85 @@ +#!/usr/bin/make -f +# Sample debian/rules that uses debhelper. +# GNU copyright 1997 to 1999 by Joey Hess. + +# Uncomment this to turn on verbose mode. +#export DH_VERBOSE=1 + +# This is the debhelper compatability version to use. +export DH_COMPAT=2 + +configure: configure-stamp +configure-stamp: + dh_testdir + # Add here commands to configure the package. + ./configure --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp + + touch configure-stamp + +build: configure-stamp build-stamp +build-stamp: + dh_testdir + + # Add here commands to compile the package. + $(MAKE) -j world + #/usr/bin/docbook-to-man debian/coq.sgml > coq.1 + + touch build-stamp + +clean: + dh_testdir + dh_testroot + rm -f build-stamp configure-stamp + + # Add here commands to clean up after the build process. + -$(MAKE) clean + -$(MAKE) archclean + + dh_clean + +install: build + dh_testdir + dh_testroot + dh_clean -k + dh_installdirs + + # Add here commands to install the package into debian/coq. + $(MAKE) install COQINSTALLPREFIX=$(CURDIR)/debian/coq + + +# 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_installdebconf + dh_installdocs +# dh_installexamples +# dh_installmenu +# dh_installlogrotate + dh_installemacsen +# dh_installpam +# dh_installmime +# dh_installinit +# dh_installcron +# dh_installman coqtop.byte coqtop.opt coqtop coqc coqmktop +# dh_installinfo +# dh_undocumented + dh_installchangelogs CHANGES + dh_link + dh_strip + dh_compress + dh_fixperms +# dh_makeshlibs + dh_installdeb +# dh_perl + dh_shlibdeps + dh_gencontrol + dh_md5sums + dh_builddeb + +binary: binary-indep binary-arch +.PHONY: build clean binary-indep binary-arch binary install configure |