The Isabelle Server: responsive control of prover sessions

Recent Isabelle repository versions (e.g. 83902fff6243 as approximation of Isabelle2018) support client-server connections for Isabelle prover sessions, with a
simple line-based protocol for synchronous commands. Asynchronous tasks work by explicit indication of forked vs. finished (or failed) background processes, potentially with intermediate notifications. Protocol messages use JSON syntax by default, but YXML is also possible (e.g. for native PIDE messages that might be supported in the future).

Further details are explained in chapter 4 of the system manual, e.g. see the Documentation panel in Isabelle/jEdit of a recent release snapshot. Here is a minimal example extracted from the manual:

isabelle server &
isabelle client
session_start {"session": "HOL"}
use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}
session_stop {"session_id": ...}
shutdown

The first two commands are for the Unix terminal, the rest for the Isabelle client-server loop. Each line needs to be applied carefully, when the previous command has finished, and use_theories needs to fit on a single line.

Under program control, explicit messages for forked and finished tasks (with unique id) may be used to enforce execution in the proper order.

Update 12-Jul-2018: Link to forthcoming Isabelle2018.

Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?

Die Internationale Kelleruni Herrenbach veranstaltet im April eine öffentliche Vorlesung über Bitcoin und Blockchain.

Thema:
Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?
Referenten:
Dr. Makarius Wenzel
Autor Christoph Ulrich Mayer
Zeit:
Freitag, 13. April 2018 um 19:30
Ort:
Lebensraum Schwabencenter (“Wohnzimmer”)

Das “Wohnzimmer” im Schwabencenter ist ein umgenutztes Ladenlokal innerhalb des regulären Einkaufszentrums. Nach der Vorlesung gibt es noch etwas zu Essen.

Peter Biet von der Kelleruni schreibt hierzu:

Ich selber bin auf diese Vorlesung sehr gespannt, denn ich lese davon ständig in der Zeitung. Ich höre von vielen gerade jungen Menschen, die relativ große Summen in Bitcoins investieren und damit dann auch tatsächlich “richtig Kohle” machen. Ich höre von der Möglichkeit, Geldflüsse unabhängig von Banken zu inszenieren, aber auch von Schwarzgeldern, die da gewaschen werden. Ich höre außerdem von den riesigen Rechnerleistungen, die benötigt werden, um Bitcoins zu schürfen. Und vor allem weiß ich Eines: Ich verstehe das Ganze überhaupt nicht. Finde, obwohl ich versucht habe, mich zu informieren einfach keinen Zugang zu der Sache.
Vielleicht geht es manchen von euch ja genau so. Jedenfalls bin ich des Öfteren gebeten worden, dass wir uns mal dieses so aktuellen Themas annehmen sollten. Und so freue ich mich sehr und bin gewiss, dass Makarius und Christoph da etwas Licht in mein/unser Wissensdunkel bringen werden.

Hier das Material von Makarius.