From 63c28a3e3d37c9d197e9366a1edbb4342eb4a935 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 Jul 2024 15:08:44 +1000 Subject: [PATCH 1/3] Add mcs-devel.xml as analogue to devel.xml This will be the default development manifest for the mcs branch, and mcs.xml will take the role default.xml has for the master branch. Signed-off-by: Gerwin Klein --- mcs-devel.xml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 mcs-devel.xml diff --git a/mcs-devel.xml b/mcs-devel.xml new file mode 100644 index 00000000..9add27a7 --- /dev/null +++ b/mcs-devel.xml @@ -0,0 +1,16 @@ + + + + + + + + + + + + + From 7579fc01bdc4a24043e22f24fef49e46c15b6896 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 Jul 2024 15:11:11 +1000 Subject: [PATCH 2/3] mcs-devel: bump kernel revision Signed-off-by: Gerwin Klein --- mcs-devel.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mcs-devel.xml b/mcs-devel.xml index 9add27a7..b9690a6b 100644 --- a/mcs-devel.xml +++ b/mcs-devel.xml @@ -12,5 +12,5 @@ - + From de8b1430cd626bb15a9ff4b88646c7c378861dbf Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 Jul 2024 15:14:41 +1000 Subject: [PATCH 3/3] Update README for new mcs-devel manifest Signed-off-by: Gerwin Klein --- README.md | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 8ffcb0dc..2b3f4a19 100644 --- a/README.md +++ b/README.md @@ -21,14 +21,19 @@ The manifest files stored here come in three categories: of the seL4 code and proof repositories. It is updated automatically by CI jobs. It points to specific revision hashes, and should generally not be modified manually. -- development manifests such as `devel.xml` and `mcs.xml`: these are for proof - development and typically point to branch names of the verification +- `mcs.xml`: this manifest stores the latest tested-as-working combination of + the seL4 code and proof repositories for the MCS proofs (the `rt` branch in + the `l4v` repository). It is updated automatically by CI jobs. It points to + specific revision hashes, and should generally not be modified manually. + +- development manifests such as `devel.xml` and `mcs-devel.xml`: these are for + proof development and typically point to branch names of the verification repositories in combination with a fixed revision hash of the seL4 code - repository. The seL4 revision in `devel.xml` is updated automatically by CI - jobs for code changes in seL4 that are not visible to the proofs. It should be - updated manually or using the [version bump][] script whenever proofs are - updated in sync with the code. This will then trigger a CI run and, if - successful, a corresponding update in `default.xml`. + repository. The seL4 revision in `devel.xml` and `mcs-devel.xml` is updated + automatically by CI jobs for code changes in seL4 that are not visible to the + proofs. It should be updated manually or using the [version bump][] script + whenever proofs are updated in sync with the code. This will then trigger a CI + run and, if successful, a corresponding update in `default.xml` or `mcs.xml`. - release version manifests such as `12.0.0.xml`: these store the repository version configuration for official releases of seL4. Use these to check proofs