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

[Mathias Fleury]

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


Best,
Mathias