|
|
**Warning:** this is a work-in-progress. The Iris developers haven't reached
|
|
|
consensus on the advice here. When they do, it will be incorporated into the
|
|
|
main repository. Feedback is most welcome! If you have comments on the document,
|
|
|
reach out to Tej on Mattermost (@tchajed).
|
|
|
|
|
|
We welcome any contributions to Iris! Before you get started, here's some advice
|
|
|
to ensure that your contribution can be merged.
|
|
|
|
|
|
Iris has many parts and the developers strive for consistency among those parts.
|
|
|
Learning Iris is already hard, and this attention to detail helpers newcomers
|
|
|
familiarize themselves with new parts of Iris more rapidly with less cognitive
|
|
|
burden. However, it can make it difficult to extend Iris if you don't have a
|
|
|
sense for the conventions Iris is targetting, and the same willingness to
|
|
|
maintain consistency. This document aims to help you navigate this tradeoff
|
|
|
between adding new features and maintaining a high quality bar in Iris.
|
|
|
|
|
|
# Fixing documentation
|
|
|
|
|
|
Documentation in Iris is lacking and is not at the same level of care as the
|
|
|
code (yet!). This means that contributions that improve documentation are
|
|
|
extremely welcome, and do not have to be perfect to be accepted if they improve
|
|
|
on what's there.
|
|
|
|
|
|
I'm still figuring out how to write long-form documentation, to supplement the
|
|
|
excellent documentation that is the Iris from the Ground Up paper. In the
|
|
|
meantime, documenting any individual library with a file-level coqdoc comment
|
|
|
can be really helpful to the next person trying to figure out what the library
|
|
|
does.
|
|
|
|
|
|
# Reporting and fixing a bug
|
|
|
|
|
|
Occasionally you'll find bugs in Iris. I hear you say _but it's verified_, so
|
|
|
here are the sort of bugs you can run into:
|
|
|
|
|
|
- The Iris Proof Mode often has bugs in error messages, which aren't as well
|
|
|
tested. For example this bug:
|
|
|
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/460 resulted in a
|
|
|
generic pattern matching failure when the IPM should have given a proper error
|
|
|
message. Reporting this bug is really all you need to do for someone to fix
|
|
|
it. If you're interested in learning about the IPM implementation (which is
|
|
|
really quite cool), we can walk you through fixing easy bugs like these.
|
|
|
- Tactics are often buggy because they're so hard to write and test. For example
|
|
|
this bug fix: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/582.
|
|
|
(This is another case where reporting the bug would help a lot; identifying
|
|
|
and fixing the problem is a bit more involved.)
|
|
|
- If you find a lemma whose name doesn't fit the Iris style, that's a bug!
|
|
|
- If a library is missing a lemma you expected, that seems like a bug! (Assuming
|
|
|
the lemma you want is true.)
|
|
|
|
|
|
# Adding a new library
|
|
|
|
|
|
Iris ships with a handful of useful libraries for algebras and ghost state.
|
|
|
These libraries are quite full-featured: they supply theorems for allocation,
|
|
|
updates, validity, and any interactions between propositions in the library, for
|
|
|
example. If you think you have a useful algebra, it's best to reach out to us
|
|
|
and come up with a plan for upstreaming it.
|
|
|
|
|
|
If you do want to add something, there are basically two ways you can go about
|
|
|
it:
|
|
|
* Provide a sketch for what you want, perhaps in the form of an implementation
|
|
|
in your own project (without needing to follow any Iris conventions). Open an
|
|
|
issue and if somebody is excited about upstreaming it, they will take it over
|
|
|
and expand your library and carefully think through how to name it. Your
|
|
|
implementation might not be in Iris, but consider it as valuable evidence that
|
|
|
the proposed library is sound!
|
|
|
* Upstream it yourself. This will be more work, but it might be quite rewarding!
|
|
|
Just be upfront that you intend to follow through, and be ready for some
|
|
|
hands-on training in how an Iris library works. If this ever becomes too much
|
|
|
and you just want the library merged, we can take over and finish naming
|
|
|
things and proving the extra theorems.
|
|
|
|
|
|
Both of these are valuable; half the battle in a verification library like Iris
|
|
|
is knowing what the useful primitives are. In something like std++, just
|
|
|
identifying a missing theorem that's true is really valuable; the proof is often
|
|
|
just an implementation detail. |