[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