coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle
Date: Tue, 17 Jan 2017 21:05:48 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wm0-f68.google.com
Ironport-phdr: 9a23:pC9RzB39sHSq+cf0smDT+DRfVm0co7zxezQtwd8Zse0TLPad9pjvdHbS+e9qxAeQG96Kt7Qf1KGP6PuocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbal8IRi0ogndq8cbjIV/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIfM+lCq4n9pkEBpgaiCwmtAuPvxSFHhmXr1qA9z+QhCwDG3AovH90QqnTZt8n6NLwIXeG71qbI1jXDb/JQ2Tfy9IjIdRYhreuSUr1tbMrc0E8iHB7LgFWXrIzqJTKV1uIVvmiU7upgSeKvi3M8pA1rozivwcEhgZTKiIIN0l3J9yp0zJwoKdGmSEN3e92pHIVKuyybNIZ7RN4pTXtytyYg0LIGvIa2fCgUx5QjwB7Sc/mHfJKJ4hLnTeqQLzJ4iG58dLKxhhu/8lKsyuL7Vsmz31ZKqjRKnsPQuXAK0hzf8smHSv1j8Ue9wTuC1Q/e5vtZLUwqlafXMZ0szqAqmpcSsknPBir2l1/3jK+SeEUk4O+o6+H/b7X6vJ+cNol0ig7gPaQ0gcGwHf84PhIAXmeB4uS81Lzj/Uv2QLVWif02lLPVv47HKsQGvqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsDwWwwu+vMtR72Y4EETaTGK6fP67ImVSToP0mOOmNYoAJvzC7JvQ4sa29xUQlkEMQKPH6laAcb2q1S6xr

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

[Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle, Talia Ringer, 01/17/2017
- Re: [Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle, Jason Gross, 01/17/2017
  - Re: [Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle, Jason Gross, 01/17/2017
    - Re: [Coq-Club] Looking for Coq diffs for a project to make proof assistants less brittle, Jason Gross, 01/20/2017