- 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 have so far not been mentioning L4V_ARCH in the instructions and
haven't pointed out which sessions need generated input.
Add this information to the instructions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
The links to nicta.com.au have stopped working, so the publication links
now point to the TS publication pages.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Python 2 has passed its sunset date, and many distributions are
withdrawing support for Python 2.
PEP 394 recommends distributions always install versioned interpreter
commands (e.g. `python3`), but does not make a recommendation about
whether or not an unversioned command (`python`) should exist, or what
version it should run.
It therefore seems advisable to explicitly run scripts using the
`python3` command, for scripts that are compatible with Python 3.
Here, we do this for Python scripts used by `run_tests`. For this to
work, some scripts have been updated in ways that will break Python 2
compatibility. But for some other scripts which were already compatible
with both Python 2 and 3, we have not yet removed Python 2
compatibility. There are also miscellaneous scripts that are not used by
`run_tests`, and these have not yet been updated to Python 3.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Miscellaneous changes to make instructions easier to follow, as well as
updating instructions for Haskell Stack (which is no longer available on
Debian Testing).
Move `mlton-compiler` to the end of the apt-get list so it's easier for
a user to leave it off.
Point the user to the mlton website when installing on Debian Buster,
since there's no maintained mlton package for that distribution.
seL4 and L4V are migrating to python 3 given the upcoming end of python
2's support. Until we've rooted out all the old scripts, we recommend
installing both systems.
- Add instructions for installing the `goto-error` macro in a place
where we might be able to find them.
- Mention the improved auto-indenter, in the hope that we will use it
when writing proofs.
Figuring out that you need to install an extra package _after_ waiting
three hours for CRefine to build isn't fun. Changes the installation
instructions to be like most other projects, i.e. "here is everything
you'll need for anything you'll want to do".
Achim D. Brucker
Gerwin Klein
Gerwin Klein
Corey Lewis
Gerwin Klein
Matthew Brecknell
Edward Pierzchalski
Japheth Lim
Alejandro Gomez-Londono
Gerwin Klein
Japheth Lim
David Greenaway