The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here's another diff:  https://github.com/mit-plv/fiat-crypto/commit/fa027c4a37ed455a26a5bb12c6f3d54ae4bd8774

The main "generator" file for this change is src/Reflection/Syntax.v.  I removed one constructor, and ended up having to touch about 2000 lines of code.  A lot of these changes were extremely routine (the inductive type now took one less argument, because a context variable was used only in that constructor, so I had to remove that argument in every place the inductive appeared), and it'd be nice to have a tool to do this for me.  Is your tool ready for consumption yet?

On Tue, Jan 17, 2017 at 3:53 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Here's a more traditional example: https://github.com/JasonGross/catdb/commit/209231ae3e94d5dbbc678c94930dcf585d53d555  (Coq 8.4). Basically, I changed [Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := Build_SpecializedCategory' { Obj :> _ := obj ; ... }.] to [Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' { Obj :> _ := obj ; Morphism' : obj -> obj -> Type;  ... }.], and had to change about 1300 lines of code.

On Tue, Jan 17, 2017 at 3:17 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Does "I changed the version of Coq" count as a small change in definitions?  If so, here are a bunch of diffs that were "oops, my last commit broke compatibility in Coq 8.4, but worked fine in Coq 8.5, here's a fix": https://github.com/mit-plv/fiat-crypto/search?p=1&q=8.4&type=Commits&utf8=%E2%9C%93  (Here are some more: https://github.com/mit-plv/fiat/search?p=1&q=8.4&type=Commits&utf8=%E2%9C%93 )

On Tue, Jan 17, 2017 at 3:07 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

I'm currently working on a research project to make proof assistants less brittle, so that when you make a small change that breaks existing proofs, I can automatically fix those proofs.

I've made progress with small examples. Now I'm looking for real diffs from Coq projects to help bring this project to the next stage. In particular, I'm looking for any diff in which you have made a small change to one of your definitions or theorems, and as a result you have had to change several proofs that have depended on those definitions or theorems. I'd like code from before and after the change.

If you have any diffs that may be useful, please send them my way.

Best,

Talia

University of Washington
http://tlringer.github.io