Add a guide for how to write commit messages and commit message tags to
make the messages more consistent and to help new people on the project
get started more quickly.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Extracted from verification-manifest README which now only points to
the instructions in this repo.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- Provide one flattened set of instructions to install all
dependencies, google repo, manifest checkout, and Isabelle
installation. At the end of it, link to the description on how to run
the proofs.
- Remove jEdit section from main README, since it's duplicated in
`setup.md`.
- update Google repo link to a page that contains installation
instructions
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We import some documentation with notes/issues on the refinement from
Haskell to C.
The file is a Markdown-ified version of previous documentation hosted at
UNSW.
Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
This link is stable over Isabelle releases and can be updated once
the repo switches over to the next release.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
* Add Style_pre.thy to contain helpful preliminary definitions.
* Change some style advice according to feedback from the team.
Co-authored-by: Corey Lewis <corlewis@gmail.com>
Co-authored-by: Matthew Brecknell <matthew@brecknell.net>
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
The rules in this style guide should work towards achieving these
goals and form the basis for arguing whether a rule should be
there or not.
Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
Add docs/Style.thy.
This is a starting point for an isabelle style guide. Some of the
material is original and some is incorporated from confluence pages.
I believe that the basics are correct but it will need to be tweaked
and corrected by other proof engineers.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
* Import documentation: Haskell assertions
We import some documentation regarding the role of assertions in Haskell, and how we use assertions in Haskell to transport information from abstract invariants to Haskell-to-C refinement proofs.
The file is a Markdown-ified version of previous documentation hosted at UNSW and Data61.
Co-authored-by: Zoltan A. Kocsis <zoltan.kocsis@data61.csiro.au>
Co-authored-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Signed-off-by: Zoltan A. Kocsis <zoltan.kocsis@data61.csiro.au>
Co-authored-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Co-authored-by: Joel Beeren <joel.beeren@data61.csiro.au>
Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
There is another (out-of-date) dependency description for l4v on the
docs site. To avoid this duplication, this commit factors out the
dependency part of the README, so that it be included directly on the
docs site without going stale.
Also, the README was getting way too long.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Gerwin Klein
Corey Lewis
Rafal Kolanski
Michael McInerney
Ivan Velickovic
Corey Lewis
Gerwin Klein
Zoltan A. Kocsis
Matthew Brecknell
Mitchell Buckley
Gerwin Klein
Mitchell Buckley