Theory Munta_Certificate_Compile_MLton

section ‹Build and Test Exported Program With MLton›
text_raw ‹\label{build-mlton}›

theory Munta_Certificate_Compile_MLton
  imports Simple_Network_Language_Certificate_Code Munta_Certificate_Testing
begin

text ‹Here is how to compile Munta Certifier with MLton and then run some benchmarks:›

compile_generated_files "code/Certificate.ML" (in Simple_Network_Language_Certificate_Code)
  external_files
    ‹Unsynchronized.sml›
    ‹Writeln.sml›
    ‹Util.sml›
    ‹Muntac.sml›
    ‹Mlton_Main.sml›
    ‹sequential.sml›
    ‹muntac.mlb›
    ‹check_benchmark.sh›
    (in "ML")
  and
    ‹HDDI_02.muntax›
    ‹HDDI_02_broadcast.muntax›
    ‹HDDI_08_broadcast.muntax›
    ‹PM_all_1.muntax›
    ‹PM_all_2.muntax›
    ‹PM_all_3.muntax›
    ‹PM_all_4.muntax›
    ‹PM_all_5.muntax›
    ‹PM_all_6.muntax›
    ‹PM_all_urgent.muntax›
    ‹bridge.muntax›
    ‹csma_05.muntax›
    ‹csma_06.muntax›
    ‹fischer.muntax›
    ‹fischer_05.muntax›
    ‹hddi_08.muntax›
    ‹light_switch.muntax› (in "benchmarks")
  export_files ‹muntac› (exe)
  where ‹fn dir =>
    let
      val exec = Generated_Files.execute dir

      val _ = exec ‹Copy MLunta› ("cp -r '" ^  Path.implode mlunta_dir ^ "' .")
      val _ = exec ‹Compile MLunta› "cd mlunta && mlton=$ISABELLE_MLTON make build_checker && cd .."
      val mlunta_path = "mlunta/build/mluntac-mlton"

      val _ =
        exec ‹Copy Isabelle library files›
          ("cp '" ^ library_path ^ "' library.ML && cp '" ^ basics_path ^ "' basics.ML")

      val _ =
        exec ‹Preparation›
          "mv code/Certificate.ML Certificate.ML"
      val _ =
        exec ‹Replace int type›
          "sed -i -e 's/IntInf/Int/g' Certificate.ML"
      val _ =
        exec ‹set›
          "set -x"
      val _ =
        ― ‹Efficient settings for ARM64 machines›
        exec ‹Compilation›
          (▩‹"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS› ^
            ― ‹these additional settings have been copied from the AFP entry ‹PAC_Checker››
            " -const 'MLton.safe false' -verbose 1 -inline 700 -cc-opt -O3 " ^
            ― ‹this one does not work on ARM64 though›
            ⌦‹"-codegen native " ^›
            ― ‹these used to be the defaults for Munta›
            "-default-type int64 " ^
            "-output muntac " ^
            "-mlb-path-var 'MLUNTA_CERT " ^ mlunta_certificate_path ^ "' " ^
            "muntac.mlb")
      val muntac_path = "./muntac";
      val muntac_path_dc = "./muntac -dc" ― ‹For deadlock checking›

      val _ = writeln "Generating certificates."

      val _ = exec ‹Gen HDDI_02› (mk_cert mlunta_path "HDDI_02")
      val _ = exec ‹Gen HDDI_02_broadcast› (mk_cert mlunta_path "HDDI_02_broadcast")
      val _ = exec ‹Gen HDDI_08_broadcast› (mk_cert mlunta_path "HDDI_08_broadcast")
      val _ = exec ‹Gen hddi_08› (mk_cert mlunta_path "hddi_08")
      val _ = exec ‹Gen PM_all_1› (mk_cert mlunta_path "PM_all_1")
      val _ = exec ‹Gen PM_all_2› (mk_cert mlunta_path "PM_all_2")
      val _ = exec ‹Gen PM_all_3› (mk_cert mlunta_path "PM_all_3")
      val _ = exec ‹Gen PM_all_4› (mk_cert mlunta_path "PM_all_4")
      val _ = exec ‹Gen PM_all_5› (mk_cert mlunta_path "PM_all_5")
      val _ = exec ‹Gen csma_05› (mk_cert mlunta_path "csma_05")
      val _ = exec ‹Gen csma_06› (mk_cert mlunta_path "csma_06")
      val _ = exec ‹Gen fischer_05› (mk_cert mlunta_path "fischer_05")

      val _ = writeln "Finished generating certificates. Now checking.";

      val _ = exec ‹Test HDDI_02› (check_cert muntac_path "HDDI_02")
      val _ = exec ‹Test HDDI_02_broadcast› (check_cert muntac_path "HDDI_02_broadcast")
      val _ = exec ‹Test HDDI_08_broadcast› (check_cert muntac_path "HDDI_08_broadcast")
      val _ = exec ‹Test hddi_08› (check_cert muntac_path "hddi_08")
      val _ = exec ‹Test PM_all_1› (check_cert muntac_path "PM_all_1")
      val _ = exec ‹Test PM_all_2› (check_cert muntac_path "PM_all_2")
      val _ = exec ‹Test PM_all_3› (check_cert muntac_path "PM_all_3")
      val _ = exec ‹Test csma_05› (check_cert muntac_path "csma_05")
      val _ = exec ‹Test csma_06› (check_cert muntac_path "csma_06")
      val _ = exec ‹Test fischer_05› (check_cert muntac_path "fischer_05")
      val _ = exec ‹Test PM_all_4› (check_cert muntac_path "PM_all_4")
      val _ = exec ‹Test PM_all_5› (check_cert muntac_path "PM_all_5")

      val _ = exec ‹Test deadlock HDDI_02› (check_cert muntac_path_dc "HDDI_02")
    in () end›

end