copy instead of symlink managed Find_Facts indexes: portable, and allows updating with local sessions;
authorFabian Huch <huch@in.tum.de>
Wed, 22 Jan 2025 10:35:17 +0100
changeset 81895 9d1003cb9844
parent 81894 dffa88c87a08
child 81896 db9bf651701d
copy instead of symlink managed Find_Facts indexes: portable, and allows updating with local sessions;
src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 17:28:09 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Wed Jan 22 10:35:17 2025 +0100
@@ -721,12 +721,13 @@
 
   /** index components **/
 
-  def resolve_indexes(solr: Solr.System): Unit = {
-    // non-portable: only for Linux or macOS
-    for (path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))) {
-      Isabelle_System.symlink(path.absolute, solr.solr_data, force = true)
-    }
-  }
+  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 find_facts_index_build(
     database: String,