Skip to content

Commit

Permalink
create action to update foundry-prove output (#1964)
Browse files Browse the repository at this point in the history
* create action to update prove output

* Set Version: 1.0.237

* manually trigger the workflow

* move as workflow

* add as workflow

* convert event as push

* rem description

* remove docker

* push updates

* remove escaped quote

* apply review suggestions

* Set Version: 1.0.238

* update submodules in action

* update submodules init

* pull all submodules

* Hotfix/add update prove ci (#1970)

* Recursive checkout already will grab the deps

* with-docker input updates

* maven

* INclude stack dep for build k-deps step, fixes failure in Reactor summary Haskell Backend

* create action to update prove output

* manually trigger the workflow

* move as workflow

* add as workflow

* convert event as push

* rem description

* remove docker

* push updates

* remove escaped quote

* apply review suggestions

* update submodules in action

* update submodules init

* pull all submodules

* Recursive checkout already will grab the deps

* with-docker input updates

* maven

* INclude stack dep for build k-deps step, fixes failure in Reactor summary Haskell Backend

* Missing build args for distro and os

* Test

* Install stack

* INclude stack dep for build k-deps step, fixes failure in Reactor summary Haskell Backend

* Force update of submodules

* SKIP_LLVM=true

* add libyaml

* add libcrypto++ dep

* commit changes

* Hotfix/add update prove ci (#1974)

* Use a terminal-rule for `--break-every-step` (#1959)

* Use a terminal-rule for --break-every-step

* Set Version: 1.0.235

* Set Version: 1.0.236

* Set Version: 1.0.237

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

* Add `PreconditionsTest.testAssume` on CI (#1924)

* add the PreconditionsTest#testAssume to CI

* Set Version: 1.0.217

* add preconditions test

* Set Version: 1.0.218

* update expected output

* Set Version: 1.0.219

* include/{evm-types,evm}, kevm-pyk/kompile.py: consistent concrete attributes for rules

* Makefile: allow passing in parallel/filter to every pytest command

* include/{evm,lemmas/lemmas}: more adjustments to concrete attributes

* Set Version: 1.0.220

* kevm-pyk/{cli,__main__}: support --pending/--failing for kevm show-kcfg too

* include/lemmas/lemmas: add simplification lemma for memoryUsageUpdate

* Set Version: 1.0.221

* include/lemmas/lemmas: correct lemma

* include/{evm-types,evm,serialization}: move concrete attribute directly onto rules

* kevm-pyk/kompile: no need for explicit concrete rules list anymore

* include/evm-node: correct concrete attribute for keccak

* .github/test-pr: up timeout with more tests being run

* Set Version: 1.0.222

* Set Version: 1.0.222

* Set Version: 1.0.223

* Set Version: 1.0.224

* fix indenting after merge

* Set Version: 1.0.225

* update hash

* Set Version: 1.0.226

* Set Version: 1.0.228

* Set Version: 1.0.237

* update expected output

* Set Version: 1.0.238

---------

Co-authored-by: François Guyot <[email protected]>
Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Andrei <[email protected]>

* Update dependency: deps/pyk_release (#1962)

* deps/pyk_release: Set Version v0.1.377

* Set Version: 1.0.237

* kevm-pyk/: sync poetry files pyk version v0.1.377

* flake.{nix,lock}: update Nix derivations

* deps/pyk_release: Set Version v0.1.378

* Set Version: 1.0.238

* kevm-pyk/: sync poetry files pyk version v0.1.378

* flake.{nix,lock}: update Nix derivations

* extend lines with a str of the summary

* Set Version: 1.0.239

* Update kevm-pyk/src/kevm_pyk/foundry.py

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>

* Don't ignore `--with-llvm-library` in `kevm kompile` (#1965)

* Don't ignore `--with-llvm-library` in `kevm kompile`

* Set Version: 1.0.237

* Set Version: 1.0.238

* Set Version: 1.0.240

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>

* Pass llvm_definition_dir to KCFGExplore in foundry-prove (#1957)

* Update foundry-kompile, passing llvm_definition_dir to KCFGExplore when using booster

* Set Version: 1.0.235

* Set Version: 1.0.237

* Set Version: 1.0.238

* Set Version: 1.0.239

* Set Version: 1.0.240

* Set Version: 1.0.241

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>

* correctly recursively invoke make (#1975)

* correctly recursively invoke make

* Set Version: 1.0.242

---------

Co-authored-by: devops <[email protected]>

* Remove legacy code and tests, use pyk runner more directly (#1977)

* package/test-package: update package testing script to run foundry proofs too

* bin/kevm: drop solc-to-k and foundry-* commands directly through to pyk

* bin/kevm, Makefile: remove kevm interpret command, no longer needed for tests

* bin/kevm: simplify fallthrough to pyk

* bin/kevm: use direct pyk prover always for run_proof

* bin/kevm: simplify logic with removed options, pass them through to pyk

* package/test-package: add search command test

* bin/kevm: simplify more options

* bin/kevm, scripts/kore-json: do not use dedicated kore -> json conversion

* bin/kevm: more simplifications

* bin/kevm: drop kompile straight through to pyk

* Makefile: remove unexercised test-suites

* Revert "package/test-package: add search command test"

This reverts commit c6dfc55.

* bin/kevm: remove search functionality

* README: interpret => run

* Set Version: 1.0.242

* Makefile: remove references to kore-json.py

* Makefile, VERIFICATION, package/test-package, tests/specs/example/erc20-spec: remove mention of --pyk option

* Makefile: run interactive tests with poetry enabled

* Makefile: remove unused recipe

* package/test-package: remove --pyk option

* tests/failing: update expected output

* bin/kevm: correctly handle kevm kompile

* kevm-pyk/__main__: make sure we print out configuration on failed kruns too

* bin/kevm: add foundry commands to ones passed through to kevm-pyk

* flake.nix: include foundry in kevm-test target

* package/test-package: disable foundry tests on nix ci

* Set Version: 1.0.243

* Makefile: bring back proto-tester

---------

Co-authored-by: devops <[email protected]>

* create action to update prove output

* manually trigger the workflow

* move as workflow

* add as workflow

* convert event as push

* rem description

* remove docker

* push updates

* remove escaped quote

* apply review suggestions

* update submodules in action

* update submodules init

* pull all submodules

* Recursive checkout already will grab the deps

* with-docker input updates

* maven

* INclude stack dep for build k-deps step, fixes failure in Reactor summary Haskell Backend

* Missing build args for distro and os

* Test

* Install stack

* INclude stack dep for build k-deps step, fixes failure in Reactor summary Haskell Backend

* Force update of submodules

* SKIP_LLVM=true

* add libyaml

* add libcrypto++ dep

* commit changes

---------

Co-authored-by: Raoul <[email protected]>
Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Franfran <[email protected]>
Co-authored-by: François Guyot <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Andrei <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Samuel Balco <[email protected]>
Co-authored-by: Dwight Guth <[email protected]>
Co-authored-by: franfran <[email protected]>

* debug test

* remove

* rem

* change echo

* docker run

* add build context

* invoke ARG

* remove FROM ubuntu:jammy

* write back old build step

* remove curly braces

* Adding brackets

* K_VERSION > K_COMMIT"

* build stack from k deps

* get var from id

* get K_VERSION from pyk

* install poetry externally

* install python

* get version from k dep

* remove poetry

* build in deps/k

* cp to new location

* install maven

* use the same user

* replace USER_ID by USER

* run from docker as github-user

* add to PATH

* check for stack upgrade

* write stack on fs

* keep invoking ARG

* remove irrelevant stack call

* add libyaml lib

* run tests and allow empty commit

* pass as PYTEST_ARGS

* test-data/show/: update expected show output

* use pytest

* Set Version: 1.0.245

* write default os-distro

* use booster backedn

* test-data/show/: update expected show output

* use github-user everywhere

* test-data/show/: update expected show output

* test-data/show/: update expected show output

* Set Version: 1.0.246

* test-data/show/: update expected show output

* trigger the action manually

* Set Version: 1.0.247

* don't override llvm

* on workflow disp

* Set Version: 1.0.248

* update master

* arg llvm

* hardcode llvm ver

* Set Version: 1.0.249

* last user forgotten

* indent on:

* Hotfix/add update prove ci (#1998)

* Test foundry build steps. Removing specific name of KEVM package version, only 1 will exist per build

* Remove need dep for testing

* Unbound version fix

* Reduce CI load for testing just packaging

* Reduce CI load for testing just packaging

* Foundry prove indent was wrong for inputs

* Var naming

* Container name

* User dockerfile pointer

* Let there be a user definition accepted from build-args

* Updating reference to 'user'

* user 17 runner always

* user def

* user change

* Fixing foundry root

* Missing slash

* Adding back original test

* cleanup ARG (#2003)

* ARG before FROM and call first

* remove llvm out of scope

* deps/k: back out changes

* apply review suggestions

* Set Version: 1.0.250

* Set Version: 1.0.250

* Set Version: 1.0.251

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Freeman <[email protected]>
Co-authored-by: F-WRunTime <[email protected]>
Co-authored-by: François Guyot <[email protected]>
Co-authored-by: Raoul <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Andrei <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Samuel Balco <[email protected]>
Co-authored-by: Dwight Guth <[email protected]>
  • Loading branch information
13 people authored Aug 10, 2023
1 parent fc2465a commit 5672e27
Show file tree
Hide file tree
Showing 10 changed files with 220 additions and 365 deletions.
67 changes: 60 additions & 7 deletions .github/actions/with-docker/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,28 +3,81 @@ description: 'Run a given stage with Docker Image'
inputs:
tag:
description: 'Docker image tag to use'
type: string
required: true
subdir:
description: 'Subdirectory where code is cloned.'
required: false
type: string
default: './'
os:
description: 'OS to setup Docker for.'
required: false
type: string
default: 'ubuntu'
distro:
description: 'Distribution to setup Docker for.'
required: false
type: string
default: 'jammy'
llvm:
description: 'LLVM version to use.'
required: false
type: number
default: 14
jdk:
description: 'JDK version to use.'
required: false
type: number
default: 17
dockerfile:
description: 'Hardcode the path of the dockerfile to use.'
required: false
type: string
default: '.github/workflows/Dockerfile'
runs:
using: 'composite'
steps:
- name: 'Set up Docker'
shell: bash {0}
env:
TAG_NAME: ${{ inputs.tag }}
run: |
set -euxo pipefail
TAG_NAME=${{ inputs.tag }}
SUBDIR=${{ inputs.subdir }}
BASE_OS=${{ inputs.os }}
BASE_DISTRO=${{ inputs.distro }}
JDK_VERSION=${{ inputs.jdk }}
DOCKERFILE=${{ inputs.dockerfile }}
LLVM_VERSION=${{ inputs.llvm }}
USER=github-user
GROUP=${USER}
Z3_VERSION=4.12.1
LLVM_VERSION=14
K_COMMIT=$(cat deps/k_release)
USER_ID=1000
GROUP_ID=${USER_ID}
K_VERSION=$(cat deps/k/package/version)
docker build . \
--file .github/workflows/Dockerfile.z3 \
--tag z3:${Z3_VERSION} \
docker build . --file .github/workflows/Dockerfile \
docker build deps/k \
--file deps/k/.github/workflows/Dockerfile.stack-deps \
--tag stack:${BASE_DISTRO}-${K_VERSION} \
--build-arg BASE_OS=${BASE_OS} \
--build-arg BASE_DISTRO=${BASE_DISTRO}
docker build . --file ${DOCKERFILE} \
--tag runtimeverification/${TAG_NAME} \
--build-arg USER_ID=${USER_ID} \
--build-arg GROUP_ID=${GROUP_ID} \
--build-arg USER=${USER} \
--build-arg GROUP=${GROUP} \
--build-arg BASE_DISTRO=${BASE_DISTRO} \
--build-arg K_COMMIT=${K_COMMIT} \
--build-arg K_VERSION=${K_VERSION} \
--build-arg Z3_VERSION=${Z3_VERSION} \
--build-arg LLVM_VERSION=${LLVM_VERSION}
Expand All @@ -35,8 +88,8 @@ runs:
--tty \
--detach \
--user root \
--workdir /home/user/workspace \
--workdir /home/${USER}/workspace \
runtimeverification/${TAG_NAME}
docker cp . ${TAG_NAME}:/home/user/workspace
docker exec ${TAG_NAME} chown -R user:user /home/user
docker cp . ${TAG_NAME}:/home/${USER}/workspace
docker exec ${TAG_NAME} chown -R ${USER}:${GROUP} /home/${USER}
36 changes: 27 additions & 9 deletions .github/workflows/Dockerfile
Original file line number Diff line number Diff line change
@@ -1,12 +1,20 @@
ARG K_COMMIT
ARG Z3_VERSION
ARG LLVM_VERSION
ARG K_VERSION
ARG K_COMMIT
ARG BASE_DISTRO

FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY

ARG K_COMMIT
ARG Z3_VERSION
FROM z3:${Z3_VERSION} as Z3

ARG K_VERSION
ARG BASE_DISTRO
FROM stack:${BASE_DISTRO}-${K_VERSION} as STACK

ARG K_COMMIT
ARG LLVM_VERSION
FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}

COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
Expand All @@ -15,6 +23,8 @@ COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast

COPY --from=Z3 /usr/bin/z3 /usr/bin/z3

COPY --from=STACK /usr/local/bin/stack /usr/local/bin/stack

ARG LLVM_VERSION

RUN apt-get update \
Expand All @@ -26,28 +36,36 @@ RUN apt-get update \
curl \
debhelper \
libboost-test-dev \
libcrypto++-dev \
libprocps-dev \
libssl-dev \
libyaml-dev \
llvm-${LLVM_VERSION}-dev \
llvm-${LLVM_VERSION}-tools \
maven \
netcat \
protobuf-compiler \
maven \
python3 \
python3-pip

ARG USER_ID=1000
ARG GROUP_ID=1000
RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
ARG USER=user
ARG GROUP
ARG USER_ID
ARG GROUP_ID
RUN groupadd -g ${GROUP_ID} ${GROUP} && useradd -m -u ${USER_ID} -s /bin/sh -g ${GROUP} ${USER}

USER user:user
RUN mkdir /home/user/workspace
WORKDIR /home/user/workspace
USER ${USER}:${GROUP}
RUN mkdir /home/${USER}/workspace
WORKDIR /home/${USER}/workspace

ENV PATH=/home/user/.cargo/bin:/home/user/.local/bin:${PATH}
ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PATH}

RUN curl -sSL https://install.python-poetry.org | python3 - \
&& poetry --version

RUN cargo install svm-rs --version 0.3.0 \
&& svm install 0.8.13 \
&& solc --version

COPY --from=STACK --chown=$USER:$GROUP /home/$USER/.stack /home/$USER/.stack
36 changes: 18 additions & 18 deletions .github/workflows/master-push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -69,9 +69,9 @@ jobs:
run: |
set -euxo pipefail
version=$(cat package/version)
docker exec -u user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'package/debian/package jammy'
docker exec -u user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'ls ..'
docker cp kevm-package-jammy-${GITHUB_SHA}:/home/user/kevm_${version}_amd64.deb ./
docker exec -u github-user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'package/debian/package jammy'
docker exec -u github-user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'ls ..'
docker cp kevm-package-jammy-${GITHUB_SHA}:/home/github-user/kevm_${version}_amd64.deb ./
- name: 'Tear down Docker'
if: always()
run: |
Expand All @@ -86,28 +86,28 @@ jobs:
docker build . --tag ${tag_name} --file package/docker/Dockerfile \
--build-arg K_VERSION=${k_version} \
--build-arg KEVM_VERSION=${version}
docker run \
--name ${container_name} \
--rm \
--interactive \
--tty \
--detach \
--user root \
--workdir /home/user \
docker run \
--name ${container_name} \
--rm \
--interactive \
--tty \
--detach \
--user root \
--workdir /home/github-user \
${tag_name}
- name: 'Test Docker Image'
run: |
set -euxo pipefail
version=$(cat package/version)
k_version=$(cat deps/k_release)
container_name="kevm-ci-test-${GITHUB_SHA}"
docker cp ./tests/foundry ${container_name}:/home/user/foundry
docker exec -u user ${container_name} /bin/bash -c "sudo chown user:user -R /home/user/foundry"
docker exec -u user ${container_name} /bin/bash -c "forge build --root foundry"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root foundry --verbose --test AssertTest.test_assert_true_branch"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root foundry --verbose AssertTest.test_assert_true_branch"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root foundry --verbose"
docker cp ./tests/foundry ${container_name}:/home/github-user/foundry
docker exec -u github-user ${container_name} /bin/bash -c "sudo chown github-user:github-user -R /home/github-user/foundry"
docker exec -u github-user ${container_name} /bin/bash -c "forge build --root foundry"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root foundry --verbose --test AssertTest.test_assert_true_branch"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root foundry --verbose AssertTest.test_assert_true_branch"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root foundry --verbose"
docker stop --time=0 ${container_name}
- name: 'Push Docker Image to DockerHub'
env:
Expand Down
98 changes: 47 additions & 51 deletions .github/workflows/test-pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -77,12 +77,12 @@ jobs:
with:
tag: kevm-ci-profile-${{ github.sha }}
- name: 'Build kevm-pyk'
run: docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make poetry'
run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make poetry'
- name: 'Build Foundry'
run: docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make build-foundry'
run: docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make build-foundry'
- name: 'Run profiling'
run: |
docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make profile'
docker exec -u github-user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make profile'
- name: 'Tear down Docker'
if: always()
run: |
Expand All @@ -104,19 +104,19 @@ jobs:
with:
tag: kevm-ci-concrete-${{ github.sha }}
- name: 'Build kevm-pyk'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make poetry'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make poetry'
- name: 'Build blockchain-k-plugin-deps'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make CXX=clang++-14 plugin-deps'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make CXX=clang++-14 plugin-deps'
- name: 'Build kevm'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make build-kevm build-haskell build-llvm build-node -j`nproc` RELEASE=true'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make build-kevm build-haskell build-llvm build-node -j`nproc` RELEASE=true'
- name: 'Test kevm-pyk'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-integration'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-integration'
- name: 'Test conformance'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-conformance'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-conformance'
- name: 'Test llvm krun'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-interactive-run TEST_CONCRETE_BACKEND=llvm'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-interactive-run TEST_CONCRETE_BACKEND=llvm'
- name: 'Test node'
run: docker exec -u user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-node -j`nproc`'
run: docker exec -u github-user kevm-ci-concrete-${GITHUB_SHA} /bin/bash -c 'make test-node -j`nproc`'
- name: 'Tear down Docker'
if: always()
run: |
Expand All @@ -137,7 +137,7 @@ jobs:
with:
tag: kevm-ci-haskell-${{ github.sha }}
- name: 'Prove Haskell'
run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove'
run: docker exec -u github-user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove'
- name: 'Tear down Docker'
if: always()
run: |
Expand All @@ -158,11 +158,11 @@ jobs:
with:
tag: kevm-ci-foundry-${{ github.sha }}
- name: 'Build kevm-pyk'
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make poetry'
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make poetry'
- name: 'Build Foundry'
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
- name: 'Foundry Prove'
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS=-vv'
run: docker exec -u github-user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS=-vv'
- name: 'Tear down Docker'
if: always()
run: |
Expand Down Expand Up @@ -229,7 +229,7 @@ jobs:
- name: 'Test KEVM'
run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kevm-test

dockerhub-image-dry-run:
build-deb-package:
name: 'Build Ubuntu Jammy DockerHub Image'
runs-on: [self-hosted, linux, normal]
needs: kevm-pyk-code-quality-checks
Expand All @@ -247,43 +247,39 @@ jobs:
run: |
set -euxo pipefail
version=$(cat package/version)
docker exec -u user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'package/debian/package jammy'
docker exec -u user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'ls ..'
docker cp kevm-package-jammy-${GITHUB_SHA}:/home/user/kevm_${version}_amd64.deb ./
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kevm-package-jammy-${GITHUB_SHA}
- name: 'Build Docker Image'
docker exec -u github-user kevm-package-jammy-${GITHUB_SHA} /bin/bash -c 'package/debian/package jammy'
docker cp kevm-package-jammy-${GITHUB_SHA}:/home/github-user/kevm_${version}_amd64.deb ./
- name: 'Define Foundry Test Variables'
run: |
set -euxo pipefail
version=$(cat package/version)
k_version=$(cat deps/k_release)
tag_name="runtimeverificationinc/kevm:ubuntu-jammy-${version}"
container_name="kevm-ci-test-${GITHUB_SHA}"
docker build . --tag ${tag_name} --file package/docker/Dockerfile \
--build-arg K_VERSION=${k_version} \
--build-arg KEVM_VERSION=${version}
docker run \
--name ${container_name} \
--rm \
--interactive \
--tty \
--detach \
--user root \
--workdir /home/user \
${tag_name}
- name: 'Test Docker Image'
echo "version=$(cat package/version)" >> $GITHUB_ENV
echo "k_version=$(cat deps/k_release)" >> $GITHUB_ENV
echo "tag_name=runtimeverificationinc/kevm:ubuntu-jammy-$(cat package/version)" >> $GITHUB_ENV
echo "container_name=kevm-ci-test-${GITHUB_SHA}" >> $GITHUB_ENV
- name: 'Setup Foundry Test Docker'
uses: ./.github/actions/with-docker
with:
tag: kevm-ci-test-${{ github.sha }}
dockerfile: package/docker/Dockerfile

- name: 'KEVM Foundry Test'
run: |
set -euxo pipefail
version=$(cat package/version)
k_version=$(cat deps/k_release)
container_name="kevm-ci-test-${GITHUB_SHA}"
docker cp ./tests/foundry ${container_name}:/home/user/foundry
docker exec -u user ${container_name} /bin/bash -c "sudo chown user:user -R /home/user/foundry"
docker exec -u user ${container_name} /bin/bash -c "forge build --root foundry"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root foundry --verbose --test AssertTest.test_assert_true_branch"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root foundry --verbose AssertTest.test_assert_true_branch"
docker exec -u user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root foundry --verbose"
docker stop --time=0 ${container_name}
version=${{ env.veresion }}
k_version=${{ env.k_version }}
container_name=${{ env.container_name}}
docker cp ./tests/foundry ${container_name}:/home/github-user/foundry
docker exec -u github-user ${container_name} /bin/bash -c "sudo chown github-user:github-user -R /home/github-user/foundry"
docker exec -u github-user ${container_name} /bin/bash -c "forge build --root /home/github-user/foundry"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root /home/github-user/foundry --verbose"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root /home/github-user/foundry --verbose --test AssertTest.test_assert_true_branch"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root /home/github-user/foundry --verbose AssertTest.test_assert_true_branch"
docker exec -u github-user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root /home/github-user/foundry --verbose"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kevm-package-jammy-${GITHUB_SHA}
docker stop --time=0 kevm-ci-test-${GITHUB_SHA}
Loading

0 comments on commit 5672e27

Please sign in to comment.