Dear Makarius On 10/05/2018 07:10 PM, Makarius wrote: > What is the purpose of the session HLDE, with its duplicate theory > Solver_Code that is also in Diophantine_Eqns_Lin_Hom?
As the author of the corresponding ROOT file, when I look at it now, I cannot think of any reason to have also session HLDE (except of course the shorter name). cheers chris > > 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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
