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