# HG changeset patch
# User haftmann
# Date 1694624935 0
# Node ID b0ddfa5b9ddcbdb1216ec2f120c578abd953cc55
# Parent  d052d61da39827d25ffb11edb7b3741560f0a40e
some hints on managed installations

diff -r d052d61da398 -r b0ddfa5b9ddc src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Wed Sep 13 17:08:54 2023 +0000
+++ b/src/Doc/Codegen/Further.thy	Wed Sep 13 17:08:55 2023 +0000
@@ -4,6 +4,16 @@
 
 section \<open>Further issues \label{sec:further}\<close>
 
+subsection \<open>Runtime environments for \<^text>\<open>Haskell\<close> and \<^text>\<open>OCaml\<close>\<close>
+
+text \<open>
+  The Isabelle System Manual \<^cite>\<open>"isabelle-system"\<close> provides some hints
+  how runtime environments for \<^text>\<open>Haskell\<close> and \<^text>\<open>OCaml\<close> can be
+  set up and maintained conveniently using managed installations within
+  the Isabelle environments.
+\<close>
+
+
 subsection \<open>Incorporating generated code directly into the system runtime -- \<open>code_reflect\<close>\<close>
 
 subsubsection \<open>Static embedding of generated code into the system runtime\<close>
diff -r d052d61da398 -r b0ddfa5b9ddc src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Wed Sep 13 17:08:54 2023 +0000
+++ b/src/Doc/System/Misc.thy	Wed Sep 13 17:08:55 2023 +0000
@@ -466,4 +466,30 @@
   \<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>).
 \<close>
 
+
+section \<open>Managed installations of \<^text>\<open>Haskell\<close> and \<^text>\<open>OCaml\<close>\<close>
+
+text \<open>
+  Code generated in Isabelle \<^cite>\<open>"Haftmann-codegen"\<close> for \<^text>\<open>SML\<close>
+  or \<^text>\<open>Scala\<close> integrates easily using Isabelle/ML or Isabelle/Scala
+  respectively.
+
+  To facilitate integration with further target languages, there are
+  tools to provide managed installations of the required ecosystems:
+
+  \<^item> Tool @{tool_def ghc_setup} provides a basic \<^text>\<open>Haskell\<close> \<^cite>\<open>"Thompson-Haskell"\<close> environment
+    consisting of the Glasgow Haskell Compiler and the Haskell Tool Stack.
+
+  \<^item> Tool @{tool_def ghc_stack} provides an interface to that \<^text>\<open>Haskell\<close>
+    environment; use \<^verbatim>\<open>isabelle ghc_stack --help\<close> for elementary
+    instructions.
+
+  \<^item> Tool @{tool_def ocaml_setup} provides a basic \<^text>\<open>OCaml\<close> \<^cite>\<open>OCaml\<close> environment
+    consisting of the OCaml compiler and the OCaml Package Manager.
+
+  \<^item> Tool @{tool_def ocaml_opam} provides an interface to that \<^text>\<open>OCaml\<close>
+    environment; use \<^verbatim>\<open>isabelle ocaml_opam --help\<close> for elementary
+    instructions.
+\<close>
+
 end