6

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?

2 Answers 2

6

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.

3

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.

2
  • 1
    What does Praktomat do now that secure mode doesn't exist anymore?
    – larsrh
    Commented Mar 5, 2018 at 13:31
  • 1
    I guess the Isabelle support there is a bit stale :-) Commented Mar 5, 2018 at 14:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.