From c75e037b3c265ef517eb1152f44e9613a9a4087a Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 2 Dec 2015 17:37:10 -0500 Subject: [PATCH] doc(emacs/README.md): mention issue 906 in Known Issues see #906 [skip ci] --- src/emacs/README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/emacs/README.md b/src/emacs/README.md index 5d72e2dbe..ac6e81ae8 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -187,6 +187,15 @@ You may also need to install [emacs-unicode-fonts](https://github.com/rolandwalk (unicode-fonts-setup) ``` +"Variable binding depth exceeds max-specpdl-size" Error +--------------------------------------------------------- + +See [Issue 906](https://github.com/leanprover/lean/issues/906) for details. +[Moritz Kiefer](https://github.com/cocreature) reported that `proofgeneral` +comes with an old version of `mmm-mode` (0.4.8, released in 2004) on ArchLinux +and it caused this problem. Either removing `proofgeneral` or upgrading +`mmm-mode` to the latest version (0.5.1 as of 2015 Dec) resolves this issue. + Contributions =============