# HG changeset patch # User Fabian Huch # Date 1739551221 -3600 # Node ID 2cc21c84232d6ba69fa6b5a143fa32e8812550b4 # Parent 338572994dae9a3d04fc9941b5719fdac625b9ca# Parent 5ecd0209c0a80db0c7574c94468215e6707677c4 merged diff -r 5ecd0209c0a8 -r 2cc21c84232d 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) diff -r 5ecd0209c0a8 -r 2cc21c84232d src/Tools/Find_Facts/etc/options --- 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" diff -r 5ecd0209c0a8 -r 2cc21c84232d src/Tools/Find_Facts/src/find_facts.scala --- 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)) } })) diff -r 5ecd0209c0a8 -r 2cc21c84232d src/Tools/Find_Facts/src/solr.scala --- 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](