summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-24 15:17:35 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-01-03 18:24:14 -0500
commit1729cf9def36f907dc6b2f601bed957de8d82b5b (patch)
treed137c8869f5d02ec762cbf5fbdac0961f2810650
parenta150c4bb3db62e4488ded15e413ccfafe4264bc4 (diff)
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.
-rw-r--r--debian/README.Debian4
-rw-r--r--debian/changelog1
-rw-r--r--debian/control22
-rw-r--r--debian/coqide.1166
-rw-r--r--debian/coqide.desktop8
-rw-r--r--debian/coqide.dirs1
-rw-r--r--debian/coqide.install8
-rw-r--r--debian/coqide.links.in2
-rw-r--r--debian/libcoq-ocaml-dev.install.in1
-rw-r--r--debian/not-installed3
-rwxr-xr-xdebian/rules4
11 files changed, 9 insertions, 211 deletions
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 <glondu@debian.org>, Sun, 19 Jan 2014 15:11:59 +0100
+ -- Benjamin Barenblat <bbaren@debian.org>, 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 <bbaren@debian.org> 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 <samuel.mimram@ens-lyon.org>,
-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