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/README.Debian | 4 +- debian/changelog | 1 + debian/control | 22 +---- debian/coqide.1 | 166 ------------------------------------- debian/coqide.desktop | 8 -- debian/coqide.dirs | 1 - debian/coqide.install | 8 -- debian/coqide.links.in | 2 - debian/libcoq-ocaml-dev.install.in | 1 - debian/not-installed | 3 + debian/rules | 4 +- 11 files changed, 9 insertions(+), 211 deletions(-) delete mode 100644 debian/coqide.1 delete mode 100644 debian/coqide.desktop delete mode 100644 debian/coqide.dirs delete mode 100644 debian/coqide.install delete mode 100644 debian/coqide.links.in create mode 100644 debian/not-installed diff --git a/debian/README.Debian b/debian/README.Debian index 55825cf9..2cadf798 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -17,6 +17,4 @@ For interactive use of coqtop, we suggest - or the Proof-General (x)emacs mode, available in the proofgeneral package. -However, we recommend you to use the CoqIde GTK+ interface provided in coqide. - - -- Stéphane Glondu , Sun, 19 Jan 2014 15:11:59 +0100 + -- Benjamin Barenblat , Mon, 24 Dec 2018 15:11:23 -0500 diff --git a/debian/changelog b/debian/changelog index 25a70fbb..cfed73d4 100644 --- a/debian/changelog +++ b/debian/changelog @@ -3,6 +3,7 @@ coq (8.8.2-1) UNRELEASED; urgency=medium * New upstream release (Closes: #910840) * Add Benjamin Barenblat to uploaders * Update debian/watch for upstream's transition to GitHub (Closes: #902903) + * Stop distributing CoqIDE (Closes: #916369) -- Benjamin Barenblat Mon, 24 Dec 2018 14:56:15 -0500 diff --git a/debian/control b/debian/control index 739bb2aa..5af6c74b 100644 --- a/debian/control +++ b/debian/control @@ -35,7 +35,6 @@ Depends: ocaml-best-compilers, ocaml-findlib Provides: coq-${F:CoqABI} -Recommends: coqide | proofgeneral Suggests: ocaml-nox, proofgeneral, @@ -52,25 +51,8 @@ Description: proof assistant for higher-order logic (toplevel and compiler) . This package provides coqtop, a command line interface to Coq. . - A graphical interface for Coq is provided in the coqide package. - Coq can also be used with ProofGeneral, which allows proofs to be - edited using emacs and xemacs. This requires the proofgeneral - package to be installed. - -Package: coqide -Architecture: any -Depends: - coq (= ${binary:Version}), - ${ocaml:Depends}, - ${shlibs:Depends}, - ${misc:Depends} -Description: proof assistant for higher-order logic (gtk interface) - 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 Camlp5. - . - This package provides CoqIde, a graphical user interface for - developing proofs. + The proofgeneral package allows proofs to be edited using Emacs and + XEmacs. Package: coq-theories Architecture: any 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). diff --git a/debian/coqide.desktop b/debian/coqide.desktop deleted file mode 100644 index ea667c56..00000000 --- a/debian/coqide.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[Desktop Entry] -Name=CoqIDE Proof Assistant -Comment=Graphical interface for the Coq proof assistant -Exec=coqide -Type=Application -Categories=Development;Science;Math;IDE;GTK; -Terminal=false -Icon=coq diff --git a/debian/coqide.dirs b/debian/coqide.dirs deleted file mode 100644 index c1da623a..00000000 --- a/debian/coqide.dirs +++ /dev/null @@ -1 +0,0 @@ -usr/share/pixmaps diff --git a/debian/coqide.install b/debian/coqide.install deleted file mode 100644 index c0189e2d..00000000 --- a/debian/coqide.install +++ /dev/null @@ -1,8 +0,0 @@ -usr/bin/coqide* -usr/share/coq/coq.png -usr/share/coq/*.lang -usr/share/coq/*_style.xml -usr/share/doc/coq/FAQ-CoqIde usr/share/doc/coqide -usr/share/man/man1/coqide* -usr/lib/coq/toploop/coqidetop.* -debian/coqide.desktop usr/share/applications diff --git a/debian/coqide.links.in b/debian/coqide.links.in deleted file mode 100644 index c73095fe..00000000 --- a/debian/coqide.links.in +++ /dev/null @@ -1,2 +0,0 @@ -/usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.byte.1 -OPT: /usr/share/man/man1/coqide.1 /usr/share/man/man1/coqide.opt.1 diff --git a/debian/libcoq-ocaml-dev.install.in b/debian/libcoq-ocaml-dev.install.in index ec726f1f..9ef519ac 100644 --- a/debian/libcoq-ocaml-dev.install.in +++ b/debian/libcoq-ocaml-dev.install.in @@ -3,7 +3,6 @@ usr/share/man/man1/coqmktop* usr/lib/coq/engine/engine.cma usr/lib/coq/grammar/compat5.cmo usr/lib/coq/grammar/grammar.cma -usr/lib/coq/ide/ide.cma usr/lib/coq/interp/interp.cma usr/lib/coq/kernel/kernel.cma usr/lib/coq/lib/clib.cma diff --git a/debian/not-installed b/debian/not-installed new file mode 100644 index 00000000..bfec6ce3 --- /dev/null +++ b/debian/not-installed @@ -0,0 +1,3 @@ +# CoqIDE is temporarily disabled. +usr/share/man/man1/coqide.1 +usr/lib/coq/toploop/coqidetop.cmxs diff --git a/debian/rules b/debian/rules index 5cc70086..58393fb4 100755 --- a/debian/rules +++ b/debian/rules @@ -36,6 +36,7 @@ CONFIGUREOPTS := -arch Linux -prefix /usr -mandir /usr/share/man \ -configdir /etc/xdg/coq \ -emacslib /usr/share/emacs/site-lisp/coq \ -browser "/usr/bin/x-www-browser %s &" \ + -coqide no \ -with-doc no \ -debug \ $(NATIVE_COMPUTE) @@ -101,11 +102,10 @@ override_dh_auto_install: override_dh_install: chmod a-x debian/tmp/usr/lib/coq/toploop/*cma dh_install --fail-missing - cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm .PHONY: override_dh_ocaml override_dh_ocaml: - dh_ocaml --nodefined-map coqide:Xmlprotocol,Ide_slave,Xml_printer,Richprinter,Document,Xml_parser,Xml_lexer,Serialize + dh_ocaml for f in debian/*substvars; do echo $$f; cat $$f; done .PHONY: override_dh_gencontrol -- cgit v1.2.3