Re: [isabelle] Automating the auto-tools
On 7/21/2012 1:52 PM, Makarius wrote:
You can also control the range of checking a little bit: the Prover
Session panel has a "Check" button, which tells to prover to check the
whole of the current buffer, until you "Cancel" or recommence normal
I'm not editing big files yet, although they've become big enough that I
try not to do a save on a file in my other editor, or jEdit will reload
the whole thing and prove it all from the top.
I'll try to remember the check button, but I forsee building up theories
hierarchically so I can build the heap for what I'm doing. For anything
that's in the heap, speed's not a problem, as far as I can tell. Speed
problems for sessions in src/HOL went away after I built the heap for them.
The way you have things working is not a problem with me. I've started
to use 2 views as my standard setup. The edits stay in sync, and the
prover for the two views is the same prover.
Any keystroke in a file that my test file imports causes the prover to
start over in that file, but I now create a copy of my working file for
my tester file to import, so that doesn't happen.
The continuous prover works good for me. I don't have any longing for
manually stepping through a theory like in PG, but I have decently fast
computer. It's not extraordinarily fast. It's an i3 with 16GB of ram.
This archive was generated by a fusion of
Pipermail (Mailman edition) and