[isabelle-dev] AFP/HLDE

[Christian Sternagel]

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