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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
