c.sternagel at gmail.com
Fri Oct 5 20:20:09 CEST 2018
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).
> 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:
> (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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev