Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Enable options for controlling booster execution #2243

Merged
merged 21 commits into from
Feb 7, 2024
Merged

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented Jan 9, 2024

Blocked on: runtimeverification/pyk#804
Blocked on: #2236
Blocked on: #2269

This PR takes advantage of a few new features introduced in pyk, and makes a few updates to CLI and testing options:

  • Option --fast-check-subsumption allows a faster way to check that a node will definitely not be subsumed into the target.
  • Option --always-check-subsumption allows checking even non-terminal node for subsumption.
  • Options --[no-]post-exec-simplify allows telling the booster to not call the old backend to simplify states that it produces before handing them back to pyk (see (Dev.) Options to control fall-back reasons and post-exec simplification hs-backend-booster#436).
  • Option --fallback-on allows the user to specify the fallback reasons the booster will consider (see (Dev.) Options to control fall-back reasons and post-exec simplification hs-backend-booster#436).
  • Option --interim-simplification allows the user to specify how frequently to invoke the full simplifier on the execution state.
  • By default, all breaks are turned off for testing purposes (which mimics CLI behavior better). Before, we had break_on_calls set to True for testing/CI behavior, but False for CLI behavior, which made it hard to track down a bug.
  • An option --spec-name is added to make test-prove-pyk ... pytest testsuite, which allows filtering for a specific specification to run in the testing harness environment (much faster to narrow down to specific test that way).

@ehildenb ehildenb self-assigned this Jan 9, 2024
@yale-vinson
Copy link

It looks like you and Andrei have had some back and forth on this one. Is there an ETA to merge this one?

@yale-vinson yale-vinson added the enhancement New feature or request label Jan 24, 2024
@ehildenb ehildenb marked this pull request as ready for review February 7, 2024 19:58
Copy link
Contributor

@anvacaru anvacaru left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved with a typo fix. 👍

kevm-pyk/src/kevm_pyk/cli.py Outdated Show resolved Hide resolved
@rv-jenkins rv-jenkins merged commit e2d5d20 into master Feb 7, 2024
11 checks passed
@rv-jenkins rv-jenkins deleted the breaking-steps branch February 7, 2024 21:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
automerge enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants