Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] generating isabelle theory files from ML modules?

Email Gateway (Aug 18 2022 at 10:13):

From: Tuvshintur Tserendorj <uesn@cs.tu-berlin.de>
hi,

Does someone know there exists anytool for generating isabelle theory
files from ML modules (functions)?

Is such a tool needed?

cheers,
Tuvshintur

Email Gateway (Aug 18 2022 at 10:14):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,

For "normal" use of Isabelle there is no need deal with ML --
development is done in Isar .thy files.

If you have a particular application involving ML programming, you may
embed ML code into your .thy files using

ML {*
val bla = ...;
fun foo x = ...;
...
*}

sections.

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

Email Gateway (Aug 18 2022 at 10:14):

From: David Aspinall <David.Aspinall@ed.ac.uk>
If you mean are there ML functions which help generate theory file text,
e.g. by building a parse tree and then printing it, then I believe the
answer is "no, not at the moment" but yes, such a tool is needed if you
want to manipulate proof scripts programmatically. I have wanted to do
this for Proof General for a long time, but it seems difficult to
achieve with Isar's extensible language and parsing combinators.

- David.

Tuvshintur Tserendorj wrote:

Last updated: May 03 2024 at 04:19 UTC