verify an Isabelle proof from the command line

Question

How can I verify that a *.thy file is a valid Isabelle proof from the command line? Doing it in the GUI amounts to seeing that there are no issues/errors/warnings etc, I guess. But is there a way to do it from the command line?

Answer 1

You just have to write a small ROOT-file and then invoke isabelle build. E.g., if you want to check that theories Foo.thy and Bar.thy compile, then you create a file with name ROOT with the following content:

session Test = HOL + 
theories
  Foo
  Bar

Then the compilation can be done via

isabelle build -d. Test

See the Isabelle system manual (Chapter 2) for more details.