[isabelle-dev] AFP/HLDE

[Makarius]

What is the purpose of the session HLDE, with its duplicate theory
Solver_Code that is also in Diophantine_Eqns_Lin_Hom?

I've had seen odd crashes due to its non-temporary output into
ISABELLE_TMP, but the technical problem behind it might be actually in
Isabelle/Scala (rm_tree):

Exception in thread "process_manager" java.nio.file.NoSuchFileException:
/tmp/isabelle-mawenzel/process7653301744367976304/HLDE/Main.hi
        at
sun.nio.fs.UnixException.translateToIOException(UnixException.java:86)

(Isabelle/742c88258cf8 + AFP/854bc290d72b + a derivative of "isabelle
dump" that is not in these repositories).


The HLDE session also touches the open question how to deal with
generated material in AFP. We have already a concept for "exports" in
Isabelle2018 (see NEWS). Maybe that is already sufficient that we can
make such sessions pure in the sense that nothing is written into odd
places in the file-system, only into the formal session database.


	Makarius