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

Mathias Fleury mathias.fleury12 at gmail.com
Sat Mar 30 19:49:30 CET 2019

Hi all,

I had a look at that:

> 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

The programs expects as first argument a path where the complemented automaton can be written (i.e., ./Completion /tmp/automaton). The path is extracted with hd and if you don't pass an argument, then an error is raised because the list of arguments is empty.

Now I am not certain if the correct fix is to:
  - add an argument in the Isabelle theory
  - remove the part writing the file in Completion.sml,
  - change Completion.sml to either print the automaton to stdout if there is no argument, or to print it to a file if there is an argument


More information about the isabelle-dev mailing list