Feedback from Coq Community Survey 2022. #671
Comments
|
Thanks a lot @Zimmi48 for summarizing all this! Very useful feedback |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The Coq Community Survey 2022 contained some questions for Proof General users. Here are the results.
Emacs plugins in use
User satisfaction
Duration of use
Emacs variants
To this question, the other answers were:
Proof General features
Windows usage
Open text questions
A first question was related to Company-Coq and the results were already reported in cpitclaudel/company-coq#258.
To the question "Do you use specific customizations or fixups of Proof General or Company-Coq (in your
~/.emacs)? If yes, briefly speaking, what are these customizations and would you like to have some of them applied by default?", the answers were:Would make better defaults IMO:
proof-follow-mode 'followdown
proof-sticky-errors t
I use the following and it would be nice to have them by default, in decreasing order of importance:
A workaround for Unable to use C-r as redo in evil mode with ProofGeneral and Coq #430
A hack to find and reload the current opam env:
(defun load-opam-env ()
(mapc
(lambda (s)
(let ((r (split-string s "=")))
(setenv (car r) (cadr r))))
(split-string (shell-command-to-string "opam env --shell=bash | sed -e 's/;.*;/;/'")))
)
A custom command to make the main window be 80 characters wide (used with a small screen when the total width is smaller than 160 chars - I'd rather the goal and response buffers be narrower and I also don't like to have them arranged bellow the main window).
I am using the Emacs settings shipped by UniMath, see https://github.com/UniMath/UniMath/blob/master/UniMath/.dir-locals.el.
In particular, UniMath is loading the Agda (!) Unicode input method, which is shipped along with UniMath (https://github.com/UniMath/UniMath/blob/master/emacs/agda/agda-input.el).
Possibly Proof General could include a Unicode input method similar to Agda's? Maybe it does already, in which case I am not aware of it.
UniMath also comes with the very useful
etagsfeature.I've hacked an agda-like input mode for symbols.
I added a command that allows me to switch between different versions of Coq (UniMath, HoTT or standard Coq). This might be useful to be a default command.
I disable the splash screen, set the communication to go through a pipe instead of a PTY because I was running into length limits, and disable
proof-script-next-command-advancewhen using electric terminators.Disable splash screen, unset
coq-one-command-per-line, make syntax-highlighting less insane.No
I like (setq coq-prefer-top-of-conclusion t).
I have a lot of Iris-specific customization which is not relevant to most people.
no
There is a customization that I wrote long time ago and no longer know what it does
Electric terminator disabled, I kwoty triggering it by accident.
integration with undo-tree
Yes.
Here's what I have in my emacs config:
(add-hook 'coq-mode-hook (lambda () (electric-indent-local-mode -1)))
(add-hook 'coq-mode-hook (lambda () (setq show-trailing-whitespace t)))
(setq! proof-three-window-mode-policy 'hybrid)
(setq! coq-one-command-per-line nil)
(setq! proof-splash-enable nil)
(setq! proof-splash-screen t)
(setq! coq-unicode-tokens-enable nil)
(setq! proof-electric-terminator-enable nil)
(setq! proof-next-command-insert-space nil)
(setq! PA-one-command-per-line nil)
(setq! PA-script-indent nil)
I invoke opam to find out about local switches and select the right version of Coq for a given project
'(coq-indent-modulestart 0) ;; Hope this becomes default
'(safe-local-variable-values ;; Set by QuickChick automatically, but forgot what it's for
'((eval progn
(make-local-variable 'coq-prog-args)
(setq coq-prog-args
`("-emacs" "-R" ,(expand-file-name
(locate-dominating-file buffer-file-name ".dir-locals.el"))
"QuickChick")))))
Iris related symbols identation
I use electric mode for parentheses, printing of line numbers (even though it's badly rendered in emacs). I also turn off auto indent because it's terrible with Coq.
Finally I remove trailing spaces on save, except that it sometimes reverts compilation with PG.
I'm not used to using letters (n/p/f/b) to navigate, so I did my keybindings closer to what can be seen in CoqIDE:
C-↑ : previous (proof-undo-last-successful-command)
C-↓ : next (proof-assert-next-command-interactive)
C-c ↑ : retract to the top (proof-retract-buffer)
C-c ↓ : do all (proof-process-buffer)
C-c → : go here (proof-goto-point)
You can't put that by default, since (n/p/f/b) is the Emacs way to navigate.
But having some kind of "CoqIDE navigation mode" option using arrows could be more beginner friendly.
I have a list of modified keywords for SSReflect that Assia made a while ago (2007). I am pretty sure most of them are outdated or have been incorporated in the main distribution, but I am lazy to try...
The three-windows mode should be enabled by default, to my humble opinion.
I disable all forms of "electric-indent-mode", please disable by default, so that one doesn't need to tell every new user how to disable it..
theme config (I use emacs with a dark theme)
My customizations are minimal. The most important tweak I do is setting proof-follow-mode to ‘followdown. I wish this was the default. I also set coq-indent-semicolon-tactical to 0, and coq-smie-after-bolp-indentation to 0 as well. These are personal preferences, so I don’t think they should be applied by default.
Integration with evil mode. Shorter shortcuts.
I set
(setq proof-script-fly-past-comments t)in order to deactivate the evaluation of comments. When I open some file with a lot of comments (for instance, tutorials), I like to skip the evaluation of the comments and just evaluate the commands.(setq proof-follow-mode 'followdown) should be default.
Disable the very ugly toolbar.
(setq overlay-arrow-string nil) ; otherwise, the first two chars of the current line are hidden in emacs -nw
'(proof-locked-face ((t (:background "color-33"))))
'(proof-queue-face ((t (:background "color-70"))))
'(proof-tactics-name-face ((t (:foreground "color-27"))))
; the defaults with white foreground are unusable
'(coq-indent-modulestart 0)
'(coq-indent-proofstart 0)
Proper indentation for ssreflect tactics
I disabled the splash screen.
Yes. I enable additional Unicode substitutions and customize the keybindings to integrate better with spacemacs.
I created easier keystrokes for moving forward, back and to "here": SHIFT-PgDn, SHIFT-PgUp and SHIFT-RET.
(define-key coq-mode-map (kbd "S-RET") 'proof-goto-point) ; shift-RET
(define-key coq-mode-map (kbd "S-") 'proof-assert-next-command-interactive); shift-PageDown
(define-key coq-mode-map (kbd "S-") 'proof-undo-last-successful-command); shift-PageUp
Automatically use Coq from a particular opam switch for a certain project.
None
No, I don't.
(setq coq-highlight-hyps-cited-in-response nil)
Had to patch doom and disable magic indentation detector
I've disabled electric-indent-mode for coq.
I have mainly applied general changes not specifically for Coq. Below are some customisations that I used in my .emacs file. The first 4 had an impact on my use of Coq.
;; see matching pairs of parentheses and other characters
;; when point is on one of the paired characters, the other is highlighted
(show-paren-mode 1)
;; Coq: it was useful to inspect a term from the goal and modify it
;; rebind C-x o to M-o
(global-set-key (kbd "M-o") 'other-window)
;; Coq: it was easier to navigate through the Coq windows and other frames, in order to copy/search something
;; rebind C-c s to coq-SearchConstant when in coq-mode mode
;; (eval-after-load 'coq-mode
;; '(define-key coq-keymap (kbd "C-c s") 'coq-SearchConstant))
;; Coq: it was before 2019
;; add hook to coq-mode-hook
(add-hook 'coq-mode-hook (lambda () (local-set-key (kbd "C-c RET") 'proof-goto-point)))
(add-hook 'coq-mode-hook (lambda () (local-set-key (kbd "C-c C-s") 'coq-SearchConstant)))
(custom-set-faces
;; custom-set-faces was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
)
;; Coq: it was before 2019
;; re-open files I had open before
(desktop-save-mode 1)
;; display column number in the mode line
(setq column-number-mode t)
;; default to better frame titles
(setq frame-title-format
(concat "%b - emacs@" system-name))
;; set delay before showing a matching parenthesis to 0
(setq show-paren-delay 0)
(custom-set-variables
'(proof-splash-enable nil))
;; Proof General: don't print '=>' over source code to show next command to process
(setq overlay-arrow-string "")
;; Don't show Emacs startup screen
(setq inhibit-startup-screen t)
Disable splash screen, clear out the abbrev-mode table, mark underscore as a part of a word. I would love to see all of these applied by default.
(setq proof-splash-enable nil)
(setq coq-mode-abbrev-table '())
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?_ "w")))
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?' "w")))
Custom key shortcuts related to script interpretation (but I don't remember which ones specifically)
I have some code to list OPAM switches that have coq installed, and switch Proof General between them. But it slows down my emacs startup considerably, because
opam config list --safe coqhas to be run for each switch, and it's pretty slow(define-key-lazy coq-mode-map (kbd "M-") 'proof-goto-point)
The current keybinding are harmful
I deactivate any kind of electric mode.
I seem to have modified some of the faces to better fit with my default theme.
I disable proof-splash-enable.
The last question was "What improvements, bug fixes and new features would you most like to see in Proof General?". The answers were:
async proof checking support
Multiple coq instances in the same emacs process
The central relevant feature keeping me from using PG all the time is parallel proof processing
Some QoL when building using dune could be appreciable: currently, afaiw, we need to use a _CoqProject pointing into the _build folder explicitly rather than pointing at the sources. It also interacts badly with "require before compile".
Automatic indentation doesn't really work with the MathComp proof style (cf. https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#indentation-in-proof-scripts), which is annoying.
I would like for it to work more like a proper IDE (as in integrated with something which CoqIDE is not, for instance). Mouseover terms to see their type (like regular IDEs). Quality of life things.
The layout of the 2 or 3 windows is often messed up and needs to be reinstated manually.
Ability to process multiple.v files at the same time like in CoqIDE.
The indentation of ssreflect code in conjunction with bullets is really messed up! Sometimes it indents way into the middle and I don't know why. Usually involves a "by" tactical.
Support for elpi
None
Well
proof-omit-proofs-optionwas one of them, but that already exists.I often need to debug a broken proof and setting up two instances of Proof General for the old and new code is quite annoying, particularly if they also need different versions of Coq.
Auto formatting!
Support for Vim
Support for parallel compilation.
Built-in support for Unicode, most of the features of Company-Coq.
Autofill.
Ability to customize indentation. (I have to turn it off entirely when using bra-ket notation, because it interprets angle brackets as parentheses.
Async processing I supoose
Compatibility with undo-tree plugin (Does PG disable undo-tree? #513)
Support for dune (compilation of dependencies from the editor).
Parallel processing using the STM.
support asynchronous proof processing
Better customization for indentation styles, I've raised the issues in the tracker.
Parallel typechecking for files in different buffers
I think it would be better for everyone if support for emacs was dropped as it is the source of a lot of bad practices. Emacs is too focused on text rather than on structure (combine autocompletion or line numbers with headers to see how broken it is) and seriously outdated. Because of its existence we had to wait years before getting a decent experience for users. Emacs is all but user-friendly and even experts I see struggle with.
Search for lemmas (particularly to find more general lemmas than the one looked for)
Reliability, particularly for large files (e.g., machine produced files).
Small possible improvement:
Holding (C-↓) to go down the proof and execute several tactics works fine.
However holding (C-↑) to undo several tactics fails. So I have to hold Ctrl down and repeatedly press ↑. Nothing too important though.
I haven't kept up with the most recent PG features, so some of this might be already there.
A command to process the entire buffer in parallel.
Asynchronous and parallel buffer processing. Ideally, I would like PG and Coq to process everything that it can and print the proof state when I place a cursor at a point. I wouldn't have to need to type C-c C-n all the time.
Automatic indentation commands that work with SSR tactics.
Efficiency. For big projects Emacs + Proof General + Company Coq is terribly slow and sometimes hangs.
For some reason my smart identation is weird on pattern matching on doom, I have to dig deeper on what's the root of the issue.
Sometimes, the indentation is bad, especially when
;is used in combination with*.I don't have any concrete example at hand, sorry.
parallel processing of proofs (within one file)
Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733 #437
Better search and jumping. Jumping to definitions doesn't work well with modules.
Also better tools for refactoring. It's a pain when you add or remove arguments to a function or change a name and have to touch everything up manually.
better sync with the prover. Sometime PG does not show the current goal.
Proof General has changed over the years and I haven't been able to keep up, so I all I do is try to get it to work, which sometimes is a challenge when I have to upgrade to a new version of Coq or MacOS changes. I would like this to be easier.
I use one big emacs window divided into 3 subwindows. I have to do this often by hand because the default doesn't work for me. When I start of Coq, the default is 3 windows side by side and they are two narrow. I have to fix this by hand and create 2 windows side by side, and then split one of them in half horizontally for the goals and response subwindows. This is the configuration that works on my screen. If I restart Coq on a new file in the same emacs session, Proof General reverts to 3 side-by-side windows and I have to start over again to change it by hand. I would like more flexibility in setting up the default behavior.
The three window layout followed by Proof General displays goals and response buffers on the right hand side of the frame. I wish there was an option to show these on the left hand side. When looking at my monitor, I like to write on the right hand section of the screen, and read from the left hand section.
semantic "goto definition"
async protocol.
Indentation sometimes bugs out. Usage via TRAMP in emacs is slow, and required hacks to work last time I tried. Not sure about the current status, but proper TRAMP support would be great!
It seems to get slow if I have a large file (about 1000 lines)
Support for the STM in order to jump to a proof in the middle of a file without checking all the proof scripts.
I'm only a casual Coq user. Often, when I go back to Coq, my Proof General is out of date, so my first hour of working on a Coq project consists of getting Proof General back into a workable state. And even then, regularly there are issues, and I restart my Coq session all the time. However, I find CoqIDE not an alternative, the editor feels too primitive to me. (Also: does it have an electric terminator? I don't want to live without that.)
Better support for showing the time taken for each line. (It's buggy, especially when trying to undo.)
A clean way to stop Coq in the ID when a tactic diverges (I guess this is not Proof General specific).
Display of docstrings for constants (I know this is more a request for Coq).
Caching of proof state at each dot.
I'd like to either have a frame for searches that persists or somehow make the responses frame persist some data. I find it super annoying to have responses disappear immediately after doing one step in something and having to re-search lemmas and such. I understand why it happens, but it still is super annoying.
I use a big font and PG miscalculates the length of lines of text that fit in the goals and responses windows. I'd like PG to fix this issue.
Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733 #437
Proof general +company coq is unusable on large files, as stepping through the buffer takes very long.
refactoring facilities.
Indentation depends sometimes on the application, I'd appreciate a mode saying "please don't try to automatically indent this place", easy to reach from the menu for instance
*response*buffer only shows up in the*coq*buffer.backtracking into proofs and sections; I used to use the XML-based version for this until it bitroted
The automatic indent has been broken for me for a while (indents way too much on enter), and tactic completion no longer works for me. Keep meaning to go through the issue list for those.
A full rewrite to use a reasonable protocol (issue already filled)
Dune support
I have not used Proof General much because of incompatibilities with other things in my Emacs environment -- one of these days I should figure out how to solve this problem but until then I have no useful feedback.
The text was updated successfully, but these errors were encountered: