Skip to content

GitLab

Indentation config

Merged Jonas Kastberg requested to merge jihgfee/iris-coq:indentation_config into master

The indentation strategy of Emacs / ProofGeneral is not compatible with the Iris syntax, and can sometimes leave definitions, lemmas, and proofs, in a non-constructive state, e.g.:

Definition my_iris_def my_assumption my_conclusion :=
  my_assumption -∗
                my_conclusion.

The suggested fix (by adding a line to the users Emacs config file) relates the Iris-specific symbols with closely related known Coq symbols (e.g. "-∗" with "->"), and use their indentation strategy instead. This gives a much nicer result:

Definition my_iris_def my_assumption my_conclusion :=
  my_assumption -∗
  my_conclusion.

TODO: We should figure out what symbols to include, and the best symbols to relate them to. There are also outstanding indentation errors that are Iris related which we might see if we can fix (or at least address explicitly that we do not). The worst offender that I have found so far is:

iInduction xs as [|x xs IHxs] forall (ys).
                                     - <proof>
Edited by Jonas Kastberg