l4v-deploy: add deployment to/from other manifests

Add mechanism for deploying after preprocess and after proof test to manifests other than devel.xml/default.xml. Currently only mcs.xml and mcs-devel.xml are allowed. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jul 18, 2024 · 19d5710 · 19d5710
1 parent c753e01
commit 19d5710
Showing 1 changed file with 17 additions and 5 deletions.
diff --git a/l4v-deploy/steps.sh b/l4v-deploy/steps.sh
@@ -22,14 +22,23 @@ echo "::endgroup::"
 
 if [ -z "${INPUT_PREPROCESS}" ]
 then
-  # As a safeguard, we insist that INPUT_MANIFEST is
-  # only set for preprocess updates.
-  if [ -n "${INPUT_MANIFEST}" ]
+  # For deployment after test, we can only deal with the default devel.xml and a
+  # potentially provided mcs-devel.xml, but no other input manifests.
+  if [ -n "${INPUT_MANIFEST}" ] && [ "${INPUT_MANIFEST}" != "mcs-devel.xml" ]
   then
-    echo "Error: INPUT_MANIFEST was set for a non-preprocess deployment" >&2
+    echo "Error: INPUT_MANIFEST was set, but not mcs-devel.xml for a non-preprocess deployment" >&2
     exit 1
   fi
 
+  if [ "${INPUT_MANIFEST}" == "mcs-devel.xml" ]; then
+    # for checkout-manifest.sh; read input from mcs-devel.xml
+    export REPO_MANIFEST="$INPUT_MANIFEST"
+    # deploy hashes to mcs.xml
+    declare -a MANIFEST_FILE=("--manifest-file" "mcs.xml")
+  else
+    declare -a MANIFEST_FILE
+  fi
+
   echo "::group::Repo checkout"
   export REPO_DEPTH=0
   checkout-manifest.sh
@@ -43,10 +52,13 @@ then
   echo "::endgroup::"
 
   echo "::group::Deploy"
-  staging-manifest ssh://[email protected]/seL4/verification-manifest.git
+  staging-manifest "${MANIFEST_FILE[@]}" ssh://[email protected]/seL4/verification-manifest.git
   echo "::endgroup::"
 else
   if [ -n "${INPUT_MANIFEST}" ]; then
+    # for checkout-manifest.sh
+    export REPO_MANIFEST="$MANIFEST_FILE"
+    # for sel4-pp
     declare -a MANIFEST_FILE=("--manifest-file" "${INPUT_MANIFEST}")
   else
     declare -a MANIFEST_FILE