From 04c838a604255c8b79425b731daa006047275da5 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 17 Jul 2004 23:41:17 +0000 Subject: Try to build in opt, ready for dpatch, manpages added (but not used yet). --- debian/changelog | 7 ++ debian/control | 4 +- debian/coq-interface.1 | 154 +++++++++++++++++++++++++++++++++++++++++++ debian/coq_makefile.1 | 96 +++++++++++++++++++++++++++ debian/coqc.1 | 172 +++++++++++++++++++++++++++++++++++++++++++++++++ debian/coqide.1 | 2 +- debian/coqmktop.1 | 70 ++++++++++++++++++++ debian/coqtop.1 | 155 ++++++++++++++++++++++++++++++++++++++++++++ debian/patches/00list | 0 debian/rules | 24 ++++--- 10 files changed, 671 insertions(+), 13 deletions(-) create mode 100644 debian/coq-interface.1 create mode 100644 debian/coq_makefile.1 create mode 100644 debian/coqc.1 create mode 100644 debian/coqmktop.1 create mode 100644 debian/coqtop.1 create mode 100644 debian/patches/00list 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 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 Uploaders: Ralf Treinen , Sven Luther , Jerome Marant , Remi Vanicat , Stefano Zacchiroli 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 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 -- cgit v1.2.3