PLDI 2021 Release: PUMPKIN Pi

This is the release for our PLDI 2021 paper, "Proof Repair Across Type Equivalences." DEVOID is no more; it is but a special case of a more general tool that ports programs and proofs across equivalences!

Silent arXiv update

Not describing

Swapping and renaming constructors

DEVOID now supports swapping and renaming constructors of inductive types. In particular:

1. Find ornament can prove equivalences between two types that are the same up to reordering and renaming of constructors. It has some extra UI functionality to deal with ambiguity when there are multiple possible swaps.

2. Save ornament allows you to supply only one of promote or forget if you'd like, so that if you want to define the swapping relation yourself (sometimes easier if there are many possible swaps), you only need to write one direction and DEVOID will do the rest for you.

3. Lift now lifts across these relations as well.

See Swap.v for a walkthrough of some examples. Enjoy!

It's a new record!

Lots is new in DEVOID:

• Search and lifting between nested tuples and records
• Whole module lifting
• Smarter caching
• Configuration to set terms as opaque to optimize lifting
• An option for producing prettier types when lifting
• Better error messages
• A command to set your own equivalences (experimental)

An example of whole module lifting across records can be found here. Check it out!

ITP camera-ready

This release builds on the ITP submission release with a few new features:

• An option Set DEVOID search prove coherence to tell Find ornament to generate a proof of coherence
• An option Set DEVOID search prove equivalence to tell Find ornament to generate proofs of section and retraction
• Documentation and tests for these options
• An updated case study that:
  • Uses DEVOID's generated functions (the old case study was not doing this by mistake)
  • Uses DEVOID's generated equivalences
  • Uses a trick from a reviewer to produce more meaningful numbers that do not include printing time
• A few bug fixes:
  • SECTION/RETRACTION recurse into the algorithm as well
  • Lazy eta expansion is slightly smarter
  • Packing to deal with non-primitive projections is much smarter
• Extra documentation in existing examples, especially for user-friendly types
• Documentation for restrictions on inputs
• Lengthy, expanded README

Final state during ITP submission

This is the final state of the paper for the ITP submission.

The big change since the last release is that I've thought a lot about two things:

1. a methodology for user-friendly proof types that is independent of UIP holding on the index type
2. the implementation bugs in listToVect

While neither of these really take away from the ITP submission, I think they are natural questions people will have. I wasn't able to resolve either of those entirely; the former I think is really interesting work that further improves usability and that will take a little more time, and the latter is just some debugging that can wait until after the submission.

Consequentially, I've written comments linking to the issues tracking these, and I've added some of my thoughts in these issues.

Enable asynchronous processing

DEVOID now works with asynchronous processing in CoqIDE.

Better documented initial release with better examples

Generalize the theorem lift_pres_zip in the examples.

Better documented initial release

v1.1

Merge branch 'master' of https://github.com/uwplse/ornamental-search

Initial release

v1.0

Merge branch 'master' of https://github.com/uwplse/ornamental-search