Terminal nodes being rechecked every load

Open
#4,213 3 comments 0 reactions 1 assignee View on GitHub

@nwatson22 is already working on this.

Since Apr 24, 2024.

Assessment

This issue has not been assessed yet.

Description

pyk

As an example, when loading a proof that depends on another proof (via the depends(...) directive for KClaim), we get messages that look like this:

image

This isn't necessary, takes some time at load (not much), and clutters the log. When loading a proof written to disk, we should just assume that the input data is valid if it's in the correct format.

Dominant language
Python
Stars
591
Forks
163
PR merge metrics
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.