summaryrefslogtreecommitdiff
path: root/debian/README.Debian
diff options
context:
space:
mode:
Diffstat (limited to 'debian/README.Debian')
-rw-r--r--debian/README.Debian20
1 files changed, 20 insertions, 0 deletions
diff --git a/debian/README.Debian b/debian/README.Debian
new file mode 100644
index 00000000..2cadf798
--- /dev/null
+++ b/debian/README.Debian
@@ -0,0 +1,20 @@
+--------------------------
++ Coq package for Debian +
+--------------------------
+
+Binary (in)compatibility
+------------------------
+The compiled libraries of Coq (the *.vo) are not expected to be backward or
+forward compatible between releases (including plX releases). In case of a new
+upstream release, your Coq files should be recompiled.
+
+
+Coq frontends
+-------------
+For interactive use of coqtop, we suggest
+ - a readline editor, such as ledit or rlwrap (or anything that provides the
+ readline-editor virtual packages);
+ - or the Proof-General (x)emacs mode, available in the proofgeneral
+ package.
+
+ -- Benjamin Barenblat <bbaren@debian.org>, Mon, 24 Dec 2018 15:11:23 -0500