summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-17 23:41:17 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-17 23:41:17 +0000
commit04c838a604255c8b79425b731daa006047275da5 (patch)
treec3f0a5f3d2ef3e9559067d7ab95ed4fb25720443 /debian
parent97cc3f9bb7f50a9d38494b3a4c5fa78384f1cf79 (diff)
Try to build in opt, ready for dpatch, manpages added (but not used yet).
Diffstat (limited to 'debian')
-rw-r--r--debian/changelog7
-rw-r--r--debian/control4
-rw-r--r--debian/coq-interface.1154
-rw-r--r--debian/coq_makefile.196
-rw-r--r--debian/coqc.1172
-rw-r--r--debian/coqide.12
-rw-r--r--debian/coqmktop.170
-rw-r--r--debian/coqtop.1155
-rw-r--r--debian/patches/00list0
-rwxr-xr-xdebian/rules24
10 files changed, 671 insertions, 13 deletions
diff --git a/debian/changelog b/debian/changelog
index b610546e..0f8ef5a2 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+coq (8.0pl1-1) unstable; urgency=low
+
+ * At least the version without QPL-licensed files is out,
+ closes: #230356, #250497.
+
+ -- Samuel Mimram <samuel.mimram@ens-lyon.org> Sun, 18 Jul 2004 01:10:24 +0200
+
coq (8.0-1) unstable; urgency=low
* New upstream release.
diff --git a/debian/control b/debian/control
index f9e0e8b3..c4ce8e17 100644
--- a/debian/control
+++ b/debian/control
@@ -4,7 +4,7 @@ Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Jerome Marant <jerome@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>
Standards-Version: 3.6.1
-Build-Depends: debhelper (>= 4.0.0), ocaml-3.07, ocaml-best-compilers, liblablgtk2-ocaml-dev
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-3.07, ocaml-best-compilers, liblablgtk2-ocaml-dev
Package: coq
Architecture: any
@@ -26,7 +26,7 @@ Description: Proof assistant for higher-order logic
Package: coqide
Architecture: any
-Depends: coq (>= 8.0), ${shlibs:Depends}
+Depends: coq (>= 8.0), liblablgtk2-ocaml, ${shlibs:Depends}
Description: 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
diff --git a/debian/coq-interface.1 b/debian/coq-interface.1
new file mode 100644
index 00000000..73e6eaa6
--- /dev/null
+++ b/debian/coq-interface.1
@@ -0,0 +1,154 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq-interface \-
+
+
+.SH SYNOPSIS
+.B coq-interface
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coq-interface
+is a Coq customized toplevel system for Coq containing some modules
+useful for the graphical interface. This program is not for the casual
+user.
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Help. Will give you the complete list of options accepted by
+coq-interface (the same as coqtop).
+.BI \-I\ dir ,\ \-include\ dir
+Add directory dir in the include path.
+.TP
+.BI \-R\ dir\ coqdir
+Recursively map physical
+.I dir
+to logical
+.IR coqdir .
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.BI \-is\ f ,\ \-inputstate\ f
+Read state from
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\ f
+Write state in file
+.IR f .coq.
+.TP
+.BI \-load\-ml\-object\ f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\ f
+Load ML file
+.IR f .
+.TP
+.BI \-l\ f ,\ \-load\-vernac\-source\ f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\ f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\ f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.TP
+.BI \-compile\ f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\ f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR -batch ).
+.TP
+.B \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B -v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\ f
+Set the rcfile to
+.IR f .
+.TP
+.BI \-user\ u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\ f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coqdep (1),
+.BR coqtop (1),
+.BR parser (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/debian/coq_makefile.1 b/debian/coq_makefile.1
new file mode 100644
index 00000000..7890fde1
--- /dev/null
+++ b/debian/coq_makefile.1
@@ -0,0 +1,96 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq_makefile \- The Coq Proof Assistant makefile generator
+
+
+.SH SYNOPSIS
+.B coq_makefile
+[
+.B options
+]
+[
+.I subdirectory
+]
+[
+.I file.v
+]
+[
+.I file.ml
+]
+
+.SH DESCRIPTION
+
+.B coq_makefile
+is a makefile generator for Coq proof developments.
+
+.SH OPTIONS
+
+.TP
+.I subdirectory
+Subdirectory that should be "made".
+.TP
+.I file.v
+Coq file to be compiled.
+.TP
+.I file.ml
+ML file to be compiled.
+.TP
+.B \-h,\ \-\-help
+Will give you a description of the whole list of options of
+.BR coq_makefile .
+.TP
+.BI \-custom\ command\ dependencies\ file
+Add target
+.I file
+with command
+.I command
+and dependencies
+.I dependencies.
+.TP
+.BI \-I dir
+Look for dependencies in
+.IR dir .
+.TP
+.BI \-R\ physicalpath\ logicalpath
+Look for dependencies recursively starting from.
+.IR physicalpath .
+The logical path associated to the physical path is
+.IR logicalpath .
+.TP
+.IB VARIABLE\ =\ value
+Add the variable definition "VARIABLE=value".
+.TP
+.B \-byte
+Compile with byte-code version of
+.BR coq (1).
+.TP
+.B \-opt
+Compile with native-code version of
+.BR coq (1).
+.TP
+.B \-impredicative\-set
+Compile with option
+.B \-impredicative\-set
+of
+.BR coq (1).
+.TP
+.B
+.BI \-f\ file
+Take the contents of file as arguments.
+.TP
+.BI \-o\ file
+Output should go in file
+.IR file .
+
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqtc (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/debian/coqc.1 b/debian/coqc.1
new file mode 100644
index 00000000..baa04a88
--- /dev/null
+++ b/debian/coqc.1
@@ -0,0 +1,172 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqc \- The Coq Proof Assistant compiler
+
+
+.SH SYNOPSIS
+.B coqc
+[
+.B general \ Coq \ options
+]
+.I file
+
+
+.SH DESCRIPTION
+
+.B coqc
+is the batch compiler for the Coq Proof Assistant.
+The options are basically the same as coqtop(1).
+.IR file.v \&
+is the vernacular file to compile.
+.IR file \&
+must be formed
+only with the characters `a` to `Z`, `0`-`9` or `_` and must begin
+with a letter.
+The compiler produces an object file
+.IR file.vo \&.
+
+For interactive use of Coq, see
+.BR coqtop(1).
+
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Show the whole list of options of coqc and coqtop.
+.TP
+.B \-verbose
+Compile verbosely.
+.TP
+.BI \-image\ f
+Specify an alternative executable for Coq.
+.TP
+.B \-t
+Keep temporary files.
+.TP
+.BI \-I\ dir ,\ \-include\ dir
+Add directory dir in the include path.
+.TP
+.BI \-R\ dir\ coqdir
+Recursively map physical dir to logical coqdir.
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.BI \-is\ f ,\ \-inputstate\ f
+Read state from file
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\ f
+Write state in file
+.IR f .coq.
+.TP
+.BR \-load\-ml\-object\ f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\ f
+Load ML file
+.IR f .
+.TP
+.BI \-l\ f ,\ \-load\-vernac\-source\ f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\ f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\ f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.TP
+.BI \-compile\ f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\ f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.B \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B \-v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\ f
+Set the rcfile to
+.IR f .
+.TP
+.BI \-user\ u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\ f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coq_makefile (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/debian/coqide.1 b/debian/coqide.1
index 35a78c79..20379ef4 100644
--- a/debian/coqide.1
+++ b/debian/coqide.1
@@ -25,7 +25,7 @@ For command-line-oriented use of Coq, see
.TP
.B \-h
-Get the complete list of options accepted by
+Show the complete list of options accepted by
.BR coqide .
.TP
.BI \-I\ dir ,\ \-include\ dir
diff --git a/debian/coqmktop.1 b/debian/coqmktop.1
new file mode 100644
index 00000000..a35e436a
--- /dev/null
+++ b/debian/coqmktop.1
@@ -0,0 +1,70 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqmktop \- The Coq Proof Assistant user-tactics linker
+
+
+.SH SYNOPSIS
+.B coqmktop
+[
+.I options
+]
+.I files
+
+
+.SH DESCRIPTION
+
+.B coqmktop
+builds a new Coq toplevel extended with user-tactics.
+.IR files \&
+are the Objective Caml object or library files (i.e. with suffix .cmo,
+.cmx, .cma or .cmxa) to link with the Coq system.
+The linker produces an executable Coq toplevel which can be called
+directly or through coqc(1), using the -image option.
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Show a list of the available options.
+.TP
+.BI \-srcdir\ dir
+Specify where the Coq source files are.
+.TP
+.BI \-o\ exec\-fil
+Specify the name of the resulting toplevel.
+.TP
+.B \-opt
+Compile in native code.
+.TP
+.B \-full
+Link high level tactics.
+.TP
+.B \-top
+Build Coq on a ocaml toplevel (incompatible with
+.BR \-opt ).
+.TP
+.B \-searchisos
+Build a toplevel for SearchIsos.
+.TP
+.B \-ide
+Build a toplevel for the Coq IDE.
+.TP
+.BI \-R\ dir
+Specify recursively directories for Ocaml.
+.TP
+.B \-v8
+Link with V8 grammar.
+
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR ocamlmktop (1).
+.BR ocamlc (1).
+.BR ocamlopt (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/debian/coqtop.1 b/debian/coqtop.1
new file mode 100644
index 00000000..b136a68b
--- /dev/null
+++ b/debian/coqtop.1
@@ -0,0 +1,155 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coqtop \- The Coq Proof Assistant toplevel system
+
+
+.SH SYNOPSIS
+.B coqtop
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is the toplevel system of Coq, for interactive use.
+It reads phrases on the standard input, and prints results on the
+standard output.
+
+For batch-oriented use of Coq, see
+.BR coqc (1).
+
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Show the complete list of options accepted by coqtop.
+.TP
+.BI \-I\ dir ,\ \-include\ dir
+Add directory dir in the include path.
+.TP
+.BI \-R\ dir\ coqdir
+Recursively map physical dir to logical coqdir.
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.BI \-is\ f ,\ \-inputstate\ f
+Read state from file
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\ f
+Write state in file
+.IR f .coq.
+.TP
+.BR \-load\-ml\-object\ f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\ f
+Load ML file
+.IR f .
+.TP
+.BI \-l\ f ,\ \-load\-vernac\-source\ f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\ f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\ f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.TP
+.BI \-compile\ f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\ f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.B \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B \-v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\ f
+Set the rcfile to
+.IR f .
+.TP
+.BI \-user\ u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\ f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coq-tex (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/debian/patches/00list b/debian/patches/00list
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/debian/patches/00list
diff --git a/debian/rules b/debian/rules
index beb3d42c..27b02b62 100755
--- a/debian/rules
+++ b/debian/rules
@@ -1,6 +1,9 @@
#!/usr/bin/make -f
# debian/rules for coq
+# We want to use dpatch.
+include /usr/share/dpatch/dpatch.make
+
COQPREF=$(CURDIR)/debian/tmp
ADDPREF=COQINSTALLPREFIX=$(COQPREF)
@@ -21,29 +24,30 @@ configure-stamp: patch
if [ `arch` = ppc ] ; then ./configure $(CONFIGUREOPTS) ; fi
touch configure-stamp
-build: configure-stamp build-stamp
+build: patch-stamp configure-stamp build-stamp
build-stamp:
dh_testdir
+# if grep -q BEST=opt config/Makefile; \
+# then ($(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
+# && $(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
+# && $(MAKEQ) bin/coqtop.opt bin/coqtop \
+# && $(MAKEQ) states \
+# && $(MAKEQ) world ) \
if grep -q BEST=opt config/Makefile; \
- then ($(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
- && $(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
- && $(MAKEQ) bin/coqtop.opt bin/coqtop \
- && $(MAKEQ) states \
- && $(MAKEQ) world ) \
- || (echo WARNING: NATIVE CODE COMPILATION FAILED \
- && echo Trying to build coq in bytecode \
+ then ($(MAKE) world) \
+ || (echo WARNING: NATIVE CODE COMPILATION FAILED \
+ && echo Trying to build coq in bytecode instead \
&& $(MAKE) archclean clean \
&& $(MAKE) BEST=byte world \
&& echo NATIVE CODE COMPILATION FAILED \
&& echo Coq was built in bytecode instead); \
else $(MAKE) world; \
fi
- $(MAKE) world
touch test-suite/success/debian.v8
$(MAKE) check
touch build-stamp
-clean:
+clean: unpatch
dh_testdir
dh_testroot
rm -f build-stamp configure-stamp