Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] libisabelle: Status update and call for proposals

Email Gateway (Aug 22 2022 at 12:02):

From: Lars Hupel <hupel@in.tum.de>
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).

Last updated: Nov 21 2024 at 12:39 UTC