cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

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

Open mn200 opened this issue 6 years ago • 0 comments

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.

mn200 avatar Jan 08 '20 06:01 mn200