Re: [isabelle] few questions about Isabelle/jEdit



The batch mode is when Isabelle is not running in interactive mode. Similarly, you check a theory when you build a heap image or build the documentation for it. If ever there is an error in a theory, the whole process will fail. Most people want to at least produce a PDF file for their theories, so the theory is always checked this way.

To understand all of this, you may have a look at “The Isabelle System Manual” which is the file `doc/system.pdf`.


Le Sun, 20 Apr 2014 16:04:56 +0200, noam neer <noamneer at gmail.com> a écrit:

thanks.

how do I run it as batch job on windows ?


On Sun, Apr 20, 2014 at 2:20 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

Everything is processed in parallel under the assumption that everything
above has been processed okay. It is quite normal for processing to reach the end of the file even though significant parts of proofs are continuing to execute. You need to check that there is no red anywhere in the sidebar.
The definitive test is to run it as a batch job.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.