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

Makarius makarius at sketis.net
Sat Mar 30 23:45:06 CET 2019

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.


More information about the isabelle-dev mailing list