# HG changeset patch
# User wenzelm
# Date 1740342161 -3600
# Node ID d3b401fe8188a9c136403cfb01e87892cb57d444
# Parent  979b63c3b4c1aa8d9315b6352961dc73adbbf80f
clarified component name and content for FIND_FACTS_INDEXES: prefer db with compression;

diff -r 979b63c3b4c1 -r d3b401fe8188 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sun Feb 23 15:48:08 2025 +0100
+++ b/src/Doc/System/Presentation.thy	Sun Feb 23 21:22:41 2025 +0100
@@ -221,9 +221,9 @@
   the search index can be specified via system option 
   @{system_option find_facts_database_name}. A finished search index can be
   packed for later use as a regular Isabelle component using the 
-  @{tool_def find_facts_index_build} tool: Initializing such a component
-  causes it to be added to the list of managed components in
-  @{setting FIND_FACTS_INDEXES}.
+  @{tool_def find_facts_index_build} tool, with a \<^verbatim>\<open>.db\<close> file and
+  \<^verbatim>\<open>etc/settings\<close> to augment @{setting FIND_FACTS_INDEXES} for use by @{tool
+  find_facts_server}.
 
   \<^medskip>
   The user interface of the search is available as web application that 
diff -r 979b63c3b4c1 -r d3b401fe8188 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun Feb 23 15:48:08 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Feb 23 21:22:41 2025 +0100
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import isabelle.find_facts.Find_Facts
+
 
 object Build_Release {
   /** release context **/
@@ -496,9 +498,9 @@
           val database_dir =
             other_isabelle.expand_path(
               Path.explode("$FIND_FACTS_HOME_USER/solr") + Path.basic(database_name))
-          val database_target_dir =
+          val database_target =
             other_isabelle.expand_path(
-              Path.explode("$FIND_FACTS_HOME/lib/find_facts-" + database_name))
+              Path.explode("$FIND_FACTS_HOME/lib") + Path.basic(database_name).db)
 
           val sessions =
             other_isabelle.bash("bin/isabelle sessions -a " + opt_dirs).check.out_lines
@@ -506,8 +508,7 @@
             "bin/isabelle find_facts_index -o find_facts_database_name=" +
               Bash.string(database_name) + " -n -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)
+          Find_Facts.make_database(database_target, database_dir)
 
           Isabelle_System.rm_tree(database_dir)
           database_dir.dir.file.delete  // "$FIND_FACTS_HOME_USER/solr"
diff -r 979b63c3b4c1 -r d3b401fe8188 src/Tools/Find_Facts/etc/settings
--- a/src/Tools/Find_Facts/etc/settings	Sun Feb 23 15:48:08 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Sun Feb 23 21:22:41 2025 +0100
@@ -3,8 +3,8 @@
 FIND_FACTS_HOME="$COMPONENT"
 FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts"
 
-if [ -d "$FIND_FACTS_HOME/lib/find_facts-isabelle" ]; then
-  FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/find_facts-isabelle"
+if [ -f "$FIND_FACTS_HOME/lib/isabelle.db" ]; then
+  FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/isabelle.db"
 else
   FIND_FACTS_INDEXES=""
 fi
diff -r 979b63c3b4c1 -r d3b401fe8188 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sun Feb 23 15:48:08 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Feb 23 21:22:41 2025 +0100
@@ -761,13 +761,23 @@
 
   /** index components **/
 
-  def resolve_indexes(solr: Solr.System): Unit =
-    for {
-      path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))
-      database = Library.perhaps_unprefix("find_facts-", path.file_name)
-      database_dir = solr.database_dir(database)
-      if !database_dir.is_dir
-    } Isabelle_System.copy_dir(path, database_dir, direct = true)
+  def resolve_indexes(solr: Solr.System, progress: Progress = new Progress): Unit = {
+    val compress_cache = Compress.Cache.make()
+    for (path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))) {
+      val database = path.drop_ext.file_name
+      val database_dir = solr.database_dir(database)
+      if (!database_dir.is_dir) {
+        progress.echo("Extracting " + path.expand)
+        Isabelle_System.make_directory(database_dir)
+        File_Store.database_extract(path, database_dir, compress_cache = compress_cache)
+      }
+    }
+  }
+
+  def make_database(database_path: Path, database_dir: Path): Unit =
+    File_Store.make_database(database_path, database_dir,
+      compress_options = Compress.Options_Zstd(level = 8),
+      compress_cache = Compress.Cache.make())
 
   def find_facts_index_build(
     database: String,
@@ -776,13 +786,15 @@
   ): Unit = {
     val solr = Solr.init(solr_data_dir)
 
-    val component = "find_facts-" + database
+    val component = "find_facts_" + database + "-" + Date.Format.alt_date(Date.now())
     val component_dir =
       Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
-    Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
+    val database_path = Path.basic(database).db
+    make_database(component_dir.path + database_path, solr.database_dir(database))
+
     component_dir.write_settings(
-      "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
+      "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database_path.implode + "\"")
   }
 
 
@@ -993,7 +1005,7 @@
     val web_assets = load_web_assets
 
     val solr = Solr.init(solr_data_dir)
-    resolve_indexes(solr)
+    resolve_indexes(solr, progress = progress)
 
     using(solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))