tuned -- prefer Isar command 'compile_generated_files';
authorwenzelm
Tue Apr 09 10:51:35 2019 +0200 (5 months ago)
changeset 700824f936de6d9b8
parent 70081 093ab1a99eb6
child 70083 96776eb41854
tuned -- prefer Isar command 'compile_generated_files';
NEWS
src/Tools/Haskell/Test.thy
     1.1 --- a/NEWS	Tue Apr 09 10:28:17 2019 +0200
     1.2 +++ b/NEWS	Tue Apr 09 10:51:35 2019 +0200
     1.3 @@ -265,9 +265,8 @@
     1.4      eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
     1.5    \<close>
     1.6  
     1.7 -The ML function Generate_File.generate writes all generated files from a
     1.8 -given theory to the file-system, e.g. a temporary directory where some
     1.9 -external compiler is applied.
    1.10 +See also commands 'export_generated_files' and 'compile_generated_files'
    1.11 +to use the results.
    1.12  
    1.13  * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
    1.14  option ML_environment to select a named environment, such as "Isabelle"
     2.1 --- a/src/Tools/Haskell/Test.thy	Tue Apr 09 10:28:17 2019 +0200
     2.2 +++ b/src/Tools/Haskell/Test.thy	Tue Apr 09 10:51:35 2019 +0200
     2.3 @@ -4,29 +4,24 @@
     2.4  
     2.5  section \<open>Test build of Isabelle/Haskell modules\<close>
     2.6  
     2.7 -theory Test imports Haskell
     2.8 +theory Test
     2.9 +  imports Haskell
    2.10  begin
    2.11  
    2.12 -ML \<open>
    2.13 -  Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
    2.14 +compile_generated_files _ (in Haskell)
    2.15 +  where \<open>fn dir =>
    2.16      let
    2.17 -      val src_dir = Path.append tmp_dir (Path.explode "src");
    2.18 -      val files = Generated_Files.get_files \<^theory>\<open>Haskell\<close>;
    2.19 -      val _ = List.app (Generated_Files.write_file src_dir) files;
    2.20 -
    2.21 -      val modules = files
    2.22 +      val modules =
    2.23 +        Generated_Files.get_files \<^theory>\<open>Haskell\<close>
    2.24          |> map (#path #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
    2.25        val _ =
    2.26 -        GHC.new_project tmp_dir
    2.27 +        GHC.new_project dir
    2.28            {name = "isabelle",
    2.29             depends =
    2.30              ["bytestring", "containers", "network", "split", "threads", "utf8-string", "uuid"],
    2.31             modules = modules};
    2.32 -
    2.33 -      val (out, rc) =
    2.34 -        Isabelle_System.bash_output
    2.35 -          (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
    2.36 -    in if rc = 0 then writeln out else error out end)
    2.37 -\<close>
    2.38 +    in
    2.39 +      writeln (Generated_Files.execute dir \<open>Build\<close> "mv Isabelle src && isabelle ghc_stack build")
    2.40 +    end\<close>
    2.41  
    2.42  end