# HG changeset patch # User wenzelm # Date 1675599239 -3600 # Node ID c42bf52381f1358a463c8d368dc0d0f634ac4b4a # Parent f6ba88f2313576f7e170c6933d6f621806bc7b71 proper compiler root for arm64; diff -r f6ba88f23135 -r c42bf52381f1 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 """)