[isabelle-dev] NEWS: export_code with formally generated files

[Makarius]

*** HOL ***

* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.

* Command 'export_code': the 'file' argument is now legacy and will be
removed soon: writing to the physical file-system is not well-defined in
a reactive/parallel application like Isabelle. The empty 'file' argument
has been discontinued already: it is superseded by the file-browser in
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.


This refers to Isabelle/6de8b7a5cd44 -- it is the result of a private
discussion with Florian Haftmann yesterday, and the cumulative
discussions about this topic on isabelle-dev in the past few months.

It should now be in principle possible to avoid writing to the
file-system within regular session builds: generated sources may be
turned into executables within Isabelle/ML, and the result exported to
the session database -- all in a formally stateless manner. It some
helpful operations are still missing, we have time before the release to
make it really work well.

Note that the "isabelle build -e" option is a convenient way to make
session exports physically available, but this is not enabled by default
(it is private to an interested user). Consequently, such exports are
not swept under the carpet via .hgignore: if some accidental residues
remain, they should be clearly visible.


Current examples are in AFP/09ea4594dc4e:

  * Diophantine_Eqns_Lin_Hom for Haskell (with GHC)
  * Buchi_Complementation for SML (with MLton)

The latter was actually untested before, and is presently broken:
"unhandled exception: Empty". Either this is natural bit-rot, or I've
got something wrong with the setup in
AFP/thys/Buchi_Complementation/Complementation_Build.thy


Side remark: This is how to figure out AFP metadata formally in
Isabelle/Scala.

  $ isabelle scala
  scala> val afp = AFP.init(Options.init())
  scala> afp.entries_map("Buchi_Complementation").maintainers

Of course it is also possible to inspect the file AFP/metadata/metadata
manually, but the above opens many possibilties for Isabelle/Scala
system programming.


	Makarius