Skip to content

Commit 316c0dd

Browse files
bugarelabugarela
authored
Merge pull request #1627 from informalsystems/gabriela/rust-evaluator
🦀 Migrate the Rust evaluator from private repo
2 parents 37385bb + 34f09a0 commit 316c0dd

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

71 files changed

+161476
-120
lines changed

‎.github/workflows/benchmark.yml

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
name: Benchmark
2+
3+
on:
4+
push:
5+
branches: main
6+
paths:
7+
- "evaluator/**"
8+
- ".github/workflows/benchmark.yml"
9+
merge_group:
10+
pull_request:
11+
types: [opened, synchronize]
12+
paths:
13+
- "evaluator/**"
14+
- ".github/workflows/benchmark.yml"
15+
16+
# If new code is pushed to a PR branch, then cancel in progress workflows for that PR.
17+
# Ensures that we don't waste CI time, and returns results quicker.
18+
concurrency:
19+
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
20+
cancel-in-progress: true
21+
22+
env:
23+
CARGO_INCREMENTAL: 0
24+
CARGO_TERM_COLOR: always
25+
RUST_BACKTRACE: short
26+
CARGO_NET_RETRY: 10
27+
RUSTUP_MAX_RETRIES: 10
28+
GIT_LFS_SKIP_SMUDGE: 1
29+
30+
jobs:
31+
benchmark:
32+
name: Run benchmarks
33+
runs-on: ubuntu-latest
34+
defaults:
35+
run:
36+
working-directory: ./evaluator
37+
38+
steps:
39+
- uses: actions/checkout@v4
40+
with:
41+
fetch-depth: 0 # Needed to fetch all history for comparison
42+
43+
- name: Setup Rust toolchain
44+
uses: actions-rust-lang/setup-rust-toolchain@v1
45+
46+
- name: Install cargo-critertion
47+
uses: taiki-e/install-action@v2
48+
with:
49+
tool: cargo-criterion
50+
51+
- name: Install node
52+
uses: actions/setup-node@v3
53+
54+
- name: Install Quint
55+
run: |
56+
git clone https://github.com/informalsystems/quint && cd quint/quint &&
57+
git checkout gabriela/compile-optional-flattening &&
58+
npm install && npm install -g
59+
60+
- name: Build benchmarks
61+
run: cargo build --release --benches
62+
63+
- name: Run benchmark
64+
run: |
65+
# Run benchmarks and save results
66+
cargo criterion --message-format=json > benchmark_results.json
67+
68+
- name: Process benchmark results
69+
id: benchmark-processing
70+
uses: actions/github-script@v7
71+
with:
72+
script: |
73+
const fs = require('fs');
74+
75+
function formatTime(nanoseconds) {
76+
if (nanoseconds < 1000) {
77+
return `${nanoseconds.toFixed(2)} ns`;
78+
} else if (nanoseconds < 1000000) {
79+
return `${(nanoseconds / 1000).toFixed(2)} µs`;
80+
} else if (nanoseconds < 1000000000) {
81+
return `${(nanoseconds / 1000000).toFixed(2)} ms`;
82+
} else {
83+
return `${(nanoseconds / 1000000000).toFixed(2)} s`;
84+
}
85+
}
86+
87+
const results = fs.readFileSync('evaluator/benchmark_results.json', 'utf8')
88+
.split('\n')
89+
.filter(Boolean)
90+
.map(JSON.parse);
91+
92+
let comment = '## Benchmark Results\n\n';
93+
comment += '| Benchmark | Time |\n';
94+
comment += '|-----------|------|\n';
95+
96+
results.forEach(result => {
97+
if (result.reason === 'benchmark-complete') {
98+
const name = result.id;
99+
const time = formatTime(result.mean.estimate);
100+
comment += `| ${name} | ${time} |\n`;
101+
}
102+
});
103+
104+
core.setOutput('benchmark-comment', comment);
105+
106+
- name: Find existing comment
107+
uses: peter-evans/find-comment@v3
108+
id: find-comment
109+
with:
110+
issue-number: ${{ github.event.pull_request.number }}
111+
comment-author: "github-actions[bot]"
112+
body-includes: "Benchmark Results"
113+
114+
- name: Create or update comment
115+
uses: peter-evans/create-or-update-comment@v4
116+
with:
117+
comment-id: ${{ steps.find-comment.outputs.comment-id }}
118+
issue-number: ${{ github.event.pull_request.number }}
119+
body: ${{ steps.benchmark-processing.outputs.benchmark-comment }}
120+
edit-mode: replace

‎.github/workflows/main.yml renamed to ‎.github/workflows/integration.yml

Lines changed: 13 additions & 120 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1-
# This build configuration is adapted from Apalache
1+
name: Integration Tests
22

33
on:
44
# Every pull request
55
pull_request:
6+
path:
7+
- "examples/**"
8+
- "quint/**"
9+
- "evaluator/**"
10+
- ".github/workflows/quint-fixtures.yml"
611
# When part of a merge queue
712
# See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions
813
merge_group:
@@ -13,82 +18,15 @@ on:
1318
push:
1419
branches:
1520
- main
16-
17-
name: build
21+
path:
22+
- "examples/**"
23+
- "quint/**"
24+
- "evaluator/**"
25+
- ".github/workflows/quint-fixtures.yml"
1826

1927
jobs:
20-
quint-linting:
21-
runs-on: ubuntu-latest
22-
defaults:
23-
run:
24-
working-directory: ./quint
25-
strategy:
26-
fail-fast: false
27-
steps:
28-
- uses: actions/checkout@v4
29-
- uses: actions/setup-node@v3
30-
with:
31-
node-version: "18"
32-
- run: npm install
33-
- run: npm run format-check || (echo "Run 'npm run format'" && exit 1)
34-
35-
quint-vscode-linting:
36-
runs-on: ubuntu-latest
37-
strategy:
38-
fail-fast: false
39-
steps:
40-
- uses: actions/checkout@v4
41-
- uses: actions/setup-node@v3
42-
with:
43-
node-version: "18"
44-
- name: Install quint deps
45-
run: cd ./quint && npm install
46-
- name: Install yalc
47-
run: npm i yalc -g
48-
- name: Compile quint vscode plugin
49-
run: make local
50-
- name: Run formatting for the plugin
51-
run: cd ./vscode/quint-vscode && npm run format-check || (echo "Run 'npm run format'" && exit 1)
52-
53-
quint-unit-tests:
54-
runs-on: ${{ matrix.operating-system }}
55-
defaults:
56-
run:
57-
working-directory: ./quint
58-
strategy:
59-
fail-fast: false
60-
matrix:
61-
operating-system: [ubuntu-latest, macos-latest, windows-latest]
62-
steps:
63-
- uses: actions/checkout@v4
64-
- uses: actions/setup-node@v3
65-
with:
66-
node-version: "18"
67-
- run: npm install
68-
- run: npm run compile
69-
- run: npm test
70-
71-
quint-test-generated-up-to-date:
72-
runs-on: ubuntu-latest
73-
defaults:
74-
run:
75-
working-directory: ./quint
76-
strategy:
77-
fail-fast: false
78-
steps:
79-
- uses: actions/checkout@v4
80-
- uses: actions/setup-node@v3
81-
with:
82-
node-version: "18"
83-
- run: npm install
84-
- name: Compile and update test fixtures
85-
run: npm run generate
86-
- name: Check that generated files are up to date
87-
run: |
88-
git diff --exit-code \
89-
|| ( echo ">>> ERROR: Generated files are not up to date. Run 'npm run generate'" && exit 1)
90-
9128
quint-integration-tests:
29+
name: TXM tests
9230
runs-on: ${{ matrix.operating-system }}
9331
strategy:
9432
fail-fast: false
@@ -136,6 +74,7 @@ jobs:
13674
if: matrix.operating-system != 'windows-latest'
13775

13876
quint-examples-dashboard:
77+
name: Examples Dashboard
13978
runs-on: ${{ matrix.operating-system }}
14079
strategy:
14180
fail-fast: false
@@ -175,49 +114,3 @@ jobs:
175114
# Check that it is up to date
176115
git diff --exit-code \
177116
|| ( echo ">>> ERROR: Examples dashboard is out of sync. Fix examples or run 'make examples'" && exit 1)
178-
179-
quint-antlr-grammar:
180-
runs-on: ubuntu-latest
181-
steps:
182-
- uses: actions/checkout@v4
183-
- uses: actions/setup-node@v3
184-
with:
185-
node-version: "18"
186-
- run: cd ./quint && npm install
187-
- run: cd ./quint && npm run antlr
188-
189-
quint-vscode-plugin:
190-
runs-on: ${{ matrix.operating-system }}
191-
strategy:
192-
fail-fast: false
193-
matrix:
194-
operating-system: [ubuntu-latest, macos-latest]
195-
steps:
196-
- uses: actions/checkout@v4
197-
- name: Cache nix store
198-
# Workaround for cache action not playing well with permissions
199-
# See https://github.com/actions/cache/issues/324
200-
uses: john-shaffer/cache@59429c0461095f341a8cf7388e5d3aef37b95edd
201-
with:
202-
path: |
203-
/nix/store
204-
/nix/var/nix/profiles
205-
key: ${{ runner.os }}-nix-${{ hashFiles('**.nix') }}
206-
restore-keys: |
207-
${{ runner.os }}-nix-
208-
${{ runner.os }}-
209-
- name: Install Nix
210-
uses: cachix/install-nix-action@v22
211-
with:
212-
extra_nix_config: |
213-
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
214-
- name: Build dev-shell
215-
run: nix develop -c bash -c exit
216-
- name: Install quint deps
217-
run: cd ./quint && nix develop -c npm install
218-
- name: Compile quint vscode plugin
219-
run: nix develop -c make local
220-
- name: Run vscode unit tests
221-
run: cd ./vscode/quint-vscode && nix develop -c npm test
222-
- name: Check that we can create the vsix package
223-
run: cd ./vscode/quint-vscode && nix develop -c vsce package

‎.github/workflows/lint-evaluator.yml

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
name: Lint Evaluator
2+
3+
on:
4+
push:
5+
branches: main
6+
paths:
7+
- "evaluator/**"
8+
- ".github/workflows/lint-evaluator.yml"
9+
pull_request:
10+
paths:
11+
- "evaluator/**"
12+
- ".github/workflows/lint-evaluator.yml"
13+
14+
permissions:
15+
contents: read
16+
checks: write
17+
18+
# If new code is pushed to a PR branch, then cancel in progress workflows for that PR.
19+
# Ensures that we don't waste CI time, and returns results quicker.
20+
concurrency:
21+
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
22+
cancel-in-progress: true
23+
24+
env:
25+
CARGO_INCREMENTAL: 0
26+
CARGO_TERM_COLOR: always
27+
CARGO_PROFILE_DEV_DEBUG: 1
28+
CARGO_PROFILE_RELEASE_DEBUG: 1
29+
RUST_BACKTRACE: short
30+
CARGO_NET_RETRY: 10
31+
RUSTUP_MAX_RETRIES: 10
32+
RUSTFLAGS: "-Dwarnings"
33+
34+
defaults:
35+
run:
36+
working-directory: ./evaluator
37+
38+
jobs:
39+
fmt:
40+
name: Formatting
41+
runs-on: ubuntu-latest
42+
steps:
43+
- name: Checkout
44+
uses: actions/checkout@v4
45+
- name: Setup Rust toolchain
46+
uses: actions-rust-lang/setup-rust-toolchain@v1
47+
with:
48+
components: rustfmt
49+
working-directory: ./evaluator
50+
- name: Check formatting
51+
uses: actions-rust-lang/rustfmt@v1
52+
with:
53+
manifest-path: ./evaluator/Cargo.toml
54+
working-directory: ./evaluator
55+
56+
clippy:
57+
name: Clippy
58+
runs-on: ubuntu-latest
59+
steps:
60+
- name: Checkout
61+
uses: actions/checkout@v4
62+
- name: Setup Rust toolchain
63+
uses: actions-rust-lang/setup-rust-toolchain@v1
64+
with:
65+
components: clippy
66+
working-directory: ./evaluator
67+
- name: Run clippy
68+
uses: auguwu/clippy-action@1.4.0
69+
with:
70+
token: ${{ secrets.GITHUB_TOKEN }}
71+
working-directory: ./evaluator
72+
# doc:
73+
# name: Doc
74+
# runs-on: ubuntu-latest
75+
# env:
76+
# RUSTDOCFLAGS: -Dwarnings
77+
# steps:
78+
# - uses: actions/checkout@v4
79+
# - name: Setup Rust toolchain
80+
# uses: actions-rust-lang/setup-rust-toolchain@v1
81+
# with:
82+
# # Run docs generation on nightly rather than stable. This enables features like
83+
# # https://doc.rust-lang.org/beta/unstable-book/language-features/doc-cfg.html which allows an
84+
# # API be documented as only available in some specific platforms.
85+
# toolchain: nightly
86+
# - name: Install cargo-docs-rs
87+
# uses: dtolnay/install@cargo-docs-rs
88+
# - name: Generate documentation
89+
# run: cargo docs-rs

0 commit comments

Comments
 (0)