Re: [isabelle] Sledgehammer and Nitpick from the command line?

I think using a second session of jEdit with the environment set to a different home folder is the best solution for what I'm trying to do. Running things with a batch file sounds good as an idea, but there's a lot of interaction between jEdit and Sledgehammer that would be hard to duplicate.

The main way I keep in control is by entering "sledgehammer" when I want it to start, and otherwise, making sure the "sledgehammer" command isn't in the file. Sledgehammer is very eager to start running.

I have to make sure "sledgehammer" isn't in before trying to edit the file in any way. If I try to edit the timeout value with "sledgehammer" in, it'll jump down to the sledgehammer step after a single keystroke.

Also, if I delete "sledgehammer" while the provers are still running, it seems to be good at shutting them down. I'll see a process such as "eprover.exe" taking up 25% of the CPU processing, and when I delete "sledgehammer", it'll kill the process.

I start a second copy of jEdit with a different home folder, so it doesn't write over my main jEdit settings, and then I split the screen vertically four or more times with "View / Splitting / Split Vertically". I haven't gotten to the point where I try to run sledgehammer in 4 files and nitpick in 2 files all at the same time. That will require 7 split windows.

I haven't figured out how independent the continuous prover allows sledgehammer to be when running in two different files. I might need to start up 3 or more copies of jEdit

I'm trying to see if I can compile the prover satallax for Cygwin.


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