merged
authorFabian Huch <huch@in.tum.de>
Fri, 14 Feb 2025 17:40:21 +0100
changeset 82170 2cc21c84232d
parent 82169 338572994dae (diff)
parent 82162 5ecd0209c0a8 (current diff)
child 82171 3f3769c50bf5
merged
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Fri Feb 14 17:40:21 2025 +0100
@@ -504,7 +504,7 @@
             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.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)
--- a/src/Tools/Find_Facts/etc/options	Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Tools/Find_Facts/etc/options	Fri Feb 14 17:40:21 2025 +0100
@@ -3,9 +3,3 @@
 section "Find Facts"
 
 option find_facts_database_name : string = "local"
-
-option find_facts_url_library : string = "https://isabelle.in.tum.de/dist/library/"
-  -- "base URL for Isabelle HTML presentation"
-
-option find_facts_url_afp : string = "https://www.isa-afp.org/browser_info/current/"
-  -- "base URL for AFP HTML presentation"
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 14 17:40:21 2025 +0100
@@ -115,6 +115,11 @@
   val solr_data_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/solr")
 
   object private_data extends Solr.Data("find_facts") {
+    /* meta info */
+
+    val browser_info_database = new Properties.String("browser_info_database")
+
+
     /* types */
 
     val symbol_codes =
@@ -447,6 +452,18 @@
     }
   }
 
+  def meta_info(browser_info_database: Option[Path] = None): Properties.T =
+    browser_info_database match {
+      case Some(path) => Find_Facts.private_data.browser_info_database(path.implode)
+      case None => Nil
+    }
+
+  def browser_info_database(db: Solr.Database): Path =
+    db.props match {
+      case Find_Facts.private_data.browser_info_database(file) => db.dir + Path.explode(file)
+      case _ => Browser_Info.default_database
+    }
+
   def query_block(db: Solr.Database, id: String): Option[Block] = {
     val q = Solr.filter(Find_Facts.private_data.Fields.id, Solr.phrase(id))
     Find_Facts.private_data.read_blocks(db, q, Nil).blocks.headOption
@@ -473,7 +490,7 @@
   def make_thy_blocks(
     options: Options,
     session: Session,
-    browser_info_context: Browser_Info.Context,
+    context: Browser_Info.Context,
     document_info: Document_Info,
     theory_context: Export.Theory_Context,
     snapshot: Document.Snapshot,
@@ -486,7 +503,7 @@
     val theory_info =
       document_info.theory_by_name(session_name, theory).getOrElse(
         error("No info for theory " + theory))
-    val thy_dir = browser_info_context.theory_dir(theory_info)
+    val thy_dir = context.theory_dir(theory_info)
 
     def make_node_blocks(
       snapshot: Document.Snapshot,
@@ -494,7 +511,7 @@
     ): List[Block] = {
       val version = snapshot.version.id
       val file = Path.explode(snapshot.node_name.node).squash.implode
-      val url_path = thy_dir + browser_info_context.smart_html(theory_info, snapshot.node_name.node)
+      val url_path = thy_dir + context.smart_html(theory_info, snapshot.node_name.node)
 
       val elements =
         Browser_Info.Elements(html = Browser_Info.default_elements.html - Markup.ENTITY)
@@ -585,13 +602,13 @@
     isabelle_home: Path = Path.current,
     options: List[Options.Spec] = Nil,
     dirs: List[Path] = Nil,
-    clean: Boolean = false,
+    browser_info: Boolean = true,
     no_build: Boolean = false,
     verbose: Boolean = false,
   ): String = {
     ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
-      if_proper(clean, " -c") +
+      if_proper(!browser_info, " -N") +
       if_proper(no_build, " -n") +
       if_proper(verbose, " -v") +
       Options.Spec.bash_strings(options, bg = true) +
@@ -603,7 +620,7 @@
     sessions: List[String],
     afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
-    clean: Boolean = false,
+    browser_info: Boolean = true,
     progress: Progress = new Progress
   ): Unit = {
     val store = Store(options)
@@ -615,47 +632,62 @@
     val session_structure =
       Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection)
     val deps = Sessions.Deps.load(session_structure)
-    val browser_info_context = Browser_Info.context(session_structure)
+    val context = Browser_Info.context(session_structure)
 
     if (sessions.isEmpty) progress.echo("Nothing to index")
     else {
-      val start_date = Date.now()
-      val stats =
-        using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
-          using(Export.open_database_context(store)) { database_context =>
-            val document_info = Document_Info.read(database_context, deps, sessions)
-
-            def index_session(session_name: String): Unit = {
-              using(database_context.open_session0(session_name)) { session_context =>
-                val info = session_structure(session_name)
-                progress.echo("Session " + info.chapter + "/" + session_name + " ...")
+      Isabelle_System.with_tmp_dir("browser_info") { root_dir =>
+        val start_date = Date.now()
+        val props = meta_info(if (browser_info) Some(Path.basic("browser_info.db")) else None)
+        val stats =
+          using(solr.init_database(database, Find_Facts.private_data, props, clean = true)) { db =>
+            using(Export.open_database_context(store)) { database_context =>
+              val document_info = Document_Info.read(database_context, deps, sessions)
+              val context1 =
+                Browser_Info.context(session_structure, root_dir = root_dir,
+                  document_info = document_info)
+              if (browser_info) context1.update_root()
 
-                Find_Facts.private_data.delete_session(db, session_name)
-                deps(session_name).proper_session_theories.foreach { name =>
-                  val theory_context = session_context.theory(name.theory)
-                  Build.read_theory(theory_context) match {
-                    case None => progress.echo_warning("No snapshot for theory " + name.theory)
-                    case Some(snapshot) =>
-                      progress.echo("Indexing theory " + quote(name.theory), verbose = true)
-                      val blocks =
-                        make_thy_blocks(options, session, browser_info_context, document_info,
-                          theory_context, snapshot, info.chapter)
-                      Find_Facts.private_data.update_theory(db, theory_context.theory, blocks)
+              def index_session(session_name: String): Unit = {
+                val background =
+                  if (browser_info) deps.background(session_name)
+                  else Sessions.background0(session_name)
+                using(database_context.open_session(background)) { session_context =>
+                  val info = session_structure(session_name)
+                  progress.echo("Session " + info.chapter + "/" + session_name + " ...")
+
+                  if (browser_info) Browser_Info.build_session(context1, session_context)
+
+                  Find_Facts.private_data.delete_session(db, session_name)
+                  deps(session_name).proper_session_theories.foreach { name =>
+                    val theory_context = session_context.theory(name.theory)
+                    Build.read_theory(theory_context) match {
+                      case None => progress.echo_warning("No snapshot for theory " + name.theory)
+                      case Some(snapshot) =>
+                        progress.echo("Indexing theory " + quote(name.theory), verbose = true)
+                        val blocks =
+                          make_thy_blocks(options, session, context, document_info, theory_context,
+                            snapshot, info.chapter)
+                        Find_Facts.private_data.update_theory(db, theory_context.theory, blocks)
+                    }
                   }
                 }
               }
+
+              Par_List.map(index_session, sessions)
+
+              if (browser_info)
+                Browser_Info.make_database(db.dir + Path.basic("browser_info.db"), root_dir)
             }
 
-            Par_List.map(index_session, sessions)
+            val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
+            Find_Facts.query_stats(db, query)
           }
 
-          val query = Query(Field_Filter(Field.session, sessions.map(Atom.Exact(_))))
-          Find_Facts.query_stats(db, query)
-        }
-
-      val timing = Date.now() - start_date
-      progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
-        stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
+        val timing = Date.now() - start_date
+        progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
+          stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
+      }
     }
   }
 
@@ -665,7 +697,7 @@
   def main_tool1(args: Array[String]): Unit = {
     Command_Line.tool {
       var afp_root: Option[Path] = None
-      var clean = false
+      var browser_info = true
       val dirs_buffer = new mutable.ListBuffer[Path]
       var no_build = false
       var options = Options.init()
@@ -676,7 +708,7 @@
 
     Options are:
       -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
-      -c           clean previous index
+      -N           no html presentation -- use """ + Browser_Info.default_database.implode + """
       -d DIR       include session directory
       -n           no build -- take existing session build databases
       -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -685,7 +717,7 @@
     Build and index sessions for Find_Facts.
   """,
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
-        "c" -> (_ => clean = true),
+        "N" -> (_ => browser_info = false),
         "d:" -> (arg => dirs_buffer += Path.explode(arg)),
         "n" -> (_ => no_build = true),
         "o:" -> (arg => options = options + arg),
@@ -719,8 +751,8 @@
 
       /* index */
 
-      find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
-        progress = progress)
+      find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root,
+        browser_info = browser_info, progress = progress)
     }
   }
 
@@ -833,14 +865,9 @@
 
   case class Result(blocks: Blocks, facets: Facets)
 
-  class Encode(options: Options) {
-    val library_base_url = Url(options.string("find_facts_url_library"))
-    val afp_base_url = Url(options.string("find_facts_url_afp"))
-
-    def url(block: Block): Url = {
-      val base_url = if (block.chapter == AFP.chapter) afp_base_url else library_base_url
-      base_url.resolve(block.url_path.implode)
-    }
+  object Encode {
+    def print_url(block: Block): String = 
+      HTTP.Browser_Info_Service.name + "/" + block.url_path.implode
 
     def block(block: Block): JSON.T =
       JSON.Object(
@@ -850,7 +877,7 @@
         "theory" -> block.theory,
         "file" -> block.file,
         "file_name" -> block.file_name,
-        "url" -> url(block).toString,
+        "url" -> print_url(block),
         "command" -> block.command,
         "start_line" -> block.start_line,
         "src_before" -> block.src_before,
@@ -951,7 +978,6 @@
     progress: Progress = new Progress
   ): Unit = {
     val database = options.string("find_facts_database_name")
-    val encode = new Encode(options)
 
     def rebuild(): String = {
       build_html(default_web_dir + web_html, progress = progress)
@@ -976,6 +1002,7 @@
         HTTP.server(port, name = "", services = List(
           HTTP.Fonts_Service,
           HTTP.CSS_Service,
+          HTTP.Browser_Info(database = browser_info_database(db)),
           new HTTP.Service("find_facts") {
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               if (request.toplevel) Some(HTTP.Response.html(if (devel) rebuild() else html))
@@ -991,19 +1018,19 @@
               for {
                 request <- Parse.query_block(body)
                 block <- query_block(db, request)
-              } yield encode.block(block)
+              } yield Encode.block(block)
           },
           new HTTP.REST_Service("api/blocks", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =
               for (request <- Parse.query_blocks(body))
-              yield encode.blocks(query_blocks(db, request.query, Some(request.cursor)))
+              yield Encode.blocks(query_blocks(db, request.query, Some(request.cursor)))
           },
           new HTTP.REST_Service("api/query", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =
               for (query <- Parse.query(body)) yield {
                 val facet = query_facet(db, query)
                 val blocks = query_blocks(db, query)
-                encode.result(Result(blocks, facet))
+                Encode.result(Result(blocks, facet))
               }
           }))
 
--- a/src/Tools/Find_Facts/src/solr.scala	Fri Feb 14 15:24:42 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Fri Feb 14 17:40:21 2025 +0100
@@ -11,6 +11,8 @@
 
 import isabelle._
 
+import java.util.{Properties => JProperties}
+
 import scala.jdk.CollectionConverters._
 
 import org.apache.solr.client.solrj.embedded.EmbeddedSolrServer
@@ -346,7 +348,12 @@
   class System private[Solr](val solr_data: Path) {
     def database_dir(database: String): Path = solr_data + Path.basic(database)
 
-    def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+    def init_database(
+      database: String,
+      data: Data,
+      props: Properties.T = Nil,
+      clean: Boolean = false
+    ): Database = {
       val db_dir = database_dir(database)
 
       if (clean) Isabelle_System.rm_tree(db_dir)
@@ -354,6 +361,12 @@
       val conf_dir = db_dir + Path.basic("conf")
       if (!conf_dir.is_dir) {
         Isabelle_System.make_directory(conf_dir)
+
+        val jprops = new JProperties
+        for ((key, value) <- props) jprops.put(key, value)
+        jprops.setProperty("name", database)
+        jprops.store(File.writer((db_dir + Path.basic("core.properties")).file), null)
+
         File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
         File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
         data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
@@ -365,17 +378,23 @@
     def open_database(database: String): Database =
       if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
       else {
+        val jprops = File.read_props(database_dir(database) + Path.basic("core.properties"))
+        val props =
+          (for (key <- jprops.stringPropertyNames().iterator().asScala)
+          yield key -> jprops.getProperty(key)).toList
+
         val server = new EmbeddedSolrServer(solr_data.java_path, database)
   
         val cores = server.getCoreContainer.getAllCoreNames.asScala
         if (cores.contains(database)) server.getCoreContainer.reload(database)
         else server.getCoreContainer.create(database, Map.empty.asJava)
   
-        new Database(server)
+        new Database(props, database_dir(database), server)
       }
   }
 
-  class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {
+  class Database private[Solr](val props: Properties.T, val dir: Path, solr: EmbeddedSolrServer)
+    extends AutoCloseable {
     override def close(): Unit = solr.close()
 
     def execute_query[A](