[isabelle-dev] isabelle build and code generation
makarius at sketis.net
Wed Aug 8 21:49:25 CEST 2012
On Wed, 8 Aug 2012, Florian Haftmann wrote:
> I wonder whether there is a possibility to generalize the session
> concept to other generates beyond tex as well, in particular generated
> code, e.g.
> session Foo = HOL +
> Bar [export_code = blubb in SML]
Notationally, the options go before the theories:
theories [export_code = "blubb in SML"]
They are also restricted to plain strings, with extra interpretation (and
type checking) for strings that look like bools, ints, reals.
Apart from that, options can be anything. Components can also declare new
options in etc/options, but have to coexist with a global name space
without any qualification.
These restrictions are there to make it possible to move options between
many systems, such as rather dumb editor front-ends that don't have
Isabelle name spaces nor a formal context nor attribute argument syntax.
> This would subsume the rather arcane »isabelle codegen«, and give the
> existing export_code a similar status like display_draft or thy_deps
> (and to all of them, hopefully, a more reasonable interaction paradigm
> than the current side effects on reparsing in jEdit).
I am aware of these open questions, but don't have good answers yet.
Somehow such tools need to become "stateless" or "value-oriented". This
works for plain writeln already, it can be also made to work with
display_draft or thy_deps.
For code generation one probably needs a bit more sophistication to have
some kind of "value-oriented" file-system content being exported, that
some add-on tools can then tap into.
I wonder how Eclipse does such things.
More information about the isabelle-dev