History

Gerwin Klein 372952b7b8 docs: update python setup instructions Update instructions for new python versions. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2025-04-01 11:03:26 +11:00
..
plans	make Jira links nicer	2021-04-13 16:27:42 +10:00
Makefile	docs: add style guide to `run_tests`	2021-06-29 10:57:53 +10:00
README.md	docs: add recent content to README	2024-07-10 15:20:15 +10:00
ROOT	docs: split_simps and case over fun/primrec	2022-05-05 09:18:47 +10:00
Style.thy	docs: style: fact transformers and attributes	2024-12-09 19:09:05 +11:00
Style_pre.thy	update copyright	2022-11-09 15:52:50 +11:00
arch-split.md	trivial: rename arch_split -> arch-split	2024-07-26 10:02:47 +10:00
commit-messages.md	docs: add a guide for commit messages	2024-01-17 15:21:41 +11:00
compacting-proofs.md	Matt's short guide on compacting proofs	2021-04-13 10:41:28 +10:00
conventions.md	docs: use internet archive for isabelle.systems	2024-08-09 06:40:00 +02:00
crefine-notes.md	docs: add vcg debugging guide	2024-07-10 15:20:15 +10:00
de-duplicating-proofs.md	Add arch-splitting documentation	2021-04-13 10:41:28 +10:00
find-consts.md	Japheth's guide to find_consts	2021-04-13 10:41:28 +10:00
find-theorems.md	docs+README: update Isabelle links to https	2024-01-17 15:21:06 +11:00
haskell-assertions.md	Import documentation: Haskell assertions (#285 )	2021-06-03 08:24:56 +10:00
platform-branches.md	docs: document platform branch procedure	2024-07-05 09:44:37 +10:00
setup.md	docs: update python setup instructions	2025-04-01 11:03:26 +11:00
tests.xml	docs: add style guide to `run_tests`	2021-06-29 10:57:53 +10:00
vcg-debugging.md	docs: add vcg debugging guide	2024-07-10 15:20:15 +10:00

README.md

Documentation

This directory contains markdown and theory files with conventions and other documentation for the l4v repository.

This is work in progress and contributions are welcome. Feel encouraged to raise pull requests for more material and/or corrections.

Topics

Current topics are:

Setup for doing seL4 proofs
Naming conventions in this repository
Commit message conventions in this repository
Proof style rules for this repository
Using find_theorems effectively
Using find_consts effectively
De-duplicating proofs
Compacting proofs
Architecture Split Why and How-To
Haskell Assertions: how to use assertions in Haskell to use information from AInvs on Haskell and C levels
General CRefine Notes
Debugging VCG goals and failures in CRefine
Platform branches -- what they are and how to update them

Plans

The directory plans/ contains ideas and plans for proof-engineering improvements in this repo. They are at the idea stage, not fully worked out yet. Feel free to contribute new ideas, to make an existing one more concrete, or to pick one up and work on it.