Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 153
    • Issues 153
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !752

Indentation config

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Jonas Kastberg requested to merge jihgfee/iris-coq:indentation_config into master Nov 10, 2021
  • Overview 5
  • Commits 2
  • Pipelines 2
  • Changes 1

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 Nov 10, 2021 by Jonas Kastberg
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: indentation_config