I am new to Isabelle and now trying to do a proof using the command line of Cygwin to measure the time needed to prove a lemma.
What would be the best and easiest way to do that?
I would expect there is a command like: "isabelle theory_file.thy", but having run through The Isabelle System Manual I got a feeling that everything is much more complex than that and got lost eventually.
So I have a theory file and am looking for a way to start a prove process with the Cygwin terminal included to the Isabelle2016 distribution for Windows.
Every piece of advice or direction I need to look to is highly appreciated. Thanks in advance.
If you just use the normal Prove IDE (Isabelle/jEdit), you can get timing information for individual commands as follows:
CONTROL-hover over the command keyword: timing is displayed for commands that take measurable time (more than 1 millisecond).
The Isabelle/jEdit menu item "Plugins / Isabelle / Timing" provides a separate Timing panel for theories and commands, see also the Isabelle Documentation with the label jedit.
If you really need batch-mode timing of while sessions (with all theories therein), the easiest way is via isabelle build -v. See the system manual about that (in section "Isabelle sessions and build management").
Note that everything runs in parallel by default, so timing results always need sensible interpretation.