[isabelle-dev] new isabelle interface

[Chris Capel]

Wow. What a bunch of replies I've stirred up. Now I almost feel
obligated to actually *do* something.

On Mon, Aug 25, 2008 at 04:58, Makarius <makarius at sketis.net> wrote:
>  * The Isabelle distribution also provides some tightly fit layer to
>    integrate the prover process into the JVM platform, targeting mostly
>    Scala as source language.  See also http://www.scala-lang.org/ about
>    the latest innovations in the JVM world.

Well that's bad news to me, considering I'm more of a .NET person
myself, but the world turns, and I know enough java to get by.

> On Sun, 24 Aug 2008, Chris Capel wrote:
>> I plan to use SML.NET to compile Isabelle. Does anyone forsee any
>> problems with this? Is Isabelle's code fairly portable across Standard
>> ML compilers?
>
> I would be surprised if it will work as expected.  For Isabelle you need
> the old-fashioned dynamic-compilation mode that allows to invoke the
> compiler at any point at run time.  Can SML.NET do that?

I believe that basically any .NET language can do this, though there's
more overhead involved than in a language *designed* to support this
from the ground up. But even still, I think dynamic method compilation
has seen improved support in the 2.0 version of the framework (and
thus, the 3.0 and 3.5 versions, which don't change that part).

> Moreover, our Poly/ML platform has quite good performance, including
> proper parallel execution on multiple cores.  (We will use more of that
> soon.)  I don't think you will get to the same level of Poly/ML
> performance on .NET without some fundamental rearrangements.

Well, with .NET you use the .NET threading model, which gives you
native threading performance, at least on Windows, but probably on
Linux as well. The only concern is how to handle supporting both
threading models cleanly in the Isabelle source. I'm not familiar with
the differences between .NET threads and POSIX threads.

Of course, this is all assuming I'm trying to get Isabelle compiled
under SML.NET, which would be nice since it would remove the
requirement of cygwin. But there are other ways not to require cygwin
with which Poly/ML could still be used as the compiler. C# could still
be the language used to implement the GUI, and use a pipe of one kind
or another to communicate with the prover process, which is probably
desirable anyway, as you mention.

But really, my main motivation for using SML.NET is that it would
allow me to examine the isabelle sources more closely using more
familiar tools than I would otherwise have available. :) So perhaps a
fully functioning .NET version isn't really important.

> The latest sources are always available via
> http://isabelle.in.tum.de/repos/isabelle/ which even allows you to
> subscribe to the changelog via RSS/Atom, so you can immerse yourself in
> tons of fine-grained change messages :-)

You have mentioned CVS a few times, and yet that link refers to
Mercurial. Is that a read-only mercurial mirror?

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)