quality-of-live improvements and default config for EasyCrypt

[chdoc]

In my opinion, the default configuration of ProofGeneral/EasyCrypt has several shortcomings, that should all be easy to fix:

• [ ] electric-indent-mode is enabled by default and IMHO less than useless, because the indentation it creates does not match the (mathcomp-inspired) proof layout used in the libraries and gets even worse when indenting modules and their procedures. So one basically has to undo everything it does.
• [ ] proof-find-theorems-command (i.e. C-c C-f) is undefined and should be set to "search %s.".
• [ ] proof-query-identifier-command (i.e. C-c TAB) is undefined and should be set to "print %s.".
• [ ] easycrypt-Print (i.e. C-c C-a C-p) is set but, unlike in Coq, does not default to the identifier at point (if any).

Note that proof-query-identifier does default to the identifier at point, but requires one to erase the proposed identifier if one wants to query something else. Hence, having a C-c C-a C-p do a coq-style print, defaulting to the identifier at point when the user enters nothing, would be the most comfortable option, in particular for people who use both Coq and EasyCrypt.

[chdoc]

CC: @strub

[monnier]

• [ ] electric-indent-mode is enabled by default and IMHO less than useless, because the indentation it creates does not match the (mathcomp-inspired) proof layout used in the libraries and gets even worse when indenting modules and their procedures. So one basically has to undo everything it does.

The easycrypt major mode should set electric-indent-inhibit then until the auto-indentation code is improved.

Note that proof-query-identifier does default to the identifier at point, but requires one to erase the proposed identifier if one wants to query something else.

Looks like a UI bug, which the patch below should address:

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 005d919e8..a485ae257 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2019  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -915,10 +915,10 @@ a popup with the information in it."
 If called interactively, STRING defaults to the current word near point."
   (interactive
    (list
-    (completing-read "Query identifier: "
-		     nil nil nil
-		     (current-word)
-		     'proof-query-identifier-history)))
+    (let ((def (current-word)))
+      (read-string (if def (format "Query identifier (default %s): " def)
+		     "Query identifier: ")
+		     nil 'proof-query-identifier-history def))))
   (if string (pg-identifier-query string)))
 
 (defun pg-identifier-query (identifier &optional ctxt callback)

-- Stefan

[Matafou]

+1

[strub]

I can try implementing this request, but being totally incompetent in elisp, I might need some help at some point.