On Mon, 16 Sep 2013, Josh Tilles wrote:
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)
Main Isabelle/HOL is a bottle neck in several respects, even just the
performance of doing the proofs (with or without explicit proof terms).
Below its Main theory any change requires someone with a few years of
experience to make non-trivial changes -- otherwise the bootstrap process
might get affected one way or the other. Between Main and Complex_Main it
is a bit easier, but a change there still requires to rebuild almost
anything else (this takes about 1-2h these days, where such things are
really fast compared to past times).
It is much more relaxed and fun to look through outlying, presently hardly
maintained areas, where some gems might be uncovered without getting into
technical difficulties.
In preparation of the Isabelle2013-1 release, I am myself training my
fingers (and testing the Prover IDE real-time dynamics) on
HOL/Multivariate_Analysis. These huge and mostly unformatted theories now
work out rather smoothly, even on my old 2-core MacBook Pro.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
