Commit 9f3b576
Update dependency: deps/haskell-backend_release (#4933)
**Also pins Lean toolchain for klean codegen.**
CI integration test `klean/test_generate` started failing independently
of the haskell-backend bump: the klean template's `lean-toolchain` was
set to `stable`, so `lake build` in the generated project floated to the
latest stable Lean. v4.31.0 added `ByteArray.decEq` to core, which
collides with the definition the template emits (`Prelude.lean:226`),
failing the build with `` `ByteArray.decEq` has already been declared
``. Pinned the template's `lean-toolchain` to `leanprover/lean4:v4.30.0`
(last stable before the conflict; verified locally that v4.29.1 and
v4.30.0-rc2 compile the generated `ByteArray.decEq` cleanly).
Follow-up (out of scope): the template still hand-rolls
`ByteArray.decEq`; to move to Lean ≥4.31 it should drop that and use
core's `DecidableEq ByteArray`.
---------
Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>1 parent 44f644b commit 9f3b576
5 files changed
Lines changed: 11 additions & 11 deletions
File tree
- deps
- haskell-backend/src/main/native
- pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
| 1 | + | |
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
8 | 8 | | |
9 | 9 | | |
10 | 10 | | |
11 | | - | |
| 11 | + | |
12 | 12 | | |
13 | 13 | | |
14 | 14 | | |
| |||
Submodule haskell-backend updated 14 files
- booster/hs-backend-booster.cabal+2-1
- booster/library/Booster/Pattern/Match.hs+143-137
- booster/package.yaml+1-1
- booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs+79
- booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs+144
- booster/unit-tests/Test/Booster/Pattern/MatchEval.hs+137-7
- booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs+59-4
- booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs+5-1
- dev-tools/hs-backend-booster-dev-tools.cabal+1-1
- dev-tools/package.yaml+1-1
- kore-rpc-types/kore-rpc-types.cabal+1-1
- kore/kore.cabal+1-1
- package/debian/changelog+1-1
- package/version+1-1
Lines changed: 1 addition & 1 deletion
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
| 1 | + | |
0 commit comments