From 1729cf9def36f907dc6b2f601bed957de8d82b5b Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Mon, 24 Dec 2018 15:17:35 -0500 Subject: Stop distributing CoqIDE CoqIDE currently requires gtksourceview2, which has been removed from Debian (see https://bugs.debian.org/885677). Upstream has an active pull request to update to gtksourceview3 (https://github.com/coq/coq/pull/9279), and it looks like Debian may ship gtksourceview2 with buster anyway, so this is likely to be a temporary change. --- debian/coqide.1 | 166 -------------------------------------------------------- 1 file changed, 166 deletions(-) delete mode 100644 debian/coqide.1 (limited to 'debian/coqide.1') diff --git a/debian/coqide.1 b/debian/coqide.1 deleted file mode 100644 index 20379ef4..00000000 --- a/debian/coqide.1 +++ /dev/null @@ -1,166 +0,0 @@ -.TH COQIDE 1 "July 16, 2004" - -.SH NAME -coqide \- The Coq Proof Assistant graphical interface - - -.SH SYNOPSIS -.B coqide -[ -.B options -] - -.SH DESCRIPTION - -.B coqtop -is a gtk graphical interface for the Coq proof assistant. - -For command-line-oriented use of Coq, see -.BR coqide (1) -; for batch-oriented use of Coq, see -.BR coqc (1). - - -.SH OPTIONS - -.TP -.B \-h -Show the complete list of options accepted by -.BR coqide . -.TP -.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 coqtop (1), -.BR coq-tex (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual, -.I -The Coq web site: http://coq.inria.fr, -.I -/usr/share/doc/coqide/FAQ. - -.SH AUTHOR -This manual page was written by Samuel Mimram , -for the Debian project (but may be used by others). -- cgit v1.2.3