--- a/etc/options Sat May 19 16:13:39 2018 +0200
+++ b/etc/options Sat May 19 20:05:13 2018 +0200
@@ -250,11 +250,24 @@
-- "maximum number of messages to keep SSH server connection alive"
-section "Theory export"
+section "Theory Export"
option export_theory : bool = false
+section "Build Database"
+
+option build_database_server : bool = false
+option build_database_user : string = ""
+option build_database_password : string = ""
+option build_database_name : string = ""
+option build_database_host : string = ""
+option build_database_port : int = 0
+option build_database_ssh_host : string = ""
+option build_database_ssh_user : string = ""
+option build_database_ssh_port : int = 0
+
+
section "Build Log Database"
option build_log_database_user : string = ""
--- a/src/Pure/Admin/build_history.scala Sat May 19 16:13:39 2018 +0200
+++ b/src/Pure/Admin/build_history.scala Sat May 19 20:05:13 2018 +0200
@@ -245,7 +245,7 @@
/* output log */
- val store = Sessions.store(options)
+ val store = Sessions.store(options + "build_database_server=false")
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
--- a/src/Pure/ML/ml_process.scala Sat May 19 16:13:39 2018 +0200
+++ b/src/Pure/ML/ml_process.scala Sat May 19 20:05:13 2018 +0200
@@ -38,7 +38,7 @@
sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
.selection(selection)
selected_sessions.build_requirements(List(logic_name)).
- map(a => File.platform_path(_store.heap(a)))
+ map(a => File.platform_path(_store.the_heap(a)))
}
val eval_init =
--- a/src/Pure/Thy/export.scala Sat May 19 16:13:39 2018 +0200
+++ b/src/Pure/Thy/export.scala Sat May 19 20:05:13 2018 +0200
@@ -151,8 +151,6 @@
{
val xz_cache = XZ.make_cache()
- db.create_table(Data.table)
-
private val export_errors = Synchronized[List[String]](Nil)
private val consumer =
--- a/src/Pure/Thy/sessions.scala Sat May 19 16:13:39 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Sat May 19 20:05:13 2018 +0200
@@ -969,22 +969,15 @@
override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
- /* file names */
-
- def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
- def log(name: String): Path = Path.basic("log") + Path.basic(name)
- def log_gz(name: String): Path = log(name).ext("gz")
-
-
/* directories */
- def system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
- def user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
+ val system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
+ val user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
- def output_dir: Path =
+ val output_dir: Path =
if (system_mode) system_output_dir else user_output_dir
- def input_dirs: List[Path] =
+ val input_dirs: List[Path] =
if (system_mode) List(system_output_dir)
else List(user_output_dir, system_output_dir)
@@ -993,53 +986,95 @@
else Path.explode("$ISABELLE_BROWSER_INFO")
- /* output */
+ /* file names */
- def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
+ def heap(name: String): Path = Path.basic(name)
+ def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
+ def log(name: String): Path = Path.basic("log") + Path.basic(name)
+ def log_gz(name: String): Path = log(name).ext("gz")
- def output_heap(name: String): Path = output_dir + Path.basic(name)
+ def output_heap(name: String): Path = output_dir + heap(name)
+ def output_database(name: String): Path = output_dir + database(name)
def output_log(name: String): Path = output_dir + log(name)
def output_log_gz(name: String): Path = output_dir + log_gz(name)
- def open_output_database(name: String): SQL.Database =
- SQLite.open_database(output_dir + database(name))
-
- def clean_output(name: String): (Boolean, Boolean) =
- {
- val res =
- for {
- dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
- file <- List(Path.basic(name), database(name), log(name), log_gz(name))
- path = dir + file if path.is_file
- } yield path.file.delete
- val relevant = res.nonEmpty
- val ok = res.forall(b => b)
- (relevant, ok)
- }
+ def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
- /* input */
+ /* heap */
def find_heap(name: String): Option[Path] =
- input_dirs.map(_ + Path.basic(name)).find(_.is_file)
+ input_dirs.map(_ + heap(name)).find(_.is_file)
def find_heap_digest(name: String): Option[String] =
find_heap(name).flatMap(read_heap_digest(_))
- def find_database(name: String): Option[Path] =
- input_dirs.map(_ + database(name)).find(_.is_file)
+ def the_heap(name: String): Path =
+ find_heap(name) getOrElse
+ error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
+ cat_lines(input_dirs.map(dir => " " + dir.expand.implode)))
+
+
+ /* database */
+
+ private def database_server: Boolean = options.bool("build_database_server")
- def try_open_database(name: String): Option[SQL.Database] =
- find_database(name).map(SQLite.open_database(_))
+ def access_database(name: String, output: Boolean = false): Option[SQL.Database] =
+ {
+ if (database_server) {
+ val db =
+ PostgreSQL.open_database(
+ user = options.string("build_database_user"),
+ password = options.string("build_database_password"),
+ database = options.string("build_database_name"),
+ host = options.string("build_database_host"),
+ port = options.int("build_database_port"),
+ ssh =
+ proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
+ SSH.open_session(options,
+ host = ssh_host,
+ user = options.string("build_database_ssh_user"),
+ port = options.int("build_database_ssh_port"))),
+ ssh_close = true)
+ if (output || has_session_info(db, name)) Some(db) else { db.close; None }
+ }
+ else if (output) Some(SQLite.open_database(output_database(name)))
+ else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database(_))
+ }
- private def error_input(msg: String): Nothing =
- error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode)))
+ def open_database(name: String, output: Boolean = false): SQL.Database =
+ access_database(name, output = output) getOrElse
+ error("Missing build database for session " + quote(name))
- def heap(name: String): Path =
- find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name))
+ def clean_output(name: String): (Boolean, Boolean) =
+ {
+ val relevant_db =
+ database_server &&
+ {
+ access_database(name) match {
+ case Some(db) =>
+ try {
+ db.transaction {
+ val relevant_db = has_session_info(db, name)
+ init_session_info(db, name)
+ relevant_db
+ }
+ } finally { db.close }
+ case None => false
+ }
+ }
- def open_database(name: String): SQL.Database =
- try_open_database(name) getOrElse error("Missing database file for session " + quote(name))
+ val del =
+ for {
+ dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
+ file <- List(heap(name), database(name), log(name), log_gz(name))
+ path = dir + file if path.is_file
+ } yield path.file.delete
+
+ val relevant = relevant_db || del.nonEmpty
+ val ok = del.forall(b => b)
+ (relevant, ok)
+ }
/* SQL database content */
@@ -1068,6 +1103,22 @@
db.create_table(Session_Info.table)
db.using_statement(
Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
+
+ db.create_table(Export.Data.table)
+ db.using_statement(
+ Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
+ }
+ }
+
+ def has_session_info(db: SQL.Database, name: String): Boolean =
+ {
+ db.transaction {
+ db.tables.contains(Session_Info.table.name) &&
+ {
+ db.using_statement(
+ Session_Info.table.select(List(Session_Info.session_name),
+ Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
+ }
}
}
--- a/src/Pure/Tools/build.scala Sat May 19 16:13:39 2018 +0200
+++ b/src/Pure/Tools/build.scala Sat May 19 20:05:13 2018 +0200
@@ -38,7 +38,7 @@
{
val no_timings: Timings = (Nil, 0.0)
- store.try_open_database(name) match {
+ store.access_database(name) match {
case None => no_timings
case Some(db) =>
def ignore_error(msg: String) =
@@ -189,7 +189,7 @@
isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
private val export_tmp_dir = Isabelle_System.tmp_dir("export")
- private val export_consumer = Export.consumer(store.open_output_database(name))
+ private val export_consumer = Export.consumer(store.open_database(name, output = true))
private val future_result: Future[Process_Result] =
Future.thread("build") {
@@ -425,7 +425,7 @@
if (soft_build && !fresh_build) {
val outdated =
deps0.sessions_structure.build_topological_order.flatMap(name =>
- store.try_open_database(name) match {
+ store.access_database(name) match {
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build)
@@ -546,7 +546,7 @@
ml_statistics = true,
task_statistics = true)
- using(store.open_output_database(name))(db =>
+ using(store.open_database(name, output = true))(db =>
store.write_session_info(db, name,
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
@@ -581,7 +581,7 @@
val (current, heap_digest) =
{
- store.try_open_database(name) match {
+ store.access_database(name) match {
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build) =>
@@ -613,7 +613,7 @@
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
store.clean_output(name)
- using(store.open_output_database(name))(store.init_session_info(_, name))
+ using(store.open_database(name, output = true))(store.init_session_info(_, name))
val numa_node = numa_nodes.next(used_node(_))
val job =