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 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.


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