[isabelle-dev] NEWS: SQL database access in Isabelle/Scala

Makarius makarius at sketis.net
Mon May 15 17:35:52 CEST 2017

*** System ***

* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or full-scale server
(PostgreSQL via local port or remote ssh connection).

* Results of "isabelle build" are recorded as SQLite database (i.e.
"Application File Format" in the sense of
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.

This refers to Isabelle/82add6bf8a42. There are also some administrative
notes of PostgreSQL in Admin/build_log/README.

SQL database access opens many possibilities for the near future. E.g.
PIDE markup that is stored persistently; it would allow to browse formal
sources of Isabelle + AFP in the Prover IDE (or some other client)
without reprocessing.

The implementation in src/Pure/General/sql.scala is relatively
unexciting: it shows that simple things can be done in a simple way,
without too much boilerplate of JDBC. Moreover, I did not pull in any of
the more ambitious Scala/JDBC projects that are emerging elsewhere.


More information about the isabelle-dev mailing list