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;
wenzelm@69241
     1
(*  Title:      Tools/Haskell/Test.thy
wenzelm@69225
     2
    Author:     Makarius
wenzelm@69225
     3
*)
wenzelm@69225
     4
wenzelm@69241
     5
section \<open>Test build of Isabelle/Haskell modules\<close>
wenzelm@69225
     6
wenzelm@69241
     7
theory Test imports Haskell
wenzelm@69225
     8
begin
wenzelm@69225
     9
wenzelm@69239
    10
ML \<open>
wenzelm@69444
    11
  Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
wenzelm@69225
    12
    let
wenzelm@69444
    13
      val src_dir = Path.append tmp_dir (Path.explode "src");
wenzelm@69444
    14
      val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
wenzelm@69444
    15
wenzelm@69444
    16
      val modules = files
wenzelm@69662
    17
        |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
wenzelm@69446
    18
      val _ =
wenzelm@69446
    19
        GHC.new_project tmp_dir
wenzelm@69453
    20
          {name = "isabelle",
wenzelm@69473
    21
           depends =
wenzelm@69473
    22
            ["bytestring", "containers", "network", "split", "threads", "utf8-string", "uuid"],
wenzelm@69453
    23
           modules = modules};
wenzelm@69444
    24
wenzelm@69225
    25
      val (out, rc) =
wenzelm@69225
    26
        Isabelle_System.bash_output
wenzelm@69444
    27
          (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
wenzelm@69239
    28
    in if rc = 0 then writeln out else error out end)
wenzelm@69225
    29
\<close>
wenzelm@69225
    30
wenzelm@69225
    31
end