From 5c4987e385461436933f25f4b8b373b84c47e0c1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 Jul 2024 17:40:08 +1000 Subject: [PATCH] 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 --- l4v-deploy/steps.sh | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/l4v-deploy/steps.sh b/l4v-deploy/steps.sh index 4dc5cc2c..0c4510bd 100755 --- 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://git@github.com/seL4/verification-manifest.git + staging-manifest "${MANIFEST_FILE[@]}" ssh://git@github.com/seL4/verification-manifest.git echo "::endgroup::" else if [ -n "${INPUT_MANIFEST}" ]; then + # for checkout-manifest.sh + export REPO_MANIFEST="$INPUT_MANIFEST" + # for sel4-pp declare -a MANIFEST_FILE=("--manifest-file" "${INPUT_MANIFEST}") else declare -a MANIFEST_FILE