proper compiler root for arm64;
authorwenzelm
Sun, 05 Feb 2023 13:13:59 +0100
changeset 77191 c42bf52381f1
parent 77190 f6ba88f23135
child 77192 198697983eec
proper compiler root for arm64;
src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Feb 04 23:08:36 2023 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sun Feb 05 13:13:59 2023 +0100
@@ -160,15 +160,15 @@
   val default_sha1_url = "https://isabelle.sketis.net/repos/sha1/archive"
   val default_sha1_version = "e0239faa6f42"
 
-  private def init_sources(src_dir: Path): Unit = {
-    val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML")))
+  private def init_src_root(src_dir: Path, input: String, output: String): Unit = {
+    val lines = split_lines(File.read(src_dir + Path.explode(input)))
     val ml_files =
       for {
         line <- lines
         rest <- Library.try_unprefix("use", line)
       } yield "ML_file" + rest
 
-    File.write(src_dir + Path.explode("ROOT.ML"),
+    File.write(src_dir + Path.explode(output),
 """(* Poly/ML Compiler root file.
 
 When this file is open in the Prover IDE, the ML files of the Poly/ML
@@ -215,7 +215,8 @@
           download
         }
 
-      init_sources(component_dir.src)
+      init_src_root(component_dir.src, "RootArm64.ML", "ROOT0.ML")
+      init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
 
       for (arch_64 <- List(false, true)) {
         progress.echo("Building " + polyml_platform(arch_64))
@@ -261,7 +262,14 @@
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_SOURCES="$POLYML_HOME/src"
 
-ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"
+case "$ML_PLATFORM" in
+  *arm64*)
+    ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT0.ML"
+    ;;
+  *)
+    ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"
+    ;;
+esac
 """)