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

Lars Hupel lars at hupel.info
Fri Jan 1 18:16:20 CET 2021


> 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/>)


More information about the isabelle-dev mailing list