Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Rename kprovex => kprove, kprove => kprove-legacy #2490

Closed
5 tasks done
ehildenb opened this issue Mar 18, 2022 · 7 comments
Closed
5 tasks done

Rename kprovex => kprove, kprove => kprove-legacy #2490

ehildenb opened this issue Mar 18, 2022 · 7 comments
Assignees

Comments

@radumereuta
Copy link
Contributor

Might need to adjust things in the test harness:

  • rename kprovex -> kprove in the K repo and the semantics repo.
  • check Makefiles and configuration files

@Baltoli
Copy link
Contributor

Baltoli commented May 2, 2022

WASM semantics update: runtimeverification/wasm-semantics#449

@Baltoli
Copy link
Contributor

Baltoli commented May 10, 2022

As of #2579, kprove has been deprecated and we're ready to rename kprovex.

This will be a multi-stage process again:

  • Rename current kprovex script to kprove now that the name is available, but keep a shim called kprovex.
  • Update downstream semantics that call kprovex to instead call kprove:
    • WASM
    • EVM
    • AVM
    • Michelson
    • ??? any more
  • Delete kprovex shim

@radumereuta
Copy link
Contributor

I think this list is outdated.
@Baltoli can you check if this can be closed?

@Baltoli
Copy link
Contributor

Baltoli commented Jun 6, 2022

Not quite - I need to see what's breaking the Haskell backend's PR here; once that's merged we can delete kprovex and this will be done.

@radumereuta
Copy link
Contributor

@Baltoli is this #2622 the final piece of the puzzle?

@Baltoli Baltoli closed this as completed Jun 27, 2022
@Baltoli
Copy link
Contributor

Baltoli commented Jun 27, 2022

Yes - I've closed the issue as it's all done now.

h0nzZik pushed a commit to h0nzZik/k that referenced this issue Nov 24, 2022
…untimeverification#1830)

* haskell-backend/src/main/native/haskell-backend: 79703e11 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 8428df45 - LTS Haskell 17.4

* haskell-backend/src/main/native/haskell-backend: 2e714c56 - Add an EquationVariableName to RewritingVariableName

* haskell-backend/src/main/native/haskell-backend: c5cc46be - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 0c4ad203 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: a182994f - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 9460590a - Simplify side conditions (runtimeverification#2393)

* haskell-backend/src/main/native/haskell-backend: 4fb83523 - Fix `variable` to `RewritingVariableName` in `Kore.Equation.Application` (runtimeverification#2325)

* haskell-backend/src/main/native/haskell-backend: f41cba23 - Revert "Revert runtimeverification#2315 (runtimeverification#2385)" (runtimeverification#2389)

* haskell-backend/src/main/native/haskell-backend: 44eed8d7 - Run Test workflow on macOS (runtimeverification#2420)

* haskell-backend/src/main/native/haskell-backend: 904f5322 - kore-repl: Print human-readable error messages (runtimeverification#2441)

* haskell-backend/src/main/native/haskell-backend: b49fdd3c - Make Conditional's term a strict field (runtimeverification#2442)

* haskell-backend/src/main/native/haskell-backend: 01f0402d - adding match for And (runtimeverification#2435)

* haskell-backend/src/main/native/haskell-backend: 3243d1e5 - kore-0.41.0.0 (runtimeverification#2444)

* haskell-backend/src/main/native/haskell-backend: 28913344 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: abf0292b - Use unit and element symbol attributes

* haskell-backend/src/main/native/haskell-backend: 7d3ee1bc - Inefficient Equation renaming (runtimeverification#2438)

* haskell-backend/src/main/native/haskell-backend: 95b6c107 - Stop simplifying the left-hand side of equations (runtimeverification#2392)

* haskell-backend/src/main/native/haskell-backend: 21959d95 - Add instructions for running one test in Docker (runtimeverification#2456)

* haskell-backend/src/main/native/haskell-backend: 4195d948 - Removes sort checks for Map and Set during internalization (runtimeverification#2440)

* Predicates in the condition are now simplified

* haskell-backend/src/main/native/haskell-backend: c35bfa56 - Remove defined marker (runtimeverification#2380)

* haskell-backend/src/main/native/haskell-backend: 57ad3292 - Remove cabal.project.freeze (runtimeverification#2450)

* haskell-backend/src/main/native/haskell-backend: 66158c67 - Support the --bug-report and --no-bug-report options in kore-repl (#2462)

* haskell-backend/src/main/native/haskell-backend: f0d93ac5 - Use stderr for errors (runtimeverification#2458)

* haskell-backend/src/main/native/haskell-backend: 0427fae7 - Distinguish \bottom from stuck states (runtimeverification#2451)

* haskell-backend/src/main/native/haskell-backend: d136446e - Fix Strict performance (runtimeverification#2447)

* haskell-backend/src/main/native/haskell-backend: a4e55b2a - Remove IMP fragment tests (runtimeverification#2467)

* haskell-backend/src/main/native/haskell-backend: 1f61e5a6 - Revert PRs related to InternalAc, Unit, Element & Concat symbols changes (runtimeverification#2463)

* haskell-backend/src/main/native/haskell-backend: fcfc2d52 - Remove the EvaluatedF marker from TermLike (runtimeverification#2469)

* haskell-backend/src/main/native/haskell-backend: fb56d719 - Revert PR runtimeverification#2334 (runtimeverification#2473)

* haskell-backend/src/main/native/haskell-backend: bb258f14 - Add ref = "main"; to default.nix (runtimeverification#2475)

* haskell-backend/src/main/native/haskell-backend: 964e64e7 - Update dependency: deps/k_release (runtimeverification#2464)

* haskell-backend/src/main/native/haskell-backend: abf14770 - Emit a warning when kore-exec exceeds the depth limit (runtimeverification#2461)

* haskell-backend/src/main/native/haskell-backend: 003a8424 - Update dependency: deps/k_release (runtimeverification#2478)

* haskell-backend/src/main/native/haskell-backend: 485bd89a - kore-0.42.0.0 (runtimeverification#2477)

* Add definedness to lookup rules, regenerate tests

* haskell-backend/src/main/native/haskell-backend: 78515d10 - Update dependency: deps/k_release (runtimeverification#2486)

* Revert changes to domains.md and test output

* haskell-backend/src/main/native/haskell-backend: 4f3a751c - Format code with fourmolu (runtimeverification#2382)

* haskell-backend/src/main/native/haskell-backend: de80594b - Update dependency: deps/k_release (runtimeverification#2490)

* Update map symbolic Haskell tests

* haskell-backend/src/main/native/haskell-backend: 9c9ef914 - Update dependency: deps/k_release (runtimeverification#2495)

Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com>
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants