Skip to content

Commit e925c83

Browse files
ACassimiroanvacaruPetar MaksimovicpalinatolmachPetarMax
authored
Update to match master branch (#945)
* 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]>
1 parent 30cbad9 commit e925c83

16 files changed

+1709
-50
lines changed

.github/workflows/docker-push.yml renamed to .github/workflows/kontrol-push-fixed-deps.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
---
2-
name: 'Push Docker Image'
2+
name: 'Push Kontrol w/ FIXED Dependencies'
33
on:
44
workflow_dispatch:
55

@@ -29,7 +29,7 @@ jobs:
2929
echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV}
3030
BRANCH_NAME="${{ github.event.inputs.kontrol_branch }}"
3131
SANITIZED_BRANCH_NAME=$(echo "${BRANCH_NAME}" | tr '/' '-' | tr -cd '[:alnum:]-_.')
32-
GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol:ubuntu-jammy-${SANITIZED_BRANCH_NAME}
32+
GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol-custom:ubuntu-jammy-${SANITIZED_BRANCH_NAME}
3333
echo "GHCR_TAG=${GHCR_TAG}" >> ${GITHUB_ENV}
3434
echo "DOCKER_USER=user" >> ${GITHUB_ENV}
3535
echo "DOCKER_GROUP=user" >> ${GITHUB_ENV}

‎.github/workflows/kontrol-push-unfixed-deps.yml‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
---
2+
name: 'Push Kontrol w/ Dependencies'
3+
on:
4+
workflow_dispatch:
5+
inputs:
6+
kevm-version:
7+
description: 'Branch/Tag to use for KEVM'
8+
required: false
9+
default: ''
10+
k-version:
11+
description: 'Branch/Tag to use for K'
12+
required: false
13+
default: ''
14+
llvm-version:
15+
description: 'Branch/Tag to use for LLVM Backend'
16+
required: false
17+
default: ''
18+
haskell-version:
19+
description: 'Branch/Tag to use for Haskell Backend'
20+
required: false
21+
default: ''
22+
23+
jobs:
24+
build-kontrol:
25+
runs-on: [self-hosted, normal]
26+
steps:
27+
- name: 'Login to GitHub Container Registry'
28+
uses: docker/login-action@v2
29+
with:
30+
registry: ghcr.io
31+
username: ${{ github.actor }}
32+
password: ${{ secrets.GITHUB_TOKEN }}
33+
- name: 'Build Kontrol'
34+
shell: bash
35+
run: |
36+
set -o pipefail
37+
docker run --rm -it --detach --name kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kup:latest
38+
if [ -n "${{ inputs.kevm-version }}" ]; then
39+
KEVM_OVERRIDE="--override kevm ${{ inputs.kevm-version }}"
40+
fi
41+
if [ -n "${{ inputs.k-version }}" ]; then
42+
K_OVERRIDE="--override kevm/k-framework ${{ inputs.k-version }}"
43+
fi
44+
if [ -n "${{ inputs.llvm-version }}" ]; then
45+
LLVM_OVERRIDE="--override kevm/k-framework/llvm-backend ${{ inputs.llvm-version }}"
46+
fi
47+
if [ -n "${{ inputs.haskell-version }}" ]; then
48+
HASKELL_OVERRIDE="--override kevm/k-framework/haskell-backend ${{ inputs.haskell-version }}"
49+
fi
50+
docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup install kontrol ${KEVM_OVERRIDE} ${K_OVERRIDE} ${LLVM_OVERRIDE} ${HASKELL_OVERRIDE}"
51+
docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup list kontrol --inputs" >> versions.out
52+
docker commit kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
53+
docker push ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}
54+
- name: 'Publish Versions to Artifacts'
55+
uses: actions/upload-artifact@v3
56+
with:
57+
name: Versions
58+
path: versions.out
59+
- name: 'Publish Image Name to Workflow Summary'
60+
run: |
61+
echo "Image Name: ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}" >> $GITHUB_STEP_SUMMARY
62+
- name: 'Tear down Docker'
63+
if: always()
64+
run: |
65+
docker stop --time=0 kontrol-build-with-kup-${{ github.run_id }}

‎README.md‎

Lines changed: 76 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,82 @@ To update the expected output of the tests, use the `--update-expected-output` f
7171
make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output"
7272
```
7373

74-
For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter.
74+
### Build Development Kontrol Image with Fixed Upstream Dependencies
75+
--------------------------------
76+
Relevant to this workflow [kontrol-push-fixed-deps.yml](.github/workflows/kontrol-push-fixed-deps.yml)
77+
>This is relevant for internal development to publish development images of Kontrol with modified Kontrol changes and retain fixed upstream dependencies.
78+
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.
79+
80+
The intent is to reduce the friction of needing custom builds and avoiding lengthy upstream changes and PRs.
81+
82+
### Build Kontrol with Kup and Specific Dependency Overrides
83+
--------------------------------
84+
Relevant to this workflow [kup-build-kontrol.yml](.github/workflows/kontrol-push-unfixed-deps.yml)
85+
> This is relevant for internal development to publish development images of Kontrol for use in KaaS or a dockerized test environment.
86+
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/).
87+
[See KUP docs for more information](https://github.com/runtimeverification/kup/blob/master/src/kup/install-help.md#kup-install----override)
88+
89+
#### Using Kup
90+
-------------
91+
Relevant dependency options are shown below and can be listed using `kup list kontrol --inputs`
92+
For example:
93+
```
94+
Inputs:
95+
├── k-framework - follows kevm/k-framework
96+
├── kevm - github:runtimeverification/evm-semantics (6c2526b)
97+
│ ├── blockchain-k-plugin - github:runtimeverification/blockchain-k-plugin (c9264b2)
98+
│ │ ├── k-framework - github:runtimeverification/k (5d1ccd5)
99+
│ │ │ ├── haskell-backend - github:runtimeverification/haskell-backend (d933d5c)
100+
│ │ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
101+
│ │ │ ├── llvm-backend - github:runtimeverification/llvm-backend (37b1dd9)
102+
│ │ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f)
103+
│ │ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
104+
│ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils
105+
│ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/rv-utils
106+
│ ├── haskell-backend - follows kevm/k-framework/haskell-backend
107+
│ ├── k-framework - github:runtimeverification/k (81bcc24)
108+
│ │ ├── haskell-backend - github:runtimeverification/haskell-backend (786c780)
109+
│ │ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
110+
│ │ ├── llvm-backend - github:runtimeverification/llvm-backend (d5eab4b)
111+
│ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f)
112+
│ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588)
113+
│ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils
114+
│ └── rv-utils - follows kevm/k-framework/rv-utils
115+
└── rv-utils - follows kevm/rv-utils
116+
```
117+
> **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.
118+
119+
Now run a build using kup and specific dependency overrides:
120+
121+
`kup install kontrol --override kevm/k-framework/haskell-backend "hash/branch_name" --override kevm/k-framework/haskell-backend "hash"`
122+
123+
> **Note**: It's important that you use the short-rev hash or the long for specific revisions of the dependencies to modify.
124+
125+
#### Using the workflow to publish to ghcr.io/runtimeverification
126+
--------------------------------
127+
128+
#### Running the workflow
129+
- Go to repo [Kontrol Actions Page](https://github.com/runtimeverification/kontrol/actions)
130+
- Click on "Push Kontrol w/ Dependencies" from the left hand list
131+
- Click on "Run Workflow" on the top right corner of the list of workflow runs is an option "Run Workflow".
132+
- Use the 'master' branch unless you're doing something special.
133+
- Input the override hash strings for specific dependencies to override in kontrol. See below on how to find the hash for the dependency.
134+
- Then click "Run Workflow" and a job will start.
135+
- The workflow summary shows the name of the image that was built and pushed e.g. ghcr.io/runtimeverification/kontrol-custom:tag
136+
137+
> **Note**: The tag will be a randomly generated string.
138+
139+
[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'
140+
141+
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.
142+
If an input is left blank, the workflow will workout the default hash to use based on kontrols latest release.
143+
144+
Example to fetch the desired hash to insert a different dependency version into the kontrol build.
145+
Substitude the k-framework revision used to build kontrol.
146+
```
147+
K_TAG=$(curl -s https://raw.githubusercontent.com/runtimeverification/kontrol/master/deps/k_release)
148+
git ls-remote https://github.com/runtimeverification/k.git refs/tags/v${K_TAG} | awk '{print $1}'
149+
```
75150

76151
## Resources
77152

‎deps/kevm_release‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1.0.779
1+
1.0.780

‎flake.lock‎

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
description = "Kontrol";
33

44
inputs = {
5-
kevm.url = "github:runtimeverification/evm-semantics/v1.0.779";
5+
kevm.url = "github:runtimeverification/evm-semantics/v1.0.780";
66
nixpkgs.follows = "kevm/nixpkgs";
77
k-framework.follows = "kevm/k-framework";
88
flake-utils.follows = "kevm/flake-utils";

‎poetry.lock‎

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ authors = [
1212

1313
[tool.poetry.dependencies]
1414
python = "^3.10"
15-
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.779", subdirectory = "kevm-pyk" }
15+
kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.780", subdirectory = "kevm-pyk" }
1616
eth-utils = "^4.1.1"
1717
pycryptodome = "^3.20.0"
1818
pyevmasm = "^0.2.3"

0 commit comments

Comments
 (0)