11
$\begingroup$

I have installed Proof General via Doom Emacs' coq module, keeping most settings as whatever default that module sets. Sometimes the automatic indentation this provides gives results I dislike, and furthermore does so aggressively – even if I fix the indentation manually, Proof General is quick to revert it to automatic indentation. A particularly bad case is records: which look like this:

Record foo : Type := mkFoo {
                        bar : nat;
                      }.

I would prefer:

Record foo : Type := mkFoo {
  bar : nat;
}.

Other problems include it not understanding extensions like Equations, again aggressively breaking any manual indentation.

Relevant-looking variables (ones containing substrings coq and indent) have the following values:

coq-indent-box-style             nil
coq-indent-basic                 2
coq-match-indent                 2
coq-script-indent                t
coq-indent-proofstart            2
coq-indent-modulestart           2
coq-indent-semicolon-tactical    2
coq-smie-after-bolp-indentation  2

Though I'm genuinely looking for an answer, I'm also curious as to whether this is considered on-topic. I think we should expect more gritty tooling questions, and also other acute issues (“What does this error message mean?”, “How can I make this code check?”) when we open up to the public (unless such questions are explicitly banned). An argument against these questions is that one could ask coq.zulipchat.com or wherever instead.

$\endgroup$
4
  • 1
    $\begingroup$ I think this is on topic, but should be decorated with some specific tag like “IDE”, “editors”, or whatnot. Although there is also emacs.stackexchange.com... who knows. Nevertheless it is really an issue that could disturbing your work. This is even more relevant in the case of isabelle, since everything is done in the bundled IDE by default. $\endgroup$ Feb 17 at 0:15
  • 1
    $\begingroup$ @PedroSánchezTerraf but in the case of Isabelle the IDE is basically what is shipped. Coq does not come with Doomemacs, so it is probably better suited over there. The question is quite Emacs specific and I would expect a better answer there. $\endgroup$
    – Wno-all
    Feb 17 at 7:10
  • $\begingroup$ I asked the Doom Emacs people, and they seemed to believe that the relevant settings would be in Proof General, and that the fix would be the same as in basic Emacs except for which file to put the relevant lines of elisp code in. Doom's coq module essentially does 3 things to Proof General: package management, setting indent sizes to the global indent size setting (hence the value 2 in most of the variables I could find), and setting some vi-like key bindings. All of these are overridable. $\endgroup$
    – mudri
    Feb 17 at 8:12
  • $\begingroup$ This is definitely on-topic because this is a question about a mode for a proof assistant. It would be ridiculous to make a distinction between IDEs that are shipped with the software and IDEs that are provided by the community. $\endgroup$
    – Zimm i48
    Feb 17 at 17:20

1 Answer 1

6
$\begingroup$

This also annoys me to no end. I have found a partial fix by adding the following to my user-config (I'm using spacemacs, but I assume it's the same):

(eval-after-load "proof-script"
  '(progn
     (setq electric-indent-mode nil)
     ))

This won't stop emacs from indenting it like that, but it does stop the agressiveness, i.e., the code doesn't go back to where emacs wants it to be after you fix it.

$\endgroup$
2
  • $\begingroup$ You make me realize that I also have this disabled in my own Emacs config (I'm on GNU Emacs, so it seems this is really independent of the variant) and it has been the case for such a long time that I didn't remember it when I answered the Coq Community Survey 2022. $\endgroup$
    – Zimm i48
    Feb 17 at 18:08
  • $\begingroup$ This looks like it works pretty well! I'll play about with it a bit more, then accept the answer if it all works out. $\endgroup$
    – mudri
    Feb 17 at 20:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.