monnier

> I'm inclined to blame Emacs' known sluggishness on long lines; Just to clarify: there isn't "the one Emacs sluggishness on long lines". Sadly (it would be easier to address)....

> ``` > Goal forall x, > x = > x. > ``` While I can agree with (or understand) the other choices, FWIW, the above looks wrong to me....

> I got further information about this phenomenon. > If I waited during PG was stuck for 10 minutes, then the proof process > proceeded, and I got the following...

> I got this backtrace after pressing `C-g`. Precisely, it took several > minutes to get the backtrace after `C-g`. Please report this part as a bug in Emacs, i.e....

@Matafou: Don't thank me too quickly, I was confused: the backtrace he got has nothing to do with `C-g` (indeed it says (dbus-error "Emacs not compiled with dbus support") rather...

BTW, is there any particular reason for this warning? I can't think of any reason why PG compiled with Emacs-27 would suffer from any problem when running on Emacs≥28.

> Besides that, could we make indentation of continuation lines in functions configurable? > > ```coq > (* current style: *) > List.fold_right (fun x acc => > f x...

>> Can we make sure that this doesn't break company-coq? I think it uses `xxx > defined` as a sign that it needs to reload completion lists. > Indeed this...

> - [ ] `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...

> @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,...