Theory Complementation_Build

section ‹Build and test exported program with MLton›

theory Complementation_Build
imports Complementation_Final
begin

external_file ‹code/Autool.mlb›
external_file ‹code/Prelude.sml›
external_file ‹code/Autool.sml›

compile_generated_files ✐‹contributor Makarius›
  ‹code/Complementation.ML› (in Complementation_Final)
  external_files
    ‹code/Autool.mlb›
    ‹code/Prelude.sml›
    ‹code/Autool.sml›
  export_files ‹code/Complementation.sml› and ‹code/Autool› (exe)
  where ‹fn dir =>
    let
      val exec = Generated_Files.execute (dir + Path.basic "code");
      val _ = exec ‹Prepare› "mv Complementation.ML Complementation.sml";
      val _ = exec ‹Compilation› (▩‹"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS › ^
            " -profile time -default-type intinf Autool.mlb");
      val _ = exec ‹Test› "./Autool help";
    in () end›

end