Re: [isabelle] Isabelle2021-1-RC2: Invoking smt-method in theory loaded via Isabelle/Scala



We have another application for grading Isabelle theories on do.proof.in.tum.de: https://github.com/maxhaslbeck/proving-contest-backends/blob/master/Isabelle/grader.py

Simon

Am Di., 9. Nov. 2021 um 16:36 Uhr schrieb Makarius <makarius at sketis.net>:
On 09/11/2021 14:36, Dominique Unruh wrote:
>
> scala-isabelle actually makes things easier because it encapsulates the
> undocumented (or documented-by-source-code) aspects of the invocation of
> Isabelle into a documented API (that also changes less).

The Isabelle/PIDE server does have a lot of explicit documentation: chapter 4
of the "system" manual. In retrospect, I am unsure if it ever got used in
applications so far.

There is a report by  Boris Shminke on using it from Python:
https://link.springer.com/chapter/10.1007%2F978-3-030-81097-9_20 --- but it
remains unclear if and how it works in applications.


        Makarius



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.