Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
I have to graduate
This is the first official versioned release of PUMPKIN PATCH, now featuring ornaments!
PUMPKIN PATCH is no longer just a plugin. It is a plugin suite. It includes DEVOID, the paper for which can be found here. The README has been update with information on the plugins that PUMPKIN PATCH contains.
PUMPKIN PATCH itself is still a prototype. A lot more functionality is coming soon, and existing functionality will be improved upon. In the meantime, though, DEVOID opens up a whole new host of possibilities---and all of the functionality described in the DEVOID paper can be used from within PUMPKIN PATCH.
Enjoy!
Update PUMPKIN PATCH to Coq 8.8.
Update PUMPKIN PATCH to Coq 8.6.
Code in a frozen state from the CPP 2018 paper "Adapting Proof Automation to Adapt Proofs."