Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix up the aws-lc-verification and blst-verification CI runs #2199

Merged
merged 3 commits into from
Jan 28, 2025
Merged

Fix up the aws-lc-verification and blst-verification CI runs #2199

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d179a6a
Set IN_SAW_CI=yes for the aws-lc and blst verification runs.
sauclovian-g Jan 23, 2025
b3cf031
Update the aws-lc-verification and blst-verification commit hashes.
sauclovian-g Jan 27, 2025
8f2d3b6
Bump the CI's cabal cache version since it looks like it's gotten hosed.
sauclovian-g Jan 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ env:
# older .so files are cached, which can have various effects
# (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
CABAL_CACHE_VERSION: 2
CABAL_CACHE_VERSION: 3
SOLVER_CACHE_VERSION: 1

DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
Expand Down
15 changes: 14 additions & 1 deletion s2nTests/docker/awslc.dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,24 @@ RUN curl -OL https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0
tar xf clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \
cp -r clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04/* /usr

# The commit we check out is now the head of the saw-test-runs branch,
# because we added that commit (and branch) specifically to fix up
# some problems with this test run. Prior to that the commit was the
# head of the sb/functors-ci-pin branch. It is no longer clear at this
# point (January 2025) why that particular branch was chosen (there
# are many) or how it relates to the upstream state of the repository
# (our copy in GaloisInc is a fork repo).
#
# We're using the specific commit hash rather than the branch (even
# though the branch is now specific to what we're doing here) so it
# doesn't silently update on us if/when we start tidying up over
# there.

WORKDIR /saw-script
RUN mkdir -p /saw-script && \
git clone https://github.com/GaloisInc/aws-lc-verification.git && \
cd aws-lc-verification && \
git checkout 9e9dde6882ade1f5d01c6d088e6dcca181358a74 && \
git checkout f2570467f0d8ce21df00b3cf3ccc325656d77b4e && \
git config --file=.gitmodules submodule.src.url https://github.com/awslabs/aws-lc && \
git submodule sync && \
git submodule update --init
Expand Down
7 changes: 6 additions & 1 deletion s2nTests/docker/blst.dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,14 @@ RUN curl -OL https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0
tar xf clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \
cp -r clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04/* /usr

# The commit we check out is the head of the main branch.
#
# We're using the specific commit hash (rather than checking out main)
# so it doesn't update under us unexpectedly.

RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \
cd /workdir && \
git checkout f7c50e400d18066cc4849513418c3f407ba3c608 && \
git checkout 9895c023e510c4e89dec098db0467a28ba14785b && \
git config --file=.gitmodules submodule.blst.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.blst_patched.url https://github.com/supranational/blst && \
git config --file=.gitmodules submodule.blst_bulk_addition.url https://github.com/supranational/blst && \
Expand Down
4 changes: 3 additions & 1 deletion s2nTests/scripts/awslc-entrypoint.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
#!/usr/bin/env bash
set -xe

export IN_SAW_CI=yes
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would suggest using the CI_TEST_LEVEL variable that we use in other repos for consistency. It has apparently not been set yet in the CI configuration for saw or cryptol, but it is used in numerous other repositories (e.g. https://github.com/GaloisInc/crucible/blob/master/.github/workflows/crux-llvm-build.yml#L62 and https://github.com/GaloisInc/what4/blob/038e948817b092ac7750e073f1d430ee293f3c20/.github/workflows/test.yml#L61).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So the reason I didn't do that, or the reason not to do that, or something, is that it should be a variable that's specific to SAW (and, ideally, these particular test runs) and that one isn't. In particular using it for this purpose would prevent using it in either of the other trees' CI logic.

...and given that one of the blst-verification CI jobs seems to run for >6 hours, if that tree ever comes back to life they probably should use it. :-|


cd /saw-script/aws-lc-verification/SAW
./scripts/install.sh
rm bin/saw
rm -f bin/saw
cp /saw-bin/saw bin/saw
cp /saw-bin/abc bin/abc
cp /saw-bin/yices bin/yices
Expand Down
2 changes: 2 additions & 0 deletions s2nTests/scripts/blst-entrypoint.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
#!/usr/bin/env bash
set -xe

export IN_SAW_CI=yes

cd /workdir
./scripts/install.sh
cp /saw-bin/cryptol bin/cryptol
Expand Down
Loading