Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

Implement definition alignment/assignment #31

Closed a-gardner1 closed 1 year ago

a-gardner1 commented 2 years ago

Given the prism.data.build_cache.ProjectCommitData of two commits, assign the definitions of one commit to the definitions of the other with the goal of ensuring that the assignment preserves the semantic identity of each definition. Definitions that have been removed or added between each commit are not included in the assignment.

Since there are likely to be hundreds of definitions, calculating the assignment between the unconstrained sets is prohibitively expensive. Instead, one may use the diff between the commits to limit the size of the sets for whom a nontrivial assignment must be calculated to just those definitions that intersect the lines in the diff (with the assumption that the size of the diff is much less than the size of the overall project to realize any performance gains). Definitions that do not intersect the diff may be trivially assigned by an identity map over their corresponding indices.

The following ingredients are expected to be critical to enabling a successful implementation:

The following subtasks are requested (feel free to slightly adapt them if it simplifies the implementation or improves quality of life for a user/maintainer):