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