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

Translator state should be stored as per-theory deltas (at least for load/save) #717

Open
mn200 opened this issue Jan 8, 2020 · 0 comments

Comments

@mn200
Copy link
Contributor

mn200 commented Jan 8, 2020

Currently, the translator dumps all of its state to "disk" with every export theory, when really, it should just dump the changes (new stuff) to disk and then have the loading of theories incrementally build the whole required state. This would mimic the way things like the stateful simpset is built from per-theory sets of theorems.

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

No branches or pull requests

2 participants