[isabelle-dev] NEWS: export_code with formally generated files
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).
$ 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
More information about the isabelle-dev