[isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

Hi Makarius,

>   * Are there remaining uses of 'file' with empty name? Is the virtual
> file-system browser sufficiently convenient to inspect results
> interactively?

I checked the file system browser and would be quite content with it; as
a bonus you can then make use of the syntax highlighting of jEdit (OCaml
seems not be built-in, though).

But I want to excite more feedback of users.

>   * How to specify proper (unique) export names: PIDE still lacks a
> check for uniqueness of export names, but overwriting existing exports
> is considered illegal. The 'file' allowed to produce separate names in
> the past, but it has a different meaning now (and is a candidate for
> deletion).

Well, if we re-consider the syntax, we will also find a way for this.

> Maybe 'export_code' should be renovated replaced by reformed commands
> like this:
> 
>   * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
> optional and the default something like "generated" or "code". This
> could be a "thy_decl" command that updates the theory context by
> generated files that are accessible in Isabelle/ML, in addition to the
> export; it would also include a check for duplicate names.
> 
>   * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
> ... checking" is actually a different command. It would be a "diag"
> command as before (this is relevant for parallelism).

Maybe the »checking« should just be a variant of the regular export.

Hence the modification could be quite conservative:

	export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
( file … | ( prefix … ) ( checked ) )

where »file« denotes a relative root in the file system and »checked«
indicated that the generated code will be checked implicitly.

So far my current thoughts.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190114/ee93f126/attachment.sig>