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

Proof summary improvements #1216

Merged
merged 18 commits into from
Jun 2, 2021
Merged

Proof summary improvements #1216

merged 18 commits into from
Jun 2, 2021

Conversation

robdockins
Copy link
Contributor

Some initial steps toward improving proof summaries. This currently involves tracking additional metadata about the origin of theorems and preliminary steps toward tracking dependencies between proofs.

@robdockins robdockins marked this pull request as ready for review May 18, 2021 19:02
@robdockins robdockins requested a review from brianhuffman May 18, 2021 19:02
@robdockins robdockins force-pushed the proof-summary branch 2 times, most recently from d078994 to 0e496b0 Compare May 21, 2021 22:37
@robdockins robdockins requested a review from atomb May 26, 2021 21:30
Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

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

Thanks for doing this! I like that it provides a mechanism for validating evidence. I think adapting the RPC API to avoid creating simpsets out of raw terms, too, would be a good way to go.

@@ -154,7 +154,7 @@ makeSimpset params = do
v <- getServerVal n
case v of
VSimpset ss' -> return (merge ss ss')
VTerm t -> return (addSimp (ttTerm t) ss)
VTerm t -> return (addSimp (ttTerm t) Nothing ss) -- TODO! making rewrite rules from terms!
Copy link
Contributor

Choose a reason for hiding this comment

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

Maybe we should just remove this case. I don't think it'll break any existing proofs, and we can add convenience functions for proving and then making simpsets from terms in the Python client.

robdockins added 18 commits June 2, 2021 12:37
This allows users to add metadata their rewrite rules,
and have rewriting steps record and return the metadata
for rules what were actually used in rewriting.

The intention is to use these annotations to link rewrite rules
back to theorems/axioms that generated them so proof steps
can determine the dependencies of a proof.
Currently, we use trivial `()` annotations and ignore annotations
collected by rewrite steps. The plan is to allocate unique nonces
for each theorem and use those to track theorem dependencies.
TODO! We currently are allowing users to create simpsets from
raw terms, and probably we should only let `Theorem` values
be turned into rewrite rules.
Instead, users should use `core_axiom` or `prove_print (admit "...")`
to turn terms into theorems for use with `addsimp` or `addsimps`.
Add a unique value to each generated theorem, and compute the
set of theorems a proof depends on while checking evidence.
Track the collection of all proved theorems during a run
in a `TheoremDB`; later we should be able to generate a
graph of theorem depencencies from this database.
specs that have been proved or assumed.
These are now output in JSON verification summaries.
We parse a verification summary JSON file and produce
a Graphviz file intended to be fed into `dot` to produce
a visulaization. For large proofs, especially, the layout
is problematic; however, even so, it seems like a helpful
way to scroll through a proof and get a sense of what is
proved and what depends on what.
displaying verification conditions of method specs.
This reduces clutter in the graph and produces more
readable output.
@robdockins robdockins added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 2, 2021
@mergify mergify bot merged commit cf78257 into master Jun 2, 2021
@mergify mergify bot deleted the proof-summary branch June 2, 2021 22:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants