more formal Haskell project setup, with dependencies on packages from "stackage";
--- a/lib/scripts/getsettings Mon Dec 10 22:38:03 2018 +0100
+++ b/lib/scripts/getsettings Mon Dec 10 23:03:20 2018 +0100
@@ -113,6 +113,7 @@
if [ -d "$ISABELLE_STACK_ROOT" -a -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" ]; then
if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS")/$ISABELLE_GHC_VERSION/bin/ghc" ]; then
ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc"
+ ISABELLE_GHC_STACK=true
fi
fi
--- a/src/Pure/Tools/ghc.ML Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Pure/Tools/ghc.ML Mon Dec 10 23:03:20 2018 +0100
@@ -9,6 +9,8 @@
val print_codepoint: UTF8.codepoint -> string
val print_symbol: Symbol.symbol -> string
val print_string: string -> string
+ val project_template: {depends: string list, modules: string list} -> string
+ val new_project: Path.T -> {name: string, depends: string list, modules: string list} -> unit
end;
structure GHC: GHC =
@@ -42,4 +44,47 @@
val print_string = quote o implode o map print_symbol o Symbol.explode;
+
+(* project setup *)
+
+fun project_template {depends, modules} =
+ Input.source_content_string \<open>{-# START_FILE {{name}}.cabal #-}
+name: {{name}}
+version: 0.1.0.0
+homepage: default
+license: BSD3
+author: default
+maintainer: default
+category: default
+build-type: Simple
+cabal-version: >=1.10
+
+executable {{name}}
+ hs-source-dirs: src
+ main-is: Main.hs
+ default-language: Haskell2010
+ build-depends: \<close> ^ commas ("base >= 4.7 && < 5" :: depends) ^
+ Input.source_content_string \<open>
+ other-modules: \<close> ^ commas modules ^
+ Input.source_content_string \<open>
+{-# START_FILE Setup.hs #-}
+import Distribution.Simple
+main = defaultMain
+
+{-# START_FILE src/Main.hs #-}
+module Main where
+
+main :: IO ()
+main = return ()
+\<close>;
+
+fun new_project dir {name, depends, modules} =
+ let
+ val template_path = Path.append dir (Path.basic name |> Path.ext "hsfiles");
+ val _ = File.write template_path (project_template {depends = depends, modules = modules});
+ val {rc, err, ...} =
+ Bash.process ("cd " ^ File.bash_path dir ^
+ "; isabelle ghc_stack new " ^ Bash.string name ^ " --bare " ^ File.bash_path template_path);
+ in if rc = 0 then () else error err end;
+
end;
--- a/src/Tools/Haskell/Haskell.thy Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Mon Dec 10 23:03:20 2018 +0100
@@ -8,7 +8,7 @@
imports Pure
begin
-generate_file "Library.hs" = \<open>
+generate_file "Isabelle/Library.hs" = \<open>
{- Title: Tools/Haskell/Library.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -102,7 +102,7 @@
clean_name = reverse #> dropWhile (== '_') #> reverse
\<close>
-generate_file "Value.hs" = \<open>
+generate_file "Isabelle/Value.hs" = \<open>
{- Title: Haskell/Tools/Value.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -155,7 +155,7 @@
parse_real = Read.readMaybe
\<close>
-generate_file "Buffer.hs" = \<open>
+generate_file "Isabelle/Buffer.hs" = \<open>
{- Title: Tools/Haskell/Buffer.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -181,7 +181,7 @@
content (Buffer xs) = concat (reverse xs)
\<close>
-generate_file "Properties.hs" = \<open>
+generate_file "Isabelle/Properties.hs" = \<open>
{- Title: Tools/Haskell/Properties.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -215,7 +215,7 @@
else props
\<close>
-generate_file "Markup.hs" = \<open>
+generate_file "Isabelle/Markup.hs" = \<open>
{- Title: Haskell/Tools/Markup.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -585,7 +585,7 @@
no_output = ("", "")
\<close>
-generate_file "Completion.hs" = \<open>
+generate_file "Isabelle/Completion.hs" = \<open>
{- Title: Tools/Haskell/Completion.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -646,7 +646,7 @@
markup_report [make limit name_props make_names]
\<close>
-generate_file "File.hs" = \<open>
+generate_file "Isabelle/File.hs" = \<open>
{- Title: Tools/Haskell/File.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -681,7 +681,7 @@
IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
\<close>
-generate_file "XML.hs" = \<open>
+generate_file "Isabelle/XML.hs" = \<open>
{- Title: Tools/Haskell/XML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -760,7 +760,7 @@
show_text = concatMap encode
\<close>
-generate_file "XML/Encode.hs" = \<open>
+generate_file "Isabelle/XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -846,7 +846,7 @@
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
\<close>
-generate_file "XML/Decode.hs" = \<open>
+generate_file "Isabelle/XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -957,7 +957,7 @@
variant _ _ = err_body
\<close>
-generate_file "YXML.hs" = \<open>
+generate_file "Isabelle/YXML.hs" = \<open>
{- Title: Tools/Haskell/YXML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1085,7 +1085,7 @@
_ -> err "multiple results"
\<close>
-generate_file "Pretty.hs" = \<open>
+generate_file "Isabelle/Pretty.hs" = \<open>
{- Title: Tools/Haskell/Pretty.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1239,7 +1239,7 @@
big_list name prts = block (fbreaks (str name : prts))
\<close>
-generate_file "Term.hs" = \<open>
+generate_file "Isabelle/Term.hs" = \<open>
{- Title: Tools/Haskell/Term.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1286,7 +1286,7 @@
deriving Show
\<close>
-generate_file "Term_XML/Encode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1328,7 +1328,7 @@
\case { App a -> Just ([], pair term term a); _ -> Nothing }]
\<close>
-generate_file "Term_XML/Decode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
--- a/src/Tools/Haskell/Test.thy Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/Haskell/Test.thy Mon Dec 10 23:03:20 2018 +0100
@@ -8,15 +8,18 @@
begin
ML \<open>
- Isabelle_System.with_tmp_dir "ghc" (fn dir =>
+ Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
let
- val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> dir;
+ val src_dir = Path.append tmp_dir (Path.explode "src");
+ val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
+
+ val modules = files
+ |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
+ val _ = GHC.new_project tmp_dir {name = "isabelle", depends = [], modules = modules};
+
val (out, rc) =
Isabelle_System.bash_output
- (cat_lines
- ["set -e",
- "cd " ^ File.bash_path dir,
- "\"$ISABELLE_GHC\" " ^ File.bash_paths files]);
+ (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
in if rc = 0 then writeln out else error out end)
\<close>
--- a/src/Tools/ROOT Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/ROOT Mon Dec 10 23:03:20 2018 +0100
@@ -12,5 +12,5 @@
session Haskell in Haskell = Pure +
theories
Haskell
- theories [condition = ISABELLE_GHC]
+ theories [condition = ISABELLE_GHC_STACK]
Test