On Wed, Jul 31, 2013 at 9:55 AM, Makarius <[email protected]> wrote:
> On Tue, 30 Jul 2013, Josh Tilles wrote: > > QUESTION STATED BRIEFLY: >> If I convert existing proofs in src/HOL/**.thy from apply-style to >> Isar-style, would those changes be welcome in the main repository? >> > > It depends which part of the repository are affected. To get changes > accepted, someone who is an "expert" on that area of sources needs to apply > them. Finding out works by broadcasting here on this mailing list. That sounds perfectly reasonable. Should I share my changes by just attaching patches the "broadcasting" emails? > (Changes in main HOL are always critical, since almost everything else > depends on it, also performance-wise.) Interesting—I had assumed that changing the proof of a lemma and/or theorem had no functional impact on the code once said lemma/theorem had been verified. Am I incorrect about that? (If the explanation is complicated, please don't feel obligated to go into complete detail. A one-word answer will tell me all I probably *need* to know. Any further explanation would just be to satisfy my beginner's curiosity) > > > > EXPLANATION/DETAIL: >> >>> From what I've read in the documentation, structured Isar proofs are >>> >> preferred over apply-style proofs in every case except for >> prototyping/experimentation. >> > > Unstructured proof scripts (now called "apply style) and structured Isar > proofs are historically, technically, conceptually somehow related, > although in retrospect this is somehow accidental. The Isabelle/Isar > system was made in a way to include the old script style as "guest" to the > new approach. This worked so smoothly that people sometimes think that > Isar is still about "proof scripts", but it is actually about "proof > documents". > > Moving back and forth between the two styles works for many Isabelle > experts after some practice, although my impression in recent years is that > it would be better to teach people just one style from the start, and not > pretend that one is a prerequisite to the other. (E.g. in Isabelle2013 > 'by' no longer needs to be broken up into 1-2 'apply' to diagnose its > failure.) > > There is a long story behind that, of how the system presents it by > default and how the manuals are written. And it is getting more and more > off-topic for isabelle-dev, which is about the development process, and > exploring / testing intermediate Isabelle snapshots between official > releases -- i.e. the everyday struggles with ongoing changes, not a relaxed > discussion about the big picture. I apologize if I brought up an already over-discussed topic. If I have any further questions about "proof scripts" vs "proof documents", I'll begin in the isabelle-users mailing list. > > > > Makarius >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
