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

[Makarius]

On 30/03/2019 20:00, Julian Brunner wrote:
> 
> 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.

For now it is sufficient to have some sanity check of the existing
material. I will put it into better shape following the hints below ...

> On Sat, Mar 30, 2019 at 7:49 PM Mathias Fleury
> <mathias.fleury12 at gmail.com> wrote:
>>
>> 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.


	Makarius