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

[Makarius]

On 05/02/2019 13:18, Salomon Sickert wrote:
> 
>> It should be easy to make this part of the formal session, with some
>> options [condition = ISABELLE_MLTON].
>>
>> The 'export_code' command will have to emit generated files
>> (Generated_Files.add_files) to make the assembly work in Isabelle/ML.
>>
> 
> That is a great development. 
> 
> Could someone point me to an example on how to do compilation with either mlton or polyml within a formal session?

See now AFP/09ea4594dc4e:

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

Apart from spurious Makefiles lying around (usually with the status of
untested private experiments from some years ago), there are many more
adhoc shell scripts of a similar kind in AFP. It will take some time to
sort it all out, but for the Isabelle2019 release the main goal is to
polish the programming interfaces to make it all work smoothly -- such
that there are no remaining reasons to write physical files into the
session source space.


	Makarius