[isabelle-dev] Reasons mira crashes
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:
> 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
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