[isabelle-dev] isabelle build and code generation

[Makarius]

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 +
>  theories
>    …
>  theories
>    Bar [export_code = blubb in SML]
>  …

Notationally, the options go before the theories:

   theories [export_code = "blubb in SML"]
      Bar Baz

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.


 	Makarius