[isabelle-dev] NEWS: generated code as proper theory export
makarius at sketis.net
Sat Feb 2 15:28:26 CET 2019
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
> 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
> 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
More information about the isabelle-dev