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

[Makarius]

On 30/03/2019 00:22, Makarius wrote:
> 
> Current examples are in AFP/09ea4594dc4e:
> 
>   * Diophantine_Eqns_Lin_Hom for Haskell (with GHC)

Thanks to the truly portable Haskell Stack, this works even on Windows
(Isabelle/c17c654f6bb6 + AFP/a8142ac5e4b6).

For example:

  $ isabelle build -e -d '$AFP' Diophantine_Eqns_Lin_Hom

  $ thys/Diophantine_Eqns_Lin_Hom/generated/hlde.exe "([3, 5, 1], [2, 7])"


The setup in ML merely needs to be careful about Path.exe to produce the
(optional) .exe file extension.


>  * Buchi_Complementation for SML (with MLton)

We don't have MLton on Cygwin/Windows, so there is nothing to test at
the moment.


	Makarius