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

[Julian Brunner]

Hello,

At the moment, the executable merely complements a hardcoded automaton
and writes it to a file for testing and benchmarking purposes. It will
not stay like this. Once a parser for the Hanoi Omega Automata format
has been written, this will become a generic command-line
complementation tool. I am not sure what sort of test should be run on
such a tool as part of the regular AFP build.

Julian

On Sat, Mar 30, 2019 at 7:49 PM Mathias Fleury
<mathias.fleury12 at gmail.com> wrote:
>
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev