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
editing.

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.

Regards,
GB







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.