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