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.

Sign up for GitHub

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

Jump to bottom

[Feature request] API-level provenance recording #248

Open

NicolasRouquette opened this issue Mar 11, 2023 · 0 comments

Collaborator

NicolasRouquette commented Mar 11, 2023

Is your feature request related to a problem? Please describe.

A global Pacti toggle to record the API-level provenance of contracts and terms.

Describe the solution you'd like

There are two scenarios where API-level provenance recording will be useful:

For troubleshooting purposes where it would be useful to replay the API-level recording under the debugger to diagnose a problem with a particular contract or term.
For pedagogical purposes where it is important to explain the nature of Pacti's operations and how they differ from notions like quantifier elimination.

Additional context

This provenance recording depends on term and contract ID support: #247

NicolasRouquette mentioned this issue

[Feature request] Add support for Term and Contract ID #247

Closed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment