Re: [isabelle] RC3: patch to get wwwfind running again
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and