Stream: General

Topic: running Isabelle in batch mode: how to use?

view this post on Zulip Chengsong Tan (May 15 2024 at 08:56):

Hi,
how do you make isabelle process generate all errors rather than stopping at the first error?
Currently when I run it on a theory file, it only outputs the first place where an error occurred,
for instance in the below example, only line 2424's error has been outputted, whereas I need the line 2430, 2432 to be printed out as well.
Screenshot-2024-05-15-at-12.32.20.png

Is there an 'error recovery' mode that allows processing of the entirety of a thy file?
quick_and_dirty mode doesn't work for this need.

view this post on Zulip Chengsong Tan (May 15 2024 at 09:31):

(deleted)

view this post on Zulip Chengsong Tan (May 15 2024 at 09:42):

(deleted)

view this post on Zulip Chengsong Tan (May 15 2024 at 09:46):

(deleted)

Last updated: Dec 21 2024 at 12:33 UTC