`coqindent`

## Introduction

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

## Example

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.

## Usage

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

Download: coqindent (version 2009-11-26)

## Copyright/License

I, Eelis van der Weegen, am the sole author of `coqindent`, waive my copyright to it, and release it into the Public Domain.