Email Gateway (Aug 19 2022 at 10:04): Email Gateway (Aug 19 2022 at 10:04):From: Rafal Kolanski <xs@xaph.net>
So, here is a minimal patch to get the wwwfind tool working again. It
helps that there was nothing wrong with the code itself, only the way it
was being invoked.
For those who care: when working with isabelle-process directly, the
following scenario breaks:
use_thy "MyTheory"; MyStructure.blah ();
i.e.
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.
I would be interested in the current canonical way to write isabelle
tools which take some parameters, pass them to ML code to do stuff, then
at some future point exit. The old route of
isabelle-process -r -e "use_thy \"my_thy\"; Thing.do_stuff \"$PARAM\";"
appears deprecated. This took me a while to grasp.
Keeping a back door to make this pattern possible will make it easier to
keep the ML tools going which are unlikely to be rewritten in scala
anytime soon.
Makarius:
I don't know what your plan for the "ROOT" file in WWW_Find is. I have
assumed that it is for testing purposes, so that "isabelle build" will
run over the ML files and make sure they at least typecheck. Thus I have
left it, and WWW_Find.thy unchanged, creating a "launcher" in
Start_WWW_Find.thy.
If my assumption is incorrect, you can delete ROOT and merge
Start_WWW_Find.thy into WWW_Find.thy quite easily.
Any other problems, let me know.
On 11/02/13 21:20, Makarius wrote:
There is also the Isabelle system manual, with a whole chapter on
Isabelle sessions and build management, including real-life examples.
Yes, I know. I just assumed that "build" builds an image, got it wrong
and apologised.
I'll go back to fixing wwwfind now, which definitely does not work.
You have approx. 24h left. I had reported its broken state almost 3
months ago. The Isabelle2013 release train will not wait for latecomers.
Please don't treat me as if I broke it.
Sincerely,
Rafal Kolanski.
wwwfind.patch
Email Gateway (Aug 19 2022 at 10:05):From: Makarius <makarius@sketis.net>
Nobody cares who "broke" it. This is not how software maintenance works.
Makarius
Email Gateway (Aug 19 2022 at 10:05):From: Makarius <makarius@sketis.net>
I've looked only briefly, to understand what it does. Should there be a
static Start_WWW_Find.thy in the changeset? It is missing. (Or is it
somehow dynamic?)
Makarius
Email Gateway (Aug 19 2022 at 10:05):From: Rafal Kolanski <xs@xaph.net>
I apologise, I neglected to add it in the isabelle-release repository.
Here it is again.
Rafal Kolanski.
wwwfind.patch
Email Gateway (Aug 19 2022 at 10:05):From: Makarius <makarius@sketis.net>
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
description:
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.
Makarius
Email Gateway (Aug 19 2022 at 10:05):From: Makarius <makarius@sketis.net>
OK, it is now here
https://bitbucket.org/isabelle_project/isabelle-release/commits/d90218288d51
I can confirm that it works on Linux (as specified). Being curious about
its exclusion of Mac OS X and Windows/Cygwin, I've tried the other
platforms as well, and it did not work (also as specified). The problems
seem to be unportable netstat options (Mac OS X) and other unknown
differences on Cygwin (although netstat and lighttpd are the same there as
on Linux).
So we are back to the status-quo of WWW_Find for the Isabelle2013 release.
Makarius
Email Gateway (Aug 19 2022 at 10:05):From: Makarius <makarius@sketis.net>
On Mon, 11 Feb 2013, Rafal Kolanski wrote:
The old route of isabelle-process -r -e "use_thy \"my_thy\";
Thing.do_stuff \"$PARAM\";" appears deprecated.
Deprecation probably goes back to 2007/2008, when "the_context" was the
best-known Isabelle insider joke. Whatever you do in Isabelle, it somehow
works within the formal context, including ML.
There are various ways to ensure that some ML runs within an existing
theory context. The Start_WWW_Find.thy approach looks fine in this
respect.
Keeping a back door to make this pattern possible will make it easier to
keep the ML tools going which are unlikely to be rewritten in scala
anytime soon.
When WWW_Find was implemented first several years ago, I pointed already
out that its technology was outdated. You don't do a HTTP server in ML.
The shell scripts around it only work on Linux.
The JVM platform is much better at such things, and TCP clients and
servers usually work uniformly (in contrast to Swing GUI stuff).
Isabelle/Scala is not an exotic Isabelle add-on that will emerge
eventually -- that was in 2008/2009. It is here right now, as the
standard Isabelle system programming interface.
I don't know what your plan for the "ROOT" file in WWW_Find is. I have
assumed that it is for testing purposes, so that "isabelle build" will
run over the ML files and make sure they at least typecheck.
The ROOT file is merely the result of porting the old ROOT.ML. It has
been there from the beginning of WWW_Find to have at least a static test
of its code-base.
There was never a proper dynamic test of it. 3 months ago, I realized
that it was broken, and was trying to find its maintainer. Even now, I am
unsure if it is actually maintained.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC