# HG changeset patch
# User Lukas Stevens <mail@lukas-stevens.de>
# Date 1738339312 -3600
# Node ID 2ca4fa5d1268f28728fbcd5f78e5fc74fdedf141
# Parent  9c33627cea18a98ee0a576f3d4ec368e30510457# Parent  a63f75499938ad44360638dd0658347201d042a1
merged

diff -r 9c33627cea18 -r 2ca4fa5d1268 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Jan 31 17:01:27 2025 +0100
+++ b/Admin/components/components.sha1	Fri Jan 31 17:01:52 2025 +0100
@@ -254,6 +254,7 @@
 5117b7d0283adf31cf2bde17a9912eb775a0822f jedit-20241101.tar.gz
 a8b11ddf7f6838ea53868e46cb4555b7fa60e776 jedit-20241115.tar.gz
 6a5d78867dc6f692f8f3ab758e3ac1b86fabd3bf jedit-20250129.tar.gz
+011d322d4ae1f8c57112bd695f5e812e48e1d953 jedit-20250130.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r 9c33627cea18 -r 2ca4fa5d1268 Admin/components/main
--- a/Admin/components/main	Fri Jan 31 17:01:27 2025 +0100
+++ b/Admin/components/main	Fri Jan 31 17:01:52 2025 +0100
@@ -3,7 +3,7 @@
 bash_process-20240326
 bib2xhtml-20190409
 csdp-6.1.1
-cvc4-1.8
+cvc5-1.2.0-1
 e-3.1-1
 elm-0.19.1
 easychair-3.5
@@ -15,7 +15,7 @@
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250129
+jedit-20250130
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
diff -r 9c33627cea18 -r 2ca4fa5d1268 NEWS
--- a/NEWS	Fri Jan 31 17:01:27 2025 +0100
+++ b/NEWS	Fri Jan 31 17:01:52 2025 +0100
@@ -245,6 +245,7 @@
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
+      . cvc5 1.2.0 -- with support for arm64-linux
   - Added instantiations of facts using the "of" attribute
     (e.g. "assms(1)[of x]"), which can be activated using the
     Sledgehammer option "instantiate" (default: smart, i.e. only if
@@ -262,8 +263,6 @@
 * Code generator: command 'code_reserved' now uses parentheses for
 target languages, similar to 'code_printing'.
 
-* Theory HOL.List: overloaded power operator (^^) on type list.
-
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Nunchaku.thy
--- a/src/HOL/Nunchaku.thy	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Nunchaku.thy	Fri Jan 31 17:01:52 2025 +0100
@@ -11,7 +11,7 @@
 
 The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
 the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4, Kodkodi, and SMBC are necessary to use these backend solvers.
+for cvc5, Kodkodi, and SMBC are necessary to use these backend solvers.
 *)
 
 theory Nunchaku
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -239,7 +239,7 @@
     (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN))
   ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc5" (smt_solver_tac "cvc5" lthy i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -43,7 +43,7 @@
 
   val agsyholN : string
   val alt_ergoN : string
-  val cvc4N : string
+  val cvc5N : string
   val eN : string
   val iproverN : string
   val leo2N : string
@@ -111,7 +111,7 @@
 
 val agsyholN = "agsyhol"
 val alt_ergoN = "alt_ergo"
-val cvc4N = "cvc4"
+val cvc5N = "cvc5"
 val eN = "e"
 val iproverN = "iprover"
 val leo2N = "leo2"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -30,7 +30,7 @@
    ("max_genuine", "1"),
    ("max_potential", "1"),
    ("overlord", "false"),
-   ("solvers", "cvc4 kodkod paradox smbc"),
+   ("solvers", "cvc5 kodkod paradox smbc"),
    ("specialize", "true"),
    ("spy", "false"),
    ("timeout", "30"),
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -86,7 +86,7 @@
     else
       let
         val bash_cmd =
-          "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
+          "PATH=\"$CVC5_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
           nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
           (if specialize then "" else "--no-specialize ") ^
           "--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -388,10 +388,10 @@
 
 val default_slice_schedule =
   (* FUDGE (loosely inspired by Seventeen evaluation) *)
-  [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN,
-   cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN,
+  [cvc5N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc5N, zipperpositionN,
+   cvc5N, eN, zipperpositionN, vampireN, cvc5N, cvc5N, vampireN, cvc5N, iproverN, zipperpositionN,
    spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN,
-   iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N,
+   iproverN, spassN, zipperpositionN, vampireN, cvc5N, zipperpositionN, z3N, z3N, cvc5N,
    zipperpositionN]
 
 fun schedule_of_provers provers num_slices =
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jan 31 17:01:52 2025 +0100
@@ -315,7 +315,7 @@
 val leo3_config : atp_config =
   {exec = (["LEO3_HOME"], ["leo3"]),
    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem =>
-     [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
+     [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC5_SOLVER\" --atp e=\"$E_HOME\"/eprover \
       \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
       (if full_proofs then "--nleq --naeq " else "")],
    proof_delims = tstp_proof_delims,
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/HOL/Tools/etc/options	Fri Jan 31 17:01:52 2025 +0100
@@ -26,7 +26,7 @@
 
 section "Miscellaneous Tools"
 
-public option sledgehammer_provers : string = "cvc4 verit z3 e spass vampire zipperposition"
+public option sledgehammer_provers : string = "cvc5 verit z3 e spass vampire zipperposition"
   -- "provers for Sledgehammer (separated by blanks)"
 
 public option sledgehammer_timeout : int = 30
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Fri Jan 31 17:01:52 2025 +0100
@@ -420,7 +420,10 @@
   def build_release_archive(
     context: Release_Context,
     version: String,
-    parallel_jobs: Int = 1
+    parallel_jobs: Int = 1,
+    build_library: Boolean = false,
+    include_library: Boolean = false,
+    include_find_facts: Boolean = false
   ): Unit = {
     val progress = context.progress
 
@@ -457,10 +460,13 @@
       record_bundled_components(context.isabelle_dir)
 
 
-      /* build tools and documentation */
+      /* build documentation and internal HTML library */
 
       val other_isabelle = context.other_isabelle(context.dist_dir)
 
+      def other_isabelle_purge(name: String): Unit =
+        Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.basic(name))
+
       other_isabelle.init(echo = true)
 
       try {
@@ -471,11 +477,47 @@
 
       make_news(other_isabelle)
 
-      for (name <- List("Admin", "browser_info", "heaps")) {
-        Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
+      other_isabelle_purge("browser_info")
+
+      if (build_library || include_library || include_find_facts) {
+        require(Platform.is_unix, "Linux or macOS platform required")
+
+        val opt_dirs = "-d '~~/src/Benchmarks' "
+        other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
+          " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
+          " -o system_heaps -a " + opt_dirs, echo = true).check
+
+        if (include_find_facts) {
+          val database_name = "isabelle"
+          val database_dir =
+            other_isabelle.expand_path(
+              Path.explode("$FIND_FACTS_HOME_USER/solr") + Path.basic(database_name))
+          val database_target_dir =
+            other_isabelle.expand_path(
+              Path.explode("$FIND_FACTS_HOME/lib/find_facts-" + database_name))
+
+          val sessions =
+            other_isabelle.bash("bin/isabelle sessions -a " + opt_dirs).check.out_lines
+          other_isabelle.bash(
+            "bin/isabelle find_facts_index -o find_facts_database_name=" +
+              Bash.string(database_name) + " -n " + opt_dirs +
+              Bash.strings(sessions), echo = true).check
+          Isabelle_System.make_directory(database_target_dir)
+          Isabelle_System.copy_dir(database_dir, database_target_dir, direct = true)
+
+          Isabelle_System.rm_tree(database_dir)
+          database_dir.dir.file.delete  // "$FIND_FACTS_HOME_USER/solr"
+          database_dir.dir.dir.file.delete  // "$FIND_FACTS_HOME_USER"
+        }
+
+        if (!include_library) other_isabelle_purge("browser_info")
       }
 
+      other_isabelle_purge("Admin")
+      other_isabelle_purge("heaps")
+
       other_isabelle.cleanup()
+      other_isabelle.isabelle_home_user.file.delete
 
 
       progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
@@ -485,6 +527,12 @@
         """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
       execute_tar(context.dist_dir, "-czf " +
         File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
+
+      if (build_library) {
+        progress.echo_warning("Creating library archive " + context.isabelle_library_archive + " ...")
+        execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+          " " + Bash.string(context.dist_name + "/browser_info"))
+      }
     }
   }
 
@@ -498,7 +546,6 @@
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_sessions: List[String] = Nil,
-    build_library: Boolean = false,
     parallel_jobs: Int = 1
   ): Unit = {
     val progress = context.progress
@@ -828,37 +875,6 @@
         Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
       }
     }
-
-
-    /* HTML library */
-
-    if (build_library) {
-      if (context.isabelle_library_archive.is_file) {
-        progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
-      }
-      else {
-        require(Platform.is_unix, "Linux or macOS platform required")
-        Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
-          val bundle = context.dist_name + "_" + Platform.family + ".tar.gz"
-          val bundle_path = context.dist_dir + Path.basic(bundle)
-          execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle_path))
-
-          val other_isabelle = context.other_isabelle(tmp_dir)
-
-          Isabelle_System.make_directory(other_isabelle.etc)
-          File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
-
-          other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
-            " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
-            " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
-          other_isabelle.isabelle_home_user.file.delete
-
-          execute(tmp_dir, "chmod -R a+r,g=o " + Bash.string(context.dist_name))
-          execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
-            " " + Bash.string(context.dist_name + "/browser_info"))
-        }
-      }
-    }
   }
 
 
@@ -869,6 +885,8 @@
     Command_Line.tool {
       var afp_rev = ""
       var target_dir = Path.current
+      var include_find_facts = false
+      var include_library = false
       var release_name = ""
       var source_archive = ""
       var website: Option[Path] = None
@@ -886,13 +904,15 @@
   Options are:
     -A REV       corresponding AFP changeset id
     -D DIR       target directory (default ".")
+    -F           include library: Find_Facts data
+    -L           include library: HTML presentation
     -R RELEASE   explicit release name
     -S ARCHIVE   use existing source archive (file or URL)
     -W WEBSITE   produce minimal website in given directory
     -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
     -j INT       maximum number of parallel jobs (default 1)
-    -l           build library
+    -l           build library archive
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + quote(default_platform_families.mkString(",")) + """)
     -r REV       Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
@@ -901,6 +921,8 @@
 """,
         "A:" -> (arg => afp_rev = arg),
         "D:" -> (arg => target_dir = Path.explode(arg)),
+        "F" -> (_ => include_find_facts = true),
+        "L" -> (_ => include_library = true),
         "R:" -> (arg => release_name = arg),
         "S:" -> (arg => source_archive = arg),
         "W:" -> (arg => website = Some(Path.explode(arg))),
@@ -931,7 +953,9 @@
         if (source_archive.isEmpty) {
           val context = make_context(release_name)
           val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
-          build_release_archive(context, version, parallel_jobs = parallel_jobs)
+          build_release_archive(context, version, parallel_jobs = parallel_jobs,
+            build_library = build_library, include_library = include_library,
+            include_find_facts = include_find_facts)
           context
         }
         else {
@@ -945,7 +969,7 @@
 
       build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
         more_components = more_components, build_sessions = build_sessions,
-        build_library = build_library, parallel_jobs = parallel_jobs, website = website)
+        parallel_jobs = parallel_jobs, website = website)
     }
   }
 }
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala	Fri Jan 31 17:01:52 2025 +0100
@@ -197,6 +197,8 @@
       Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
     }
 
+    (jars_dir + Path.basic("MacOS.jar")).file.delete
+
     for { (name, vers) <- download_plugins } {
       Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
         val url =
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/Build/browser_info.scala	Fri Jan 31 17:01:52 2025 +0100
@@ -51,8 +51,8 @@
       }
     }
 
-    def init_directory(dir: Path): Path = {
-      check_directory(dir)
+    def init_directory(dir: Path, permissive: Boolean = false): Path = {
+      if (!permissive) check_directory(dir)
       Isabelle_System.make_directory(dir + PATH)
       dir
     }
@@ -285,7 +285,7 @@
     /* maintain presentation structure */
 
     def update_chapter(session_name: String, session_description: String): Unit = synchronized {
-      val dir = Meta_Info.init_directory(chapter_dir(session_name))
+      val dir = Meta_Info.init_directory(chapter_dir(session_name), permissive = true)
       Meta_Info.change(dir, Meta_Info.INDEX) { text =>
         val index0 = Meta_Info.Index.parse(text, "chapter")
         val item = Meta_Info.Item(session_name, description = session_description)
@@ -312,7 +312,7 @@
     }
 
     def update_root(): Unit = synchronized {
-      Meta_Info.init_directory(root_dir)
+      Meta_Info.init_directory(root_dir, permissive = true)
       HTML.init_fonts(root_dir)
       Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
         root_dir + Path.explode("isabelle.gif"))
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Pure/System/other_isabelle.scala	Fri Jan 31 17:01:52 2025 +0100
@@ -187,6 +187,7 @@
 
   def cleanup(): Unit = {
     clean_settings()
+    ssh.delete(expand_path(Host.private_data.database))
     ssh.delete(etc, isabelle_home_user)
   }
 }
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/Tools/find_facts_index
--- a/src/Tools/Find_Facts/Tools/find_facts_index	Fri Jan 31 17:01:27 2025 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: index sessions for Find_Facts
-
-isabelle scala_build || exit $?
-
-eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
-
-classpath "$SOLR_JARS"
-
-exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Index_Tool "$@"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/Tools/find_facts_server
--- a/src/Tools/Find_Facts/Tools/find_facts_server	Fri Jan 31 17:01:27 2025 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: run server for Find_Facts
-
-isabelle scala_build || exit $?
-
-eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
-
-classpath "$SOLR_JARS"
-
-exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Server_Tool "$@"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/etc/settings
--- a/src/Tools/Find_Facts/etc/settings	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Fri Jan 31 17:01:52 2025 +0100
@@ -2,6 +2,11 @@
 
 FIND_FACTS_HOME="$COMPONENT"
 FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts"
-FIND_FACTS_INDEXES=""
 
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
+if [ -d "$FIND_FACTS_HOME/lib/find_facts-isabelle" ]; then
+  FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/find_facts-isabelle"
+else
+  FIND_FACTS_INDEXES=""
+fi
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/lib/Tools"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/lib/Tools/find_facts_index
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/lib/Tools/find_facts_index	Fri Jan 31 17:01:52 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: index sessions for Find_Facts
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Index_Tool "$@"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/lib/Tools/find_facts_server
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/lib/Tools/find_facts_server	Fri Jan 31 17:01:52 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: run server for Find_Facts
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Server_Tool "$@"
diff -r 9c33627cea18 -r 2ca4fa5d1268 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Jan 31 17:01:27 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Jan 31 17:01:52 2025 +0100
@@ -748,7 +748,7 @@
 
     Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
     component_dir.write_settings(
-      "FIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
+      "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
   }