[isabelle-dev] Reasons mira crashes

Makarius makarius at sketis.net
Thu Nov 29 11:49:15 CET 2012

On Thu, 29 Nov 2012, Alexander Krauss wrote:

>> For future changes it might be worth to keep in mind that the Mercurial 
>> project considers the python interface as internal:
>> http://mercurial.selenic.com/wiki/MercurialApi
> Right. This classification has somehow changed over the years. Back in 
> 2008, use of the API was encouraged more. Switching to a CLI interface 
> requires a bit of work, though.

Just to recall the original motivations for using Mercurial instead of Git 
(which was not as aggressible marketed in 2008 as now so there was a 
genuine choice to be made):

   (1) Mercurial emphasizes a nice semantic model of monotonic history and
       immutable changes (in coincidence with the Isabelle/ML approach and
       the then emerging PIDE document model).

   (2) Mercurial was positioned as a nice Python library/API, not a
       collection of shell scripts and C-programs.

       We even had a perspective to make Pyhton our main "lambda calculus
       approximation for system programming".  Mira is fully on that line,
       although the "lambda calculus" of Python turned out as very
       approximative indeed.

So both has shifted a bit over time.

Influenced by the crowds behind Git, Mercurial has made non-monotonic 
operations more easily accessible than before, say via some "rebase" 
option to formerly pure hg commands.  Thus it is no longer obvious which 
operations are pure and which are impure.  (The emerging DVCS GUI 
front-ends help out a bit here.)

The slight tendency away from Python APIs is another thing.  Since 
Isabelle/Scala is the official system programming language for quite some 
time already, I've occasionally checked the situation for JVM-based access 
to Mercurial operations.  Projects like http://hg4j.com/ are not very far 
yet.  Also interesting is http://mercurial.selenic.com/wiki/CommandServer 
which is a third way to the API vs. external executable problem: some hg 
process is started once and used with a certain protocol over the pipe.

I would like to see a Scala wrapper for that ...


More information about the isabelle-dev mailing list