From 891e9b02e07d1fead1a42a6b0321472eda44670d Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 3 Jul 2026 10:11:28 -0700 Subject: [PATCH 1/2] update CI for new EverParse based on KRML_EXE instead of KRML_HOME --- .github/workflows/ci.yml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ec399001..79e7d00c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -156,12 +156,6 @@ jobs: path: _opam key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }} - - name: Setup environment - run: | - echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV - echo "EVERPARSE_USE_KRML_HOME=1" >> $GITHUB_ENV - echo "ADMIT=1" >> $GITHUB_ENV - - name: Restore EverParse cache if it exists uses: actions/cache/restore@v4 with: @@ -187,6 +181,14 @@ jobs: export OCAMLRUNPARAM=b OTHERFLAGS='--admit_smt_queries true' make -kj$(nproc) + # KRML_EXE must be set for EverParse, but not when building krmllib + # as part of Karamel, so we set it only here + - name: Setup environment + run: | + echo "KRML_EXE=$(pwd)/karamel/out/bin/krml" >> $GITHUB_ENV + echo "EVERPARSE_USE_KRML_EXE=1" >> $GITHUB_ENV + echo "ADMIT=1" >> $GITHUB_ENV + - name: Generate CBOR and COSE .krml files working-directory: everparse run: | From 6f7421a3aa864e2c44a0c823be7eec1e05b426e7 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Tue, 7 Jul 2026 09:31:47 -0700 Subject: [PATCH 2/2] make sure EverParse cannot create and build its own opt/karamel --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 79e7d00c..c42142c1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -192,6 +192,7 @@ jobs: - name: Generate CBOR and COSE .krml files working-directory: everparse run: | + rm -rf opt/karamel && touch opt/karamel && git pull && make cbor-extract-krml cose-extract-krml -kj$(nproc) # Paranoid delete before saving. Note: run_id is constant across reruns.