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
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.
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.
-
1What does Praktomat do now that secure mode doesn't exist anymore?– larsrhCommented Mar 5, 2018 at 13:31
-
1I guess the Isabelle support there is a bit stale :-) Commented Mar 5, 2018 at 14:45