How do I turn off the aggressive auto-indent in Proof General/Coq

Question

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.

Answer 1

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.