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

[Makarius]

On 14/01/2019 20:20, Florian Haftmann wrote:
> 
>>   * 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.

Here is some feedback from myself as a user: the new stateless model to
generate files works well, in particular the file-browser of
Isabelle/jEdit helps.

There was only a technical problem it that should no longer occur in
practice, see

changeset:   69696:9fd395ff57bc
user:        wenzelm
date:        Sun Jan 20 21:26:15 2019 +0100
files:       Admin/components/components.sha1 Admin/components/main
src/Tools/jEdit/patches/vfs_manager
description:
avoid crash of jEdit.closeBuffer() via
TaskManager.instance.waitForIoTasks() due to race condition of save()
vs. automatic load() of already open buffer, e.g. relevant for save-as
on "isabelle-export:" artifacts;


In the mainstream this would probably be called a "fix", but the
conceptual problem behind it is still there: there are concurrent tasks
that are just concatenated in sequence, without taking the nesting of
the program structure into account. Proper futures are required instead
of slightly odd wait operations.


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

I have looked around at typical uses of 'export_code' in AFP. Most of
the time it is just informative: writing a file and looking at it in the
editor (or via the command-line!?), or doing that on the output channel.
The isabelle-export: file-system covers that already, i.e. we should be
able to eliminate almost all generated files from the AFP repository.

So "export_code .. file" should just disappear -- it is semantically
illtyped in PIDE: editing the "file" argument will leave a trace of
machine oil spilled to the physical file-system.


We do need an explicit prefix and an internal check for duplicates, e.g.
as in the command 'generated_file'.

That should be really just a prefix for the exported artifact, not the
name itself: each language processor should be smart enough to derive
file or directory names from it as required.  Thus the prefix locally
belongs in front of the arguments.

Here is an example from AFP/160ac13cdc05
SATSolverVerification/SatSolverCode.thy:

  export_code solve
    in OCaml file "code/solve.ML"
    in SML file "code/solve.ocaml
    in Haskell file "code/"

It could be turned into something like this:

  export_code "code/" = solve in OCaml SML Haskell

Some details about the automatic name derivation scheme still need to be
sorted out -- or 'file' remains as an option to specify the suffix for
effective name (without writing anything to the file-system).


	Makarius