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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev