CODEWITHSUNDEEP
command-lineisabelle
Yoni Zohar
Yoni Zohar

Reputation: 311

verify an Isabelle proof from the command line

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?

Upvotes: 6

Views: 911

Answers (2)

Joachim Breitner
Joachim Breitner

Reputation: 25763

If you want to avoid having to create a ROOT file, you might be able to do something like:

isabelle process -T Foo

But isabelle build is certainly the “more official” way.

Something similar (with a hackish dance to set the secure mode for some theories) is what the Praktomat does to submitted Isabelle theories.

Upvotes: 3

René Thiemann
René Thiemann

Reputation: 1271

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.

Upvotes: 6

Related Questions