[isabelle] libisabelle: Status update and call for proposals
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] libisabelle: Status update and call for proposals
- From: Lars Hupel <hupel at in.tum.de>
- Date: Mon, 14 Dec 2015 20:53:44 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.4.0
on Sunday, I released a new version of libisabelle. Since the initial
announcement in February, a lot of things happened, mainly driven by my
stay at EPFL over summer. In fact, the Isabelle/Leon integration is
powered by libisabelle.
Major features are:
- bootstrapping: downloading and setting up a working Isabelle
installation on all three supported platforms, given an existing JVM
- multi-tenancy: managing different Isabelle instances on the same JVM
- multi-version: support for Isabelle2014 and 2015; JDK â 7; Scala
2.10.x and 2.11.x
All of this is regularly and automatically tested on Windows, OS X and
Plans for the near future, in decreasing order of importance (and
coincidentally, also in decreasing order of immediate utility to regular
- Component management for Isabelle to be able to fetch non-AFP
developments easily (for example: IsarMathLib, IsaFoR, Autocorres),
including a command-line interface and hooking into the regular Isabelle
- Offering parts of Isabelle/Pure and Isabelle/HOL as Scala API,
including term manipulation, definitional packages and tactics.
- Seamless remoting for libisabelle applications (e.g. Leon).*
I'm also soliciting feedback with this mail. If there's anything you'd
like to see implemented or if you have any use cases, please do tell!
* Note that Isabelle/jEdit isn't and presently can't be a libisabelle
application. Hence, a PIDE display protocol as postulated by Makarius
is not within the scope of this project (unless someone not-me volunteers).
This archive was generated by a fusion of
Pipermail (Mailman edition) and