[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

[Makarius]

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
> 
> <https://ci.isabelle.systems/jenkins/job/isabelle-all/2573/consoleFull>
> 
> 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:
> <https://ci.isabelle.systems/jenkins/job/isabelle-all/2573/artifact/heaps/polyml-5.8.2_x86_64_32-linux/log/>)

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"

  ML_PLATFORM="x86_64_32-linux"
  ML_OPTIONS="--minheap 1500"


	Makarius