Re: [isabelle] RC3: patch to get wwwfind running again

On Mon, 11 Feb 2013, Rafal Kolanski wrote:

For those who care: when working with isabelle-process directly, the
following scenario breaks:
use_thy "MyTheory"; MyStructure.blah ();
1. passing use_thy "MyTheory" to isabelle-process
2. MyTheory uses ML_file "blah.ML" to define ML structures
3. trying to refer to structures from (2) after the use_thy from (1)

I don't know why exactly this is (due to contexts and thread safety?),
but I don't object to it. Just makes it hard to pass parameters in.

It is just the normal context discipline of Isabelle: everything is stored as a value within the theory (or other context). Until approx. 2008 ML values were not treated properly like that -- it was an old snag going back to pioneering days of Proof General, when one could not undo ML bindings.

For multithreaded Isabelle/ML (which became the default in Isabelle2008) there was indeed no more way to ignore this. So David Matthews and myself spent some time to solve this problem once and for all: runtime invocation of the ML compiler (via 'ML' commands or 'ML_file' in Isabelle2013) happens within the theory context.

The reason why WWW_Find broken down after such a long time is here:

changeset:   48495:bf5b45870110
user:        wenzelm
date:        Wed Jul 25 10:55:02 2012 +0200
files: lib/scripts/getsettings src/Tools/WWW_Find/ROOT src/Tools/WWW_Find/ROOT.ML src/Tools/WWW_Find/WWW_Find.thy
more standard session setup for WWW_Find;

This discontinues the old ROOT.ML with its implicit global context -- there was no way around it in the new isabelle build system.

It thus indirectly broke WWW_Find, or rather exhibited the latent problem that has been there for a long time. Or rather, it was probably not even a problem when WWW_Find was first implemented. It is totally normal that side-conditions are gradually changing, and thus one improvement here and another improvement there, or lack of improvement, eventually cause a breakdown. Then things need to be renovated.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.