[isabelle] libisabelle: Status update and call for proposals



Dear list,

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

Plans for the near future, in decreasing order of importance (and
coincidentally, also in decreasing order of immediate utility to regular
Isabelle users):
- 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
component mechanism.
- 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!

Cheers
Lars


* Note that Isabelle/jEdit isn't and presently can't be a libisabelle
application. Hence, a PIDE display protocol as postulated by Makarius
<http://sketis.net/2015/proposal-remote-prover-connectivity-for-isabellepide-2>
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 MHonArc.