src/Pure/PIDE/headless.scala
author wenzelm
Thu Dec 27 16:56:53 2018 +0100 (7 months ago ago)
changeset 69532 16779868de1f
parent 69468 5655af3ea5bd
child 69548 892b68f932f9
permissions -rw-r--r--
clarified defaults via system options;
     1 /*  Title:      Pure/PIDE/headless.scala
     2     Author:     Makarius
     3 
     4 Headless PIDE session and resources from file-system.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Headless
    16 {
    17   /** session **/
    18 
    19   def start_session(
    20     options: Options,
    21     session_name: String,
    22     session_dirs: List[Path] = Nil,
    23     include_sessions: List[String] = Nil,
    24     session_base: Option[Sessions.Base] = None,
    25     print_mode: List[String] = Nil,
    26     progress: Progress = No_Progress,
    27     log: Logger = No_Logger): Session =
    28   {
    29     val base =
    30       session_base getOrElse
    31         Sessions.base_info(options, session_name, include_sessions = include_sessions,
    32           progress = progress, dirs = session_dirs).check_base
    33     val resources = new Resources(base, log = log)
    34     val session = new Session(session_name, options, resources)
    35 
    36     val session_error = Future.promise[String]
    37     var session_phase: Session.Consumer[Session.Phase] = null
    38     session_phase =
    39       Session.Consumer(getClass.getName) {
    40         case Session.Ready =>
    41           session.phase_changed -= session_phase
    42           session_error.fulfill("")
    43         case Session.Terminated(result) if !result.ok =>
    44           session.phase_changed -= session_phase
    45           session_error.fulfill("Session start failed: return code " + result.rc)
    46         case _ =>
    47       }
    48     session.phase_changed += session_phase
    49 
    50     progress.echo("Starting session " + session_name + " ...")
    51     Isabelle_Process.start(session, options,
    52       logic = session_name, dirs = session_dirs, modes = print_mode)
    53 
    54     session_error.join match {
    55       case "" => session
    56       case msg => session.stop(); error(msg)
    57     }
    58   }
    59 
    60   private def stable_snapshot(
    61     state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
    62   {
    63     val snapshot = state.snapshot(name)
    64     assert(version.id == snapshot.version.id)
    65     snapshot
    66   }
    67 
    68   class Use_Theories_Result private[Headless](
    69     val state: Document.State,
    70     val version: Document.Version,
    71     val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
    72     val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
    73   {
    74     def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
    75     {
    76       val committed = nodes_committed.iterator.map(_._1).toSet
    77       nodes.filter(p => !committed(p._1))
    78     }
    79 
    80     def snapshot(name: Document.Node.Name): Document.Snapshot =
    81       stable_snapshot(state, version, name)
    82 
    83     def ok: Boolean =
    84       (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
    85   }
    86 
    87   class Session private[Headless](
    88     session_name: String,
    89     _session_options: => Options,
    90     override val resources: Resources) extends isabelle.Session(_session_options, resources)
    91   {
    92     session =>
    93 
    94 
    95     /* options */
    96 
    97     def default_check_delay: Time = session_options.seconds("headless_check_delay")
    98     def default_check_limit: Int = session_options.int("headless_check_limit")
    99     def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")
   100     def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
   101     def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
   102 
   103 
   104     /* temporary directory */
   105 
   106     val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
   107     val tmp_dir_name: String = File.path(tmp_dir).implode
   108 
   109     def master_directory(master_dir: String): String =
   110       proper_string(master_dir) getOrElse tmp_dir_name
   111 
   112     override def toString: String = session_name
   113 
   114     override def stop(): Process_Result =
   115     {
   116       try { super.stop() }
   117       finally { Isabelle_System.rm_tree(tmp_dir) }
   118     }
   119 
   120 
   121     /* theories */
   122 
   123     private sealed case class Use_Theories_State(
   124       last_update: Time = Time.now(),
   125       nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
   126       already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
   127       result: Promise[Use_Theories_Result] = Future.promise[Use_Theories_Result])
   128     {
   129       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
   130         copy(last_update = Time.now(), nodes_status = new_nodes_status)
   131 
   132       def watchdog(watchdog_timeout: Time): Boolean =
   133         watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
   134 
   135       def cancel_result { result.cancel }
   136       def finished_result: Boolean = result.is_finished
   137       def await_result { result.join_result }
   138       def join_result: Use_Theories_Result = result.join
   139       def check_result(
   140           state: Document.State,
   141           version: Document.Version,
   142           dep_theories: List[Document.Node.Name],
   143           beyond_limit: Boolean,
   144           watchdog_timeout: Time,
   145           commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
   146         : Use_Theories_State =
   147       {
   148         val already_committed1 =
   149           if (commit.isDefined) {
   150             (already_committed /: dep_theories)({ case (committed, name) =>
   151               def parents_committed: Boolean =
   152                 version.nodes(name).header.imports.forall({ case (parent, _) =>
   153                   Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
   154                 })
   155               if (!committed.isDefinedAt(name) && parents_committed &&
   156                   state.node_consolidated(version, name))
   157               {
   158                 val snapshot = stable_snapshot(state, version, name)
   159                 val status = Document_Status.Node_Status.make(state, version, name)
   160                 commit.get.apply(snapshot, status)
   161                 committed + (name -> status)
   162               }
   163               else committed
   164             })
   165           }
   166           else already_committed
   167 
   168         if (beyond_limit || watchdog(watchdog_timeout) ||
   169           dep_theories.forall(name =>
   170             already_committed1.isDefinedAt(name) ||
   171             state.node_consolidated(version, name) ||
   172             nodes_status.quasi_consolidated(name)))
   173         {
   174           val nodes =
   175             for (name <- dep_theories)
   176             yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
   177           val nodes_committed =
   178             for {
   179               name <- dep_theories
   180               status <- already_committed1.get(name)
   181             } yield (name -> status)
   182 
   183           try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) }
   184           catch { case _: IllegalStateException => }
   185         }
   186 
   187         copy(already_committed = already_committed1)
   188       }
   189     }
   190 
   191     def use_theories(
   192       theories: List[String],
   193       qualifier: String = Sessions.DRAFT,
   194       master_dir: String = "",
   195       check_delay: Time = default_check_delay,
   196       check_limit: Int = default_check_limit,
   197       watchdog_timeout: Time = default_watchdog_timeout,
   198       nodes_status_delay: Time = default_nodes_status_delay,
   199       id: UUID.T = UUID.random(),
   200       // commit: must not block, must not fail
   201       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
   202       commit_cleanup_delay: Time = default_commit_cleanup_delay,
   203       progress: Progress = No_Progress): Use_Theories_Result =
   204     {
   205       val dep_theories =
   206       {
   207         val import_names =
   208           theories.map(thy =>
   209             resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
   210         resources.dependencies(import_names, progress = progress).check_errors.theories
   211       }
   212 
   213       val use_theories_state = Synchronized(Use_Theories_State())
   214 
   215       def check_result(beyond_limit: Boolean = false)
   216       {
   217         val state = session.current_state()
   218         state.stable_tip_version match {
   219           case Some(version) =>
   220             use_theories_state.change(
   221               _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
   222           case None =>
   223         }
   224       }
   225 
   226       val check_progress =
   227       {
   228         var check_count = 0
   229         Event_Timer.request(Time.now(), repeat = Some(check_delay))
   230           {
   231             if (progress.stopped) use_theories_state.value.cancel_result
   232             else {
   233               check_count += 1
   234               check_result(check_limit > 0 && check_count > check_limit)
   235             }
   236           }
   237       }
   238 
   239       val consumer =
   240       {
   241         val delay_nodes_status =
   242           Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
   243             progress.nodes_status(use_theories_state.value.nodes_status)
   244           }
   245 
   246         val delay_commit_clean =
   247           Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
   248             val clean = use_theories_state.value.already_committed.keySet
   249             resources.clean_theories(session, id, clean)
   250           }
   251 
   252         val dep_theories_set = dep_theories.toSet
   253 
   254         Session.Consumer[Session.Commands_Changed](getClass.getName) {
   255           case changed =>
   256             if (changed.nodes.exists(dep_theories_set)) {
   257               val snapshot = session.snapshot()
   258               val state = snapshot.state
   259               val version = snapshot.version
   260 
   261               val theory_progress =
   262                 use_theories_state.change_result(st =>
   263                   {
   264                     val domain =
   265                       if (st.nodes_status.is_empty) dep_theories_set
   266                       else changed.nodes.iterator.filter(dep_theories_set).toSet
   267 
   268                     val (nodes_status_changed, nodes_status1) =
   269                       st.nodes_status.update(resources, state, version,
   270                         domain = Some(domain), trim = changed.assignment)
   271 
   272                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
   273                       delay_nodes_status.invoke
   274                     }
   275 
   276                     val theory_progress =
   277                       (for {
   278                         (name, node_status) <- nodes_status1.present.iterator
   279                         if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
   280                         p1 = node_status.percentage
   281                         if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   282                       } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
   283 
   284                     (theory_progress, st.update(nodes_status1))
   285                   })
   286 
   287               theory_progress.foreach(progress.theory(_))
   288 
   289               check_result()
   290 
   291               if (commit.isDefined && commit_cleanup_delay > Time.zero) {
   292                 if (use_theories_state.value.finished_result)
   293                   delay_commit_clean.revoke
   294                 else delay_commit_clean.invoke
   295               }
   296             }
   297         }
   298       }
   299 
   300       try {
   301         session.commands_changed += consumer
   302         resources.load_theories(session, id, dep_theories, progress)
   303         use_theories_state.value.await_result
   304         check_progress.cancel
   305       }
   306       finally {
   307         session.commands_changed -= consumer
   308         resources.unload_theories(session, id, dep_theories)
   309       }
   310 
   311       use_theories_state.value.join_result
   312     }
   313 
   314     def purge_theories(
   315       theories: List[String],
   316       qualifier: String = Sessions.DRAFT,
   317       master_dir: String = "",
   318       all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
   319     {
   320       val nodes =
   321         if (all) None
   322         else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _)))
   323       resources.purge_theories(session, nodes)
   324     }
   325   }
   326 
   327 
   328 
   329   /** resources **/
   330 
   331   object Resources
   332   {
   333     final class Theory private[Headless](
   334       val node_name: Document.Node.Name,
   335       val node_header: Document.Node.Header,
   336       val text: String,
   337       val node_required: Boolean)
   338     {
   339       override def toString: String = node_name.toString
   340 
   341       def node_perspective: Document.Node.Perspective_Text =
   342         Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
   343 
   344       def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
   345         List(node_name -> Document.Node.Deps(node_header),
   346           node_name -> Document.Node.Edits(text_edits),
   347           node_name -> node_perspective)
   348 
   349       def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
   350       {
   351         val (text_edits, old_required) =
   352           if (old.isEmpty) (Text.Edit.inserts(0, text), false)
   353           else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
   354 
   355         if (text_edits.isEmpty && node_required == old_required) Nil
   356         else make_edits(text_edits)
   357       }
   358 
   359       def purge_edits: List[Document.Edit_Text] =
   360         make_edits(Text.Edit.removes(0, text))
   361 
   362       def required(required: Boolean): Theory =
   363         if (required == node_required) this
   364         else new Theory(node_name, node_header, text, required)
   365     }
   366 
   367     sealed case class State(
   368       required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty,
   369       theories: Map[Document.Node.Name, Theory] = Map.empty)
   370     {
   371       lazy val theory_graph: Graph[Document.Node.Name, Unit] =
   372       {
   373         val entries =
   374           for ((name, theory) <- theories.toList)
   375           yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   376         Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   377       }
   378 
   379       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
   380 
   381       def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
   382         copy(required = (required /: names)(_.insert(_, id)))
   383 
   384       def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
   385         copy(required = (required /: names)(_.remove(_, id)))
   386 
   387       def update_theories(update: List[(Document.Node.Name, Theory)]): State =
   388         copy(theories =
   389           (theories /: update)({ case (thys, (name, thy)) =>
   390             thys.get(name) match {
   391               case Some(thy1) if thy1 == thy => thys
   392               case _ => thys + (name -> thy)
   393             }
   394           }))
   395 
   396       def remove_theories(remove: List[Document.Node.Name]): State =
   397       {
   398         require(remove.forall(name => !is_required(name)))
   399         copy(theories = theories -- remove)
   400       }
   401 
   402       def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
   403         : State =
   404       {
   405         val st1 = remove_required(id, dep_theories)
   406         val theory_edits =
   407           for {
   408             node_name <- dep_theories
   409             theory <- st1.theories.get(node_name)
   410           }
   411           yield {
   412             val theory1 = theory.required(st1.is_required(node_name))
   413             val edits = theory1.node_edits(Some(theory))
   414             (edits, (node_name, theory1))
   415           }
   416         session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   417         st1.update_theories(theory_edits.map(_._2))
   418       }
   419 
   420       def purge_theories(session: Session, nodes: List[Document.Node.Name])
   421         : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
   422       {
   423         val all_nodes = theory_graph.topological_order
   424         val purge = nodes.filterNot(is_required(_)).toSet
   425 
   426         val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
   427         val (retained, purged) = all_nodes.partition(retain)
   428 
   429         val purge_edits = purged.flatMap(name => theories(name).purge_edits)
   430         session.update(Document.Blobs.empty, purge_edits)
   431 
   432         ((purged, retained), remove_theories(purged))
   433       }
   434 
   435       def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
   436       {
   437         @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
   438           : Set[Document.Node.Name] =
   439         {
   440           val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
   441           if (add.isEmpty) front
   442           else {
   443             val pre_add = add.map(theory_graph.imm_preds)
   444             val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   445             frontier(base1, front ++ add)
   446           }
   447         }
   448         frontier(theory_graph.maximals.filter(clean), Set.empty)
   449       }
   450     }
   451   }
   452 
   453   class Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   454     extends isabelle.Resources(session_base, log = log)
   455   {
   456     resources =>
   457 
   458     private val state = Synchronized(Resources.State())
   459 
   460     def load_theories(
   461       session: Session,
   462       id: UUID.T,
   463       dep_theories: List[Document.Node.Name],
   464       progress: Progress)
   465     {
   466       val loaded_theories =
   467         for (node_name <- dep_theories)
   468         yield {
   469           val path = node_name.path
   470           if (!node_name.is_theory) error("Not a theory file: " + path)
   471 
   472           progress.expose_interrupt()
   473           val text = File.read(path)
   474           val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
   475           new Resources.Theory(node_name, node_header, text, true)
   476         }
   477 
   478       val loaded = loaded_theories.length
   479       if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
   480 
   481       state.change(st =>
   482         {
   483           val st1 = st.insert_required(id, dep_theories)
   484           val theory_edits =
   485             for (theory <- loaded_theories)
   486             yield {
   487               val node_name = theory.node_name
   488               val theory1 = theory.required(st1.is_required(node_name))
   489               val edits = theory1.node_edits(st1.theories.get(node_name))
   490               (edits, (node_name, theory1))
   491             }
   492           session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   493           st1.update_theories(theory_edits.map(_._2))
   494         })
   495     }
   496 
   497     def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
   498     {
   499       state.change(_.unload_theories(session, id, dep_theories))
   500     }
   501 
   502     def clean_theories(session: Session, id: UUID.T, clean: Set[Document.Node.Name])
   503     {
   504       state.change(st =>
   505         {
   506           val frontier = st.frontier_theories(clean).toList
   507           if (frontier.isEmpty) st
   508           else {
   509             val st1 = st.unload_theories(session, id, frontier)
   510             val (_, st2) = st1.purge_theories(session, frontier)
   511             st2
   512           }
   513         })
   514     }
   515 
   516     def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
   517       : (List[Document.Node.Name], List[Document.Node.Name]) =
   518     {
   519       state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
   520     }
   521   }
   522 }