coqindent is a small crude Python script that indents Coq proof scripts. It works by scanning coqtop's output for "# subgoals" strings and other cues that proofs have begun/ended, which is obviously an entirely fragile and irresponsible way to do it. Nevertheless, it mostly works, so perhaps it might be of use to others.
Given the input:
Lemma L: P. induction n. assert Q. intuition. split. apply H; auto. exact 3. rewrite IHn. ring. Qed.
coqindent produces the following output:
Lemma L: P.
Proof.
induction n.
assert Q.
intuition.
split.
apply H; auto.
exact 3.
rewrite IHn.
ring.
Qed.
Thus, coqindent makes indentation depth coincide with the number of pending subgoals, revealing the basic proof structure. If you prefer another layout convention, coqindent is not for you.
In addition to applying indentation, coqindent can add "Proof." openings to proofs lacking them, can erase empty lines in proofs, and can do some wrapping.
Usage: coqindent [options] coqtop-invocation < input.v > output.v
Options:
-h, --help show this help message and exit
-i STR, --subgoal-indent=STR
indent each additional subgoal by STR (default: " ")
-w N, --wrap=N wrap at natural break points after N columns
--erase-empty-lines erase empty lines in proof scripts
--add-proof begin multi-line proofs with "Proof."
Here, coqtop-invocation is simply the coqtop command along with arguments necessary to compile the Coq script. For example, if the latter requires "-I foo/bar", then you might run coqindent with
coqindent -i ' ' coqtop -I foo/bar < input.v > output.v
Download: coqindent (version 2009-11-26)
I, Eelis van der Weegen, am the sole author of coqindent, waive my copyright to it, and release it into the Public Domain.