support for build_database_server (PostgreSQL);
authorwenzelm
Sat May 19 20:05:13 2018 +0200 (14 months ago)
changeset 68221dbef88c2b6c5
parent 68220 8fc4e3d1df86
child 68222 3c1a716e7f59
support for build_database_server (PostgreSQL);
clarified signature;
etc/options
src/Pure/Admin/build_history.scala
src/Pure/ML/ml_process.scala
src/Pure/Thy/export.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/etc/options	Sat May 19 16:13:39 2018 +0200
     1.2 +++ b/etc/options	Sat May 19 20:05:13 2018 +0200
     1.3 @@ -250,11 +250,24 @@
     1.4    -- "maximum number of messages to keep SSH server connection alive"
     1.5  
     1.6  
     1.7 -section "Theory export"
     1.8 +section "Theory Export"
     1.9  
    1.10  option export_theory : bool = false
    1.11  
    1.12  
    1.13 +section "Build Database"
    1.14 +
    1.15 +option build_database_server : bool = false
    1.16 +option build_database_user : string = ""
    1.17 +option build_database_password : string = ""
    1.18 +option build_database_name : string = ""
    1.19 +option build_database_host : string = ""
    1.20 +option build_database_port : int = 0
    1.21 +option build_database_ssh_host : string = ""
    1.22 +option build_database_ssh_user : string = ""
    1.23 +option build_database_ssh_port : int = 0
    1.24 +
    1.25 +
    1.26  section "Build Log Database"
    1.27  
    1.28  option build_log_database_user : string = ""
     2.1 --- a/src/Pure/Admin/build_history.scala	Sat May 19 16:13:39 2018 +0200
     2.2 +++ b/src/Pure/Admin/build_history.scala	Sat May 19 20:05:13 2018 +0200
     2.3 @@ -245,7 +245,7 @@
     2.4  
     2.5        /* output log */
     2.6  
     2.7 -      val store = Sessions.store(options)
     2.8 +      val store = Sessions.store(options + "build_database_server=false")
     2.9  
    2.10        val meta_info =
    2.11          Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
     3.1 --- a/src/Pure/ML/ml_process.scala	Sat May 19 16:13:39 2018 +0200
     3.2 +++ b/src/Pure/ML/ml_process.scala	Sat May 19 20:05:13 2018 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4            sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
     3.5              .selection(selection)
     3.6          selected_sessions.build_requirements(List(logic_name)).
     3.7 -          map(a => File.platform_path(_store.heap(a)))
     3.8 +          map(a => File.platform_path(_store.the_heap(a)))
     3.9        }
    3.10  
    3.11      val eval_init =
     4.1 --- a/src/Pure/Thy/export.scala	Sat May 19 16:13:39 2018 +0200
     4.2 +++ b/src/Pure/Thy/export.scala	Sat May 19 20:05:13 2018 +0200
     4.3 @@ -151,8 +151,6 @@
     4.4    {
     4.5      val xz_cache = XZ.make_cache()
     4.6  
     4.7 -    db.create_table(Data.table)
     4.8 -
     4.9      private val export_errors = Synchronized[List[String]](Nil)
    4.10  
    4.11      private val consumer =
     5.1 --- a/src/Pure/Thy/sessions.scala	Sat May 19 16:13:39 2018 +0200
     5.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 19 20:05:13 2018 +0200
     5.3 @@ -969,22 +969,15 @@
     5.4      override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
     5.5  
     5.6  
     5.7 -    /* file names */
     5.8 -
     5.9 -    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
    5.10 -    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    5.11 -    def log_gz(name: String): Path = log(name).ext("gz")
    5.12 -
    5.13 -
    5.14      /* directories */
    5.15  
    5.16 -    def system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
    5.17 -    def user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
    5.18 +    val system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
    5.19 +    val user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
    5.20  
    5.21 -    def output_dir: Path =
    5.22 +    val output_dir: Path =
    5.23        if (system_mode) system_output_dir else user_output_dir
    5.24  
    5.25 -    def input_dirs: List[Path] =
    5.26 +    val input_dirs: List[Path] =
    5.27        if (system_mode) List(system_output_dir)
    5.28        else List(user_output_dir, system_output_dir)
    5.29  
    5.30 @@ -993,53 +986,95 @@
    5.31        else Path.explode("$ISABELLE_BROWSER_INFO")
    5.32  
    5.33  
    5.34 -    /* output */
    5.35 +    /* file names */
    5.36  
    5.37 -    def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    5.38 +    def heap(name: String): Path = Path.basic(name)
    5.39 +    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
    5.40 +    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    5.41 +    def log_gz(name: String): Path = log(name).ext("gz")
    5.42  
    5.43 -    def output_heap(name: String): Path = output_dir + Path.basic(name)
    5.44 +    def output_heap(name: String): Path = output_dir + heap(name)
    5.45 +    def output_database(name: String): Path = output_dir + database(name)
    5.46      def output_log(name: String): Path = output_dir + log(name)
    5.47      def output_log_gz(name: String): Path = output_dir + log_gz(name)
    5.48  
    5.49 -    def open_output_database(name: String): SQL.Database =
    5.50 -      SQLite.open_database(output_dir + database(name))
    5.51 -
    5.52 -    def clean_output(name: String): (Boolean, Boolean) =
    5.53 -    {
    5.54 -      val res =
    5.55 -        for {
    5.56 -          dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
    5.57 -          file <- List(Path.basic(name), database(name), log(name), log_gz(name))
    5.58 -          path = dir + file if path.is_file
    5.59 -        } yield path.file.delete
    5.60 -      val relevant = res.nonEmpty
    5.61 -      val ok = res.forall(b => b)
    5.62 -      (relevant, ok)
    5.63 -    }
    5.64 +    def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    5.65  
    5.66  
    5.67 -    /* input */
    5.68 +    /* heap */
    5.69  
    5.70      def find_heap(name: String): Option[Path] =
    5.71 -      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    5.72 +      input_dirs.map(_ + heap(name)).find(_.is_file)
    5.73  
    5.74      def find_heap_digest(name: String): Option[String] =
    5.75        find_heap(name).flatMap(read_heap_digest(_))
    5.76  
    5.77 -    def find_database(name: String): Option[Path] =
    5.78 -      input_dirs.map(_ + database(name)).find(_.is_file)
    5.79 +    def the_heap(name: String): Path =
    5.80 +      find_heap(name) getOrElse
    5.81 +        error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
    5.82 +          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
    5.83 +
    5.84 +
    5.85 +    /* database */
    5.86 +
    5.87 +    private def database_server: Boolean = options.bool("build_database_server")
    5.88  
    5.89 -    def try_open_database(name: String): Option[SQL.Database] =
    5.90 -      find_database(name).map(SQLite.open_database(_))
    5.91 +    def access_database(name: String, output: Boolean = false): Option[SQL.Database] =
    5.92 +    {
    5.93 +      if (database_server) {
    5.94 +        val db =
    5.95 +          PostgreSQL.open_database(
    5.96 +            user = options.string("build_database_user"),
    5.97 +            password = options.string("build_database_password"),
    5.98 +            database = options.string("build_database_name"),
    5.99 +            host = options.string("build_database_host"),
   5.100 +            port = options.int("build_database_port"),
   5.101 +            ssh =
   5.102 +              proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
   5.103 +                SSH.open_session(options,
   5.104 +                  host = ssh_host,
   5.105 +                  user = options.string("build_database_ssh_user"),
   5.106 +                  port = options.int("build_database_ssh_port"))),
   5.107 +            ssh_close = true)
   5.108 +        if (output || has_session_info(db, name)) Some(db) else { db.close; None }
   5.109 +      }
   5.110 +      else if (output) Some(SQLite.open_database(output_database(name)))
   5.111 +      else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database(_))
   5.112 +    }
   5.113  
   5.114 -    private def error_input(msg: String): Nothing =
   5.115 -      error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
   5.116 +    def open_database(name: String, output: Boolean = false): SQL.Database =
   5.117 +      access_database(name, output = output) getOrElse
   5.118 +        error("Missing build database for session " + quote(name))
   5.119  
   5.120 -    def heap(name: String): Path =
   5.121 -      find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name))
   5.122 +    def clean_output(name: String): (Boolean, Boolean) =
   5.123 +    {
   5.124 +      val relevant_db =
   5.125 +        database_server &&
   5.126 +        {
   5.127 +          access_database(name) match {
   5.128 +            case Some(db) =>
   5.129 +              try {
   5.130 +                db.transaction {
   5.131 +                  val relevant_db = has_session_info(db, name)
   5.132 +                  init_session_info(db, name)
   5.133 +                  relevant_db
   5.134 +                }
   5.135 +              } finally { db.close }
   5.136 +            case None => false
   5.137 +          }
   5.138 +        }
   5.139  
   5.140 -    def open_database(name: String): SQL.Database =
   5.141 -      try_open_database(name) getOrElse error("Missing database file for session " + quote(name))
   5.142 +      val del =
   5.143 +        for {
   5.144 +          dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
   5.145 +          file <- List(heap(name), database(name), log(name), log_gz(name))
   5.146 +          path = dir + file if path.is_file
   5.147 +        } yield path.file.delete
   5.148 +
   5.149 +      val relevant = relevant_db || del.nonEmpty
   5.150 +      val ok = del.forall(b => b)
   5.151 +      (relevant, ok)
   5.152 +    }
   5.153  
   5.154  
   5.155      /* SQL database content */
   5.156 @@ -1068,6 +1103,22 @@
   5.157          db.create_table(Session_Info.table)
   5.158          db.using_statement(
   5.159            Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
   5.160 +
   5.161 +        db.create_table(Export.Data.table)
   5.162 +        db.using_statement(
   5.163 +          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
   5.164 +      }
   5.165 +    }
   5.166 +
   5.167 +    def has_session_info(db: SQL.Database, name: String): Boolean =
   5.168 +    {
   5.169 +      db.transaction {
   5.170 +        db.tables.contains(Session_Info.table.name) &&
   5.171 +        {
   5.172 +          db.using_statement(
   5.173 +            Session_Info.table.select(List(Session_Info.session_name),
   5.174 +              Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
   5.175 +        }
   5.176        }
   5.177      }
   5.178  
     6.1 --- a/src/Pure/Tools/build.scala	Sat May 19 16:13:39 2018 +0200
     6.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 20:05:13 2018 +0200
     6.3 @@ -38,7 +38,7 @@
     6.4      {
     6.5        val no_timings: Timings = (Nil, 0.0)
     6.6  
     6.7 -      store.try_open_database(name) match {
     6.8 +      store.access_database(name) match {
     6.9          case None => no_timings
    6.10          case Some(db) =>
    6.11            def ignore_error(msg: String) =
    6.12 @@ -189,7 +189,7 @@
    6.13      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
    6.14  
    6.15      private val export_tmp_dir = Isabelle_System.tmp_dir("export")
    6.16 -    private val export_consumer = Export.consumer(store.open_output_database(name))
    6.17 +    private val export_consumer = Export.consumer(store.open_database(name, output = true))
    6.18  
    6.19      private val future_result: Future[Process_Result] =
    6.20        Future.thread("build") {
    6.21 @@ -425,7 +425,7 @@
    6.22        if (soft_build && !fresh_build) {
    6.23          val outdated =
    6.24            deps0.sessions_structure.build_topological_order.flatMap(name =>
    6.25 -            store.try_open_database(name) match {
    6.26 +            store.access_database(name) match {
    6.27                case Some(db) =>
    6.28                  using(db)(store.read_build(_, name)) match {
    6.29                    case Some(build)
    6.30 @@ -546,7 +546,7 @@
    6.31                      ml_statistics = true,
    6.32                      task_statistics = true)
    6.33  
    6.34 -              using(store.open_output_database(name))(db =>
    6.35 +              using(store.open_database(name, output = true))(db =>
    6.36                  store.write_session_info(db, name,
    6.37                    build_log =
    6.38                      if (process_result.timeout) build_log.error("Timeout") else build_log,
    6.39 @@ -581,7 +581,7 @@
    6.40  
    6.41                  val (current, heap_digest) =
    6.42                  {
    6.43 -                  store.try_open_database(name) match {
    6.44 +                  store.access_database(name) match {
    6.45                      case Some(db) =>
    6.46                        using(db)(store.read_build(_, name)) match {
    6.47                          case Some(build) =>
    6.48 @@ -613,7 +613,7 @@
    6.49                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    6.50  
    6.51                    store.clean_output(name)
    6.52 -                  using(store.open_output_database(name))(store.init_session_info(_, name))
    6.53 +                  using(store.open_database(name, output = true))(store.init_session_info(_, name))
    6.54  
    6.55                    val numa_node = numa_nodes.next(used_node(_))
    6.56                    val job =