[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"
makarius at sketis.net
Sat Jan 2 00:12:14 CET 2021
On 01/01/2021 18:16, Lars Hupel wrote:
>> The approach looks right: a theory context manages shared resources according
>> to the import graph structure.
> Sadly we now have a "total existence failure", as evidenced in
> It appears that the JVM process just hangs when (or after) building the
> document for the Network_Security_Policy_Verification session.
> (Logfiles and Session DBs are available for download:
I have stared at "consoleFull" a few minutes without spotting anything suspicious.
In Isabelle/38528017e4c8 there is some more verbosity, to see where it gets
stuck --- if it is repeatable at all.
Note that I did manage to build Isabelle + AFP with pdf + HTML several times
on other big machines, using settings like this:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1g -Xmx8g -Xss16m"
More information about the isabelle-dev