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

[Makarius]

On 11/01/2019 11:51, Makarius wrote:
> On 10/01/2019 16:38, Makarius wrote:
>> On 10/01/2019 16:28, Florian Haftmann wrote:
>>> Code generation: command 'export_code' without file keyword exports
>>> code as regular theory export, which can be materialized using tool
>>> 'isabelle export'; to get generated code dumped into output, use
>>> 'file ""'.  Minor INCOMPATIBILITY.
>>>
>>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
>>> generated code in AFP-entries.
>>
>> Great, I will try this out soon.
> 
> I have started looking and thinking about it again.

I have reworked this a bit in Isabelle/e61b0b819d28: Isabelle/jEdit is
able to browse theory exports via the virtual file-system
"isabelle-export:" and the 'export_code' command emits some information
message about it.

There are still a few open questions:

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

  * 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).


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).


	Makarius