Skip to content

Commit

Permalink
Update to match master branch (#945)
Browse files Browse the repository at this point in the history
* Implement kevm.forgetBranch cheatcode (#899)

* draft FOUNDRYSemantics

* forgetBranch

* add mlEqualsTrue

* minor corrections

* add simplification step

* formatting

* add back not equal

* rename FOUNDRYSemantics to KontrolSemantics

* checking for negation as well

* correcting indentation

* expanding functionality

* heuristic simplifications

* further refinement

* refactoring _exec_forget_custom_step

* add show test

* fix test

* update expected output

---------

Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Palina <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

* Update dependency: deps/kevm_release (#940)

* deps/kevm_release: Set Version 1.0.780

* Sync Poetry files: kevm-pyk version 1.0.780

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

---------

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

* Build Custom Kontrol Versions using a workflow (#941)

* new file:   .github/workflows/kup-build-kontrol.yml
- Adding a new feature to build kontrol images using kup and --overrides

* Update .github/workflows/kup-build-kontrol.yml

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

* modified:   .github/workflows/docker-push.yml
modified:   .github/workflows/kup-build-kontrol.yml
- Standardizing the naming between these two workflows to know which is
  for which
- Docker-push builds a custom version of kontrol with fixed dependencies
  already published and built with kontrol
- kup-build-kontrol.yml will build the existing kontrol code with a
  single new
  dependency
modified:   README.md
- Adding some readme instructions.

* renamed:    .github/workflows/docker-push.yml -> .github/workflows/kontrol-push-fixed-deps.yml
renamed:    .github/workflows/kup-build-kontrol.yml -> .github/workflows/kontrol-push-unfixed-deps.yml
modified:   README.md
- Add some background between the two kontrol build workflows

* modified:   README.md
-- Adding content to explain the two custom kontrol build workflows

* Update README.md

Co-authored-by: Anton Savienko <[email protected]>

* Filling in the 'get' placeholder with functionality to fetch appropriate
defaults when nothing is provided

* modified:   README.md
- Adding instructions to fetch hash and use the wrofklow with multiple
  dep options now available

* Update spelling and gramar

* modified:   .github/workflows/kontrol-push-unfixed-deps.yml
- Fixing reporting of final versions used to build kontrol.
- Removing dfining override for undefined inputs to the workflow

---------

Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Anton Savienko <[email protected]>

---------

Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Palina <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: devops <[email protected]>
Co-authored-by: Freeman <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: Anton Savienko <[email protected]>
  • Loading branch information
10 people authored Jan 24, 2025
1 parent 30cbad9 commit e925c83
Show file tree
Hide file tree
Showing 16 changed files with 1,709 additions and 50 deletions.
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
name: 'Push Docker Image'
name: 'Push Kontrol w/ FIXED Dependencies'
on:
workflow_dispatch:

Expand Down Expand Up @@ -29,7 +29,7 @@ jobs:
echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV}
BRANCH_NAME="${{ github.event.inputs.kontrol_branch }}"
SANITIZED_BRANCH_NAME=$(echo "${BRANCH_NAME}" | tr '/' '-' | tr -cd '[:alnum:]-_.')
GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol:ubuntu-jammy-${SANITIZED_BRANCH_NAME}
GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol-custom:ubuntu-jammy-${SANITIZED_BRANCH_NAME}
echo "GHCR_TAG=${GHCR_TAG}" >> ${GITHUB_ENV}
echo "DOCKER_USER=user" >> ${GITHUB_ENV}
echo "DOCKER_GROUP=user" >> ${GITHUB_ENV}
Expand Down
65 changes: 65 additions & 0 deletions .github/workflows/kontrol-push-unfixed-deps.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
---
name: 'Push Kontrol w/ Dependencies'
on:
workflow_dispatch:
inputs:
kevm-version:
description: 'Branch/Tag to use for KEVM'
required: false
default: ''
k-version:
description: 'Branch/Tag to use for K'
required: false
default: ''
llvm-version:
description: 'Branch/Tag to use for LLVM Backend'
required: false
default: ''
haskell-version:
description: 'Branch/Tag to use for Haskell Backend'
required: false
default: ''

jobs:
build-kontrol:
runs-on: [self-hosted, normal]
steps:
- name: 'Login to GitHub Container Registry'
uses: docker/login-action@v2
with:
registry: ghcr.io
username: ${{ github.actor }}
password: ${{ secrets.GITHUB_TOKEN }}
- name: 'Build Kontrol'
shell: bash
run: |
set -o pipefail
docker run --rm -it --detach --name kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kup:latest
if [ -n "${{ inputs.kevm-version }}" ]; then
KEVM_OVERRIDE="--override kevm ${{ inputs.kevm-version }}"
fi
if [ -n "${{ inputs.k-version }}" ]; then
K_OVERRIDE="--override kevm/k-framework ${{ inputs.k-version }}"
fi
if [ -n "${{ inputs.llvm-version }}" ]; then
LLVM_OVERRIDE="--override kevm/k-framework/llvm-backend ${{ inputs.llvm-version }}"
fi
if [ -n "${{ inputs.haskell-version }}" ]; then
HASKELL_OVERRIDE="--override kevm/k-framework/haskell-backend ${{ inputs.haskell-version }}"
fi
docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup install kontrol ${KEVM_OVERRIDE} ${K_OVERRIDE} ${LLVM_OVERRIDE} ${HASKELL_OVERRIDE}"
docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup list kontrol --inputs" >> versions.out
docker commit kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
docker push ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
- name: 'Publish Versions to Artifacts'
uses: actions/upload-artifact@v3
with:
name: Versions
path: versions.out
- name: 'Publish Image Name to Workflow Summary'
run: |
echo "Image Name: ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}" >> $GITHUB_STEP_SUMMARY
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kontrol-build-with-kup-${{ github.run_id }}
77 changes: 76 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,82 @@ To update the expected output of the tests, use the `--update-expected-output` f
make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output"
```

For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter.
### Build Development Kontrol Image with Fixed Upstream Dependencies
--------------------------------
Relevant to this workflow [kontrol-push-fixed-deps.yml](.github/workflows/kontrol-push-fixed-deps.yml)
>This is relevant for internal development to publish development images of Kontrol with modified Kontrol changes and retain fixed upstream dependencies.
The use case for this workflow is intended to facilitate testing changes to Kontrol needed for use in testing CI or in other downstream workflows without needing to publish changes or PRs first.

The intent is to reduce the friction of needing custom builds and avoiding lengthy upstream changes and PRs.

### Build Kontrol with Kup and Specific Dependency Overrides
--------------------------------
Relevant to this workflow [kup-build-kontrol.yml](.github/workflows/kontrol-push-unfixed-deps.yml)
> This is relevant for internal development to publish development images of Kontrol for use in KaaS or a dockerized test environment.
Use the workflow [Kup Build Kontrol](.github/workflows/kup-build-kontrol.yml) to publish a custom version of Kontrol for use in CI and [KaaS](https://kaas.runtimeverification.com/).
[See KUP docs for more information](https://github.com/runtimeverification/kup/blob/master/src/kup/install-help.md#kup-install----override)

#### Using Kup
-------------
Relevant dependency options are shown below and can be listed using `kup list kontrol --inputs`
For example:
```
Inputs:
├── k-framework - follows kevm/k-framework
├── kevm - github:runtimeverification/evm-semantics (6c2526b)
│ ├── blockchain-k-plugin - github:runtimeverification/blockchain-k-plugin (c9264b2)
│ │ ├── k-framework - github:runtimeverification/k (5d1ccd5)
│ │ │ ├── haskell-backend - github:runtimeverification/haskell-backend (d933d5c)
│ │ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
│ │ │ ├── llvm-backend - github:runtimeverification/llvm-backend (37b1dd9)
│ │ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f)
│ │ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
│ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
│ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/rv-utils
│ ├── haskell-backend - follows kevm/k-framework/haskell-backend
│ ├── k-framework - github:runtimeverification/k (81bcc24)
│ │ ├── haskell-backend - github:runtimeverification/haskell-backend (786c780)
│ │ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
│ │ ├── llvm-backend - github:runtimeverification/llvm-backend (d5eab4b)
│ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f)
│ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
│ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
│ └── rv-utils - follows kevm/k-framework/rv-utils
└── rv-utils - follows kevm/rv-utils
```
> **Notice**: the 'follows' in the 'kup list' output. This shows the links to the important dependencies and which are affected when you set the overrides.
Now run a build using kup and specific dependency overrides:

`kup install kontrol --override kevm/k-framework/haskell-backend "hash/branch_name" --override kevm/k-framework/haskell-backend "hash"`

> **Note**: It's important that you use the short-rev hash or the long for specific revisions of the dependencies to modify.
#### Using the workflow to publish to ghcr.io/runtimeverification
--------------------------------

#### Running the workflow
- Go to repo [Kontrol Actions Page](https://github.com/runtimeverification/kontrol/actions)
- Click on "Push Kontrol w/ Dependencies" from the left hand list
- Click on "Run Workflow" on the top right corner of the list of workflow runs is an option "Run Workflow".
- Use the 'master' branch unless you're doing something special.
- Input the override hash strings for specific dependencies to override in kontrol. See below on how to find the hash for the dependency.
- Then click "Run Workflow" and a job will start.
- The workflow summary shows the name of the image that was built and pushed e.g. ghcr.io/runtimeverification/kontrol-custom:tag

> **Note**: The tag will be a randomly generated string.
[The workflow](.github/workflows/kontrol-push-unfixed-deps.yml) takes multiple inputs to override the various components of kontrol. Those overrides are listed above in the example output of 'kup list kontrol --inputs'

To set the desired revisions of the dependencies. Find the associated hash on the branch and commit made to be used for the dependnecy override.
If an input is left blank, the workflow will workout the default hash to use based on kontrols latest release.

Example to fetch the desired hash to insert a different dependency version into the kontrol build.
Substitude the k-framework revision used to build kontrol.
```
K_TAG=$(curl -s https://raw.githubusercontent.com/runtimeverification/kontrol/master/deps/k_release)
git ls-remote https://github.com/runtimeverification/k.git refs/tags/v${K_TAG} | awk '{print $1}'
```

## Resources

Expand Down
2 changes: 1 addition & 1 deletion deps/kevm_release
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.0.779
1.0.780
8 changes: 4 additions & 4 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
description = "Kontrol";

inputs = {
kevm.url = "github:runtimeverification/evm-semantics/v1.0.779";
kevm.url = "github:runtimeverification/evm-semantics/v1.0.780";
nixpkgs.follows = "kevm/nixpkgs";
k-framework.follows = "kevm/k-framework";
flake-utils.follows = "kevm/flake-utils";
Expand Down
8 changes: 4 additions & 4 deletions poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ authors = [

[tool.poetry.dependencies]
python = "^3.10"
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.779", subdirectory = "kevm-pyk" }
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.780", subdirectory = "kevm-pyk" }
eth-utils = "^4.1.1"
pycryptodome = "^3.20.0"
pyevmasm = "^0.2.3"
Expand Down
Loading

0 comments on commit e925c83

Please sign in to comment.