search

ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

CommitMsg? #165

Closed conal closed 8 years ago

conal commented 8 years ago

When using apply from HERMIT.Plugin, what does the CommitMsg parameter mean?

xich commented 8 years ago

Sorry, forgot to reply to this.

The CommitMsg argument specifies whether to record the rewrite in the history tree. If you don't care about being able to use step/goto/etc, you can pass Never. Always causes an entry to be added even if nothing changes, Changed only adds an entry if something changes.

(Always is useful for query when modifying the lemma store... which is a definite hack. Fixing it requires changing how the Kernel works.)

There is probably a better abstraction there... it was mostly hacked in during the run up to our last paper.

conal commented 8 years ago

Ah. Sounds like it's relevant some HERMIT territory I haven't discovered yet. Thanks for the explanation.