... | ... | @@ -27,6 +27,8 @@ 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.
|
|
|
|
|
|
*RJ*: A possible place for such long-form documentation might be the document we maintain at `tex/iris.tex`. So far this is a reference, not a guide; we could either complement it with an `tex/iris-guide.tex` or add guide parts to it or decide we do not need a reference (the Coq code serves as one) and turn it into a guide.
|
|
|
|
|
|
# Reporting and fixing a bug
|
|
|
|
|
|
Occasionally you'll find bugs in Iris. I hear you say _but it's verified_, so
|
... | ... | @@ -52,7 +54,7 @@ here are the sort of bugs you can run into: |
|
|
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
|
|
|
example. If you think you have a useful algebra or Iris library, 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
|
... | ... | @@ -61,8 +63,8 @@ it: |
|
|
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!
|
|
|
implementation might not be in Iris, but demonstrating the usefulness and
|
|
|
soundness of a library is a useful contribution in its own right!
|
|
|
* 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
|
... | ... | @@ -70,6 +72,6 @@ it: |
|
|
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
|
|
|
is knowing what the useful primitives are. This is even more true for std++: just
|
|
|
identifying a missing theorem that's useful *and* true is really valuable; the proof is often
|
|
|
just an implementation detail. |