Try to build in opt, ready for dpatch, manpages added (but not used yet).

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