Isabelle2016 and command line

1
votes

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.

1
cygwinisabelle

1 Answers

1
votes

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.