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
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:
date: Wed Jul 25 10:55:02 2012 +0200
files: lib/scripts/getsettings src/Tools/WWW_Find/ROOT
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