Unable to use C-r as redo in evil mode with ProofGeneral and Coq

[sampollard]

I tried a few things when trying to get C-r to work as redo.

First, I tried installing undo-tree and turning it on via turn-on-undo-tree-mode which gives the following error: buffer does not support undo-tree-mode; undo-tree-mode NOT enabled.

My first attempt at a workaround was to remap redo to something less offensive to ProofGeneral, namely gr via the following:

(define-key evil-normal-state-map (kbd "gr") 'redo)

However, this still gave the error: Wrong type argument: commandp, redo. Anyone have any ideas?

I'm using emacs version 26.2 (from macports) and proof-general-20190618.1328

[cpitclaudel]

The docstring of turn-on-undo-tree-mode says If you want to force `undo-tree-mode' to be enabled regardless, use (undo-tree-mode 1) instead. But I'm not sure that undo-tree actually works with Proof-General (I think I tried it a while ago and ran into issues)

[sampollard]

Thanks for getting back to me. I tried the (undo-tree-mode 1) trick and got the same issue (Wrong type argument). Unfortunately I'm not much of an emacs whiz (hence the evil mode), but I can look into fixing this a little. Do you think it's a problem with Proof-General or evil or undo-tree?

[cpitclaudel]

Oh, wait; don't you need undo-tree-redo instead of redo in there? I think the problems I ran into was probably in the intersection of PG and undo-tree, since I don't use evil.

[sampollard]

Good catch! I got this to work. Here's the fix. You put

(use-package undo-tree
  :config
  (turn-on-undo-tree-mode))
(define-key evil-normal-state-map (kbd "C-r") 'undo-tree-redo)
(define-key evil-normal-state-map (kbd "u") 'undo-tree-undo)

somewhere after you enable evil mode in your .emacs. This allows vim-like undo and redo behavior, while also allowing C-c C-r to retract the whole buffer.

[erikmd]

Hi @sampollard @cpitclaudel, I didn't know undo-tree and I'm happy you could find a solution, but I'm afraid there might be some incompatibility all the same, given that ProofGeneral remaps C-_ to the function pg-protected-undo below, which acts as a "wrapper" around the standard undo/redo of emacs so that PG automatically handles retracting of the locked region at undo time:

pg-protected-undo is an interactive Lisp closure in ‘pg-user.el’.

It is bound to C-_, <undo>, C-/, C-x u, <menu-bar> <edit> <undo>.

(pg-protected-undo &optional ARG)

As ‘undo’ but avoids breaking the locked region.

A numeric ARG serves as a repeat count.
If called interactively, ARG is given by the prefix argument.
If ARG is omitted, nil, or not numeric, it takes the value 1.

It performs each of the desired undos checking that these operations will
not affect the locked region, obeying ‘proof-strict-read-only’ if required.
If strict read only behaviour is enforced, the user is queried whether to
retract before the undo is allowed.  If automatic retraction is enabled,
the retract and undo will go ahead without querying the user.

Moreover, undo/redo is always allowed in comments located in the locked region.

@sampollard So maybe if you enable undo-tree, process some proof and undo proof text within the already-processed (locked) region, I guess that the locked region won't move, so there woud be some mismatch between that region (modified by undo-tree) and the environment known by the prover. Let us know if you observe this… but if yes I'm unsure it's possible to fix it, given that undo and undo-tree don't rely on the same underlying model :-/

[sampollard]

Good noticing @erikmd. You're right, I tested it and my current workaround will not retract the locked region. I'll reopen this as a feature request. I looked briefly at the source code for undo-tree-undo here and it seems tough to fix since both undo-tree-undo and pg-protected-undo both essentially handle the undo-ing from scratch.

The only way I see is to make a new pg-protected-undo-tree-undo function or something which handles both the undo-tree tree structure and proof general's locked regions.

[cpitclaudel]

Yes, I think this is the problem I ran into (and that's why undo-tree doesn't enable itself with turn-on-… in proof-general buffers (it detects the rebinding).

The fix shouldn't be too hard when proof-strict-read-only is nil. In those cases, I think the right approach would be to advise primitive-undo, which is used both by the regular undo and by undo-tree

[cpitclaudel]

The only way I see is to make a new pg-protected-undo-tree-undo function or something which handles both the undo-tree tree structure and proof general's locked regions.

It's OK to limit usage of undo-tree to the simpler case where edits trigger an automatic retract. Then PG's implementation is mostly unneeded.

[monnier]

@sampollard So maybe if you enable undo-tree, process some proof and undo proof text within the already-processed (locked) region, I guess that the locked region won't move, so there woud be some mismatch between that region (modified by the undo) and the environment known by the prover. Let us know if you observe this… but if yes I'm unsure it's possible to fix it, given that undo and undo-tree don't rely on the same underlying model :-/

It can be fixed by replacing pg-protected-undo with an after-change-function which does the retraction (well, doing the retraction directly from after-change-function might be problematic, in which case it would have to limit itself to scheduling the retraction, and then execute that scheduled retraction later, e.g. in a post-command-hook).

    Stefan

[erikmd]

Hi Stefan,

thanks for your suggestion!

It can be fixed by replacing pg-protected-undo with an after-change-function which does the retraction (well, doing the retraction directly from after-change-function might be problematic, in which case it would have to limit itself to scheduling the retraction, and then execute that scheduled retraction later, e.g. in a post-command-hook).

Yes but it this case, one would lose the ability to emulate that setting: (setq proof-strict-read-only t)

proof-strict-read-only is a variable defined in ‘proof-useropts.el’.
Its value is ‘retract’

Documentation:
*Whether Proof General is strict about the read-only region in buffers.
If non-nil, an error is given when an attempt is made to edit the
read-only region, except for the special value ’retract which means
undo first. […]

[erikmd]

To be more precise, if one set (setq proof-strict-read-only t) with current PG master, start proving a lemma with several edits (to be undo-ed later), process its proof, and do C-_, then the undo is not performed at once but the user gets the prompt Next undo will modify read-only region, retract? (y or n) and the undo is triggered aftterwards accordingly.

[erikmd]

@cpitclaudel

The fix shouldn't be too hard when proof-strict-read-only is nil.

Yes, since setting proof-strict-read-only = nil just disables pg-protected-undo's feature (and it's true that the code could be simplified in this case!)

So it remains the other two settings: proof-strict-read-only = 'retract and proof-strict-read-only = t. 'retract alone could be implemented as @monnier outlines, but ideally it would be nice to keep support for both values 'retract and t…

Yes, I think this is the problem I ran into (and that's why undo-tree doesn't enable itself with turn-on-… in proof-general buffers (it detects the rebinding).

could you elaborate on that? I mean, is it another thing that should be fixed as well?

Finally, maybe PG could detect itself that undo-tree is enabled, if need be?

[monnier]

To be more precise, if one set (setq proof-strict-read-only t) with current PG master, start proving a lemma with several edits (to be undo-ed later), process its proof, and do C-_, then the undo is not performed at once but the user gets the prompt Next undo will modify read-only region, retract? (y or n) and the undo is triggered aftterwards accordingly.

[ I'm biased: I find this special casing of undo unconvincing. ]

I guess you could always use span-write-warning (instead of span-read-only) and then in proof-retract-before-change you signal an error when you want to keep the area read-only (the test can look at undo-in-progress to decide if the change is done as part of an undo).

    Stefan

[monnier]

The fix shouldn't be too hard when proof-strict-read-only is nil. Yes, since setting proof-strict-read-only = nil just disables pg-protected-undo's feature (and it's true that the code could be simplified in this case!)

AFAICT pg-protected-undo also does "nothing special" when proof-strict-read-only = retract (or more specifically, what it does would be done by proof-retract-before-change anyway).

[erikmd]

Thanks Stefan! :+1: so it indeed seems feasible to refactor the current implementation of the undo/revert feature, preserve the proof-strict-read-only semantics, and hopefully make it compatible with undo-tree :)

as I had worked on pg-protected-undo at the time I volunteer to prepare a branch (but I won't be able to work on it sooner than Friday 26 July)

[cpitclaudel]

Sorry, I meant the retract case, not the nil case, as you correctly guessed later in the thread :) A branch would be wonderful. :+1:

[kindaro]

@erikmd  I am curious about this feature. Is there something I can do to help fix it? I have little experience with Emacs, but if you would be kind to direct me as to what needs doing, I can put in a few days. I am not sure if I can handle it all by myself.

[kcsongor]

pg-protected-undo makes sure that when you undo, the proof state will be retracted to the point where the undo happened, and it seems to handle edits happening inside comments cleverly too. As a workaround, I wrote the following, which similarly wraps undo-tree's operations (the bindings here are for evil-mode).

    (general-define-key :states 'normal :keymaps '(coq-mode-map)
                        "C-r" 'coq-redo
                        "u" 'coq-undo)

    (defun pg-in-protected-region-p ()
      (< (point) (proof-queue-or-locked-end)))

    (defmacro coq-wrap-edit (action)
      `(if (or (not proof-locked-span)
               (equal (proof-queue-or-locked-end) (point-min)))
           (,action)
         (,action)
         (when (pg-in-protected-region-p)
           (proof-goto-point))))

    (defun coq-redo ()
      (interactive)
      (coq-wrap-edit undo-tree-redo))

    (defun coq-undo ()
      (interactive)
      (coq-wrap-edit undo-tree-undo))


    (add-hook! 'coq-mode-hook #'undo-tree-mode)

It's not as sophisticated as pg-protected-undo, as this will eagerly retract the proof state even if the undo'd action was only editing a comment, but otherwise seems to work reasonably well. Also, I notice now that none of the actual code is coq specific, so it will probably work in any ProofGeneral context.

[patbl]

For anyone searching for this error ("Wrong type argument: commandp, redo"), in my case the problem was caused by the following code:

(defvar my-keys-minor-mode-map (make-keymap) "my-keys-minor-mode keymap.")
(define-key my-keys-minor-mode-map (kbd "C-/") 'isearch-forward)

(define-minor-mode my-keys-minor-mode
  "A minor mode so that my key settings override annoying major modes."
  t " my-keys" 'my-keys-minor-mode-map)

Oddly, other keybindings (e.g., C-?) didn't cause this issue.

I recommend doing a binary search on your Emacs init file to identify the problem.