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