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

[Makarius]

On 02/02/2019 14:13, Florian Haftmann wrote:

> * The module naming schema gets more sophisticated: default, name or
> prefix.  The key point is that this naming schema is again
> target-language specific.

Just abstractly, a reform should strive for unification and
simplification whenever possible.

The different languages have slightly different side-conditions, but
maybe they can still be unified: e.g. the main NAME could become
NAME.EXT or NAME/ depending on the situation.

One could also use the const names to produce a default, e.g. according
to the traditional scheme to concatenate const base names with "_" as
separator.


> This should cover all application cases.

When export_code emits Generated_Files.add_files, there is always a
possibility to do special-purpose Isabelle/ML programming with
Generated_Files.get_files. No need to have all odd cases in one Isar
command.


> At the moment I am still in favour of a diagnostic command to emit sth
> ad-hoc into the file system -- but this could be something separate from
> export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination.

For diagnostics I have used the "isabelle-export:" VFS in Isabelle/jEdit
so far: if a physical file is required, it can be written from the
editor (which actually cased the crash before Isabelle/9fd395ff57bc).

Minor disadvantage: writing directory content is inconvenient. In that
case there is also Generated_Files.write_files.


Some months ago I've seen odd crashes with files written to
$ISABELLE_TMP_PREFIX/ in Isabelle/ML and read in Isabelle/Scala.
Moreover I've seen crashes of the Headless PIDE session of export_code
with $ISABELLE_TMP_PREFIX in particular.

There might be something wrong in my areas of responsibility, or
something inherently fragile in concurrent access to a Unix file-system.

These incidents motivated to revive the pending thread to eliminate
physical files from export_code in the first place. Mathematical files
in the theory context are more reliably than physical ones on a magnetic
drum.


	Makarius