src/Tools/Haskell/Test.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69662 fd86ed39aea4
child 70047 96fe857a7a6f
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/Haskell/Test.thy
     2     Author:     Makarius
     3 *)
     4 
     5 section \<open>Test build of Isabelle/Haskell modules\<close>
     6 
     7 theory Test imports Haskell
     8 begin
     9 
    10 ML \<open>
    11   Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
    12     let
    13       val src_dir = Path.append tmp_dir (Path.explode "src");
    14       val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
    15 
    16       val modules = files
    17         |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
    18       val _ =
    19         GHC.new_project tmp_dir
    20           {name = "isabelle",
    21            depends =
    22             ["bytestring", "containers", "network", "split", "threads", "utf8-string", "uuid"],
    23            modules = modules};
    24 
    25       val (out, rc) =
    26         Isabelle_System.bash_output
    27           (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
    28     in if rc = 0 then writeln out else error out end)
    29 \<close>
    30 
    31 end