diff --git a/src/Pure/General/http.scala b/src/Pure/General/http.scala --- a/src/Pure/General/http.scala +++ b/src/Pure/General/http.scala @@ -1,304 +1,304 @@ /* Title: Pure/General/http.scala Author: Makarius HTTP client and server support. */ package isabelle import java.io.{File => JFile} import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection} import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} object HTTP { /** content **/ val mime_type_bytes: String = "application/octet-stream" val mime_type_text: String = "text/plain; charset=utf-8" val mime_type_html: String = "text/html; charset=utf-8" val default_mime_type: String = mime_type_bytes val default_encoding: String = UTF8.charset_name sealed case class Content( bytes: Bytes, file_name: String = "", mime_type: String = default_mime_type, encoding: String = default_encoding, elapsed_time: Time = Time.zero) { def text: String = new String(bytes.array, encoding) } def read_content(file: JFile): Content = { val bytes = Bytes.read(file) val file_name = file.getName val mime_type = Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type) Content(bytes, file_name = file_name, mime_type = mime_type) } def read_content(path: Path): Content = read_content(path.file) /** client **/ val NEWLINE: String = "\r\n" object Client { val default_timeout: Time = Time.seconds(180) def open_connection(url: URL, timeout: Time = default_timeout, user_agent: String = ""): HttpURLConnection = { url.openConnection match { case connection: HttpURLConnection => if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) { val ms = timeout.ms.toInt connection.setConnectTimeout(ms) connection.setReadTimeout(ms) } proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s)) connection case _ => error("Bad URL (not HTTP): " + quote(url.toString)) } } def get_content(connection: HttpURLConnection): Content = { val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r val start = Time.now() using(connection.getInputStream)(stream => { val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) val stop = Time.now() val file_name = Url.file_name(connection.getURL) val mime_type = Option(connection.getContentType).getOrElse(default_mime_type) val encoding = (connection.getContentEncoding, mime_type) match { case (enc, _) if enc != null => enc case (_, Charset(enc)) => enc case _ => default_encoding } Content(bytes, file_name = file_name, mime_type = mime_type, encoding = encoding, elapsed_time = stop - start) }) } def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content = get_content(open_connection(url, timeout = timeout, user_agent = user_agent)) def post(url: URL, parameters: List[(String, Any)], timeout: Time = default_timeout, user_agent: String = ""): Content = { val connection = open_connection(url, timeout = timeout, user_agent = user_agent) connection.setRequestMethod("POST") connection.setDoOutput(true) val boundary = UUID.random_string() connection.setRequestProperty( "Content-Type", "multipart/form-data; boundary=" + quote(boundary)) using(connection.getOutputStream)(out => { def output(s: String): Unit = out.write(UTF8.bytes(s)) def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) def output_boundary(end: Boolean = false): Unit = output("--" + boundary + (if (end) "--" else "") + NEWLINE) def output_name(name: String): Unit = output("Content-Disposition: form-data; name=" + quote(name)) def output_value(value: Any): Unit = { output_newline(2) output(value.toString) } def output_content(content: Content): Unit = { proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) output_newline() proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) output_newline(2) content.bytes.write_stream(out) } output_newline(2) for { (name, value) <- parameters } { output_boundary() output_name(name) value match { case content: Content => output_content(content) case file: JFile => output_content(read_content(file)) case path: Path => output_content(read_content(path)) case _ => output_value(value) } output_newline() } output_boundary(end = true) out.flush() }) get_content(connection) } } /** server **/ /* response */ object Response { def apply( bytes: Bytes = Bytes.empty, content_type: String = mime_type_bytes): Response = new Response(bytes, content_type) val empty: Response = apply() def text(s: String): Response = apply(Bytes(s), mime_type_text) def html(s: String): Response = apply(Bytes(s), mime_type_html) } class Response private[HTTP](val bytes: Bytes, val content_type: String) { override def toString: String = bytes.toString } /* exchange */ class Exchange private[HTTP](val http_exchange: HttpExchange) { def request_method: String = http_exchange.getRequestMethod def request_uri: URI = http_exchange.getRequestURI def read_request(): Bytes = using(http_exchange.getRequestBody)(Bytes.read_stream(_)) def write_response(code: Int, response: Response): Unit = { http_exchange.getResponseHeaders.set("Content-Type", response.content_type) http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) using(http_exchange.getResponseBody)(response.bytes.write_stream) } } /* handler for request method */ sealed case class Arg(method: String, uri: URI, request: Bytes) { def decode_properties: Properties.T = - space_explode('&', request.text).map(s => - space_explode('=', s) match { - case List(a, b) => Url.decode(a) -> Url.decode(b) - case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s)) + space_explode('&', request.text).map( + { + case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b) + case s => error("Malformed key-value pair in HTTP/POST: " + quote(s)) }) } object Handler { def apply(root: String, body: Exchange => Unit): Handler = new Handler(root, (x: HttpExchange) => body(new Exchange(x))) def method(name: String, root: String, body: Arg => Option[Response]): Handler = apply(root, http => { val request = http.read_request() if (http.request_method == name) { val arg = Arg(name, http.request_uri, request) Exn.capture(body(arg)) match { case Exn.Res(Some(response)) => http.write_response(200, response) case Exn.Res(None) => http.write_response(404, Response.empty) case Exn.Exn(ERROR(msg)) => http.write_response(500, Response.text(Output.error_message_text(msg))) case Exn.Exn(exn) => throw exn } } else http.write_response(400, Response.empty) }) def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body) def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body) } class Handler private(val root: String, val handler: HttpHandler) { override def toString: String = root } /* server */ class Server private[HTTP](val http_server: HttpServer) { def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler) def -= (handler: Handler): Unit = http_server.removeContext(handler.root) def start(): Unit = http_server.start() def stop(): Unit = http_server.stop(0) def address: InetSocketAddress = http_server.getAddress def url: String = "http://" + address.getHostName + ":" + address.getPort override def toString: String = url } def server(handlers: List[Handler] = isabelle_resources): Server = { val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) http_server.setExecutor(null) val server = new Server(http_server) for (handler <- handlers) server += handler server } /** Isabelle resources **/ lazy val isabelle_resources: List[Handler] = List(welcome(), fonts()) /* welcome */ def welcome(root: String = "/"): Handler = Handler.get(root, arg => if (arg.uri.toString == root) { Some(Response.text("Welcome to " + Isabelle_System.identification())) } else None) /* fonts */ private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(hidden = true) def fonts(root: String = "/fonts"): Handler = Handler.get(root, arg => { val uri_name = arg.uri.toString if (uri_name == root) { Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name)))) } else { html_fonts.collectFirst( { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) }) } }) } diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala +++ b/src/Pure/ML/ml_statistics.scala @@ -1,324 +1,319 @@ /* Title: Pure/ML/ml_statistics.scala Author: Makarius ML runtime statistics. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.{SortedSet, SortedMap} import scala.swing.{Frame, Component} import org.jfree.data.xy.{XYSeries, XYSeriesCollection} import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} import org.jfree.chart.plot.PlotOrientation object ML_Statistics { /* properties */ val Now = new Properties.Double("now") def now(props: Properties.T): Double = Now.unapply(props).get /* memory status */ val Heap_Size = new Properties.Long("size_heap") val Heap_Free = new Properties.Long("size_heap_free_last_GC") val GC_Percent = new Properties.Int("GC_percent") sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int) { def heap_used: Long = (heap_size - heap_free) max 0 def heap_used_fraction: Double = if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size def gc_progress: Option[Double] = if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None } def memory_status(props: Properties.T): Memory_Status = { val heap_size = Heap_Size.get(props) val heap_free = Heap_Free.get(props) val gc_percent = GC_Percent.get(props) Memory_Status(heap_size, heap_free, gc_percent) } /* monitor process */ def monitor(pid: Long, stats_dir: String = "", delay: Time = Time.seconds(0.5), consume: Properties.T => Unit = Console.println): Unit = { def progress_stdout(line: String): Unit = { - val props = - Library.space_explode(',', line).flatMap((entry: String) => - Library.space_explode('=', entry) match { - case List(a, b) => Some((a, b)) - case _ => None - }) + val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply) if (props.nonEmpty) consume(props) } val env_prefix = if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n" Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + ML_Syntax.print_double(delay.seconds)), cwd = Path.ISABELLE_HOME.file) .result(progress_stdout = progress_stdout, strict = false).check } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var monitoring: Future[Unit] = Future.value(()) override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { session = null monitoring.cancel() } private def consume(props: Properties.T): Unit = synchronized { if (session != null) { val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics())) session.runtime_statistics.post(Session.Runtime_Statistics(props1)) } } private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.ML_Statistics(pid, stats_dir) => monitoring = Future.thread("ML_statistics") { monitor(pid, stats_dir = stats_dir, consume = consume) } true case _ => false } } override val functions = List(Markup.ML_Statistics.name -> ml_statistics) } /* memory fields (mega bytes) */ def mem_print(x: Long): Option[String] = if (x == 0L) None else Some(x.toString + " M") def mem_scale(x: Long): Long = x / 1024 / 1024 def mem_field_scale(name: String, x: Double): Double = if (heap_fields._2.contains(name) || program_fields._2.contains(name)) mem_scale(x.toLong).toDouble else x val CODE_SIZE = "size_code" val STACK_SIZE = "size_stacks" val HEAP_SIZE = "size_heap" /* standard fields */ type Fields = (String, List[String]) val tasks_fields: Fields = ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent", "tasks_total")) val workers_fields: Fields = ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) val GC_fields: Fields = ("GCs", List("partial_GCs", "full_GCs", "share_passes")) val heap_fields: Fields = ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", "size_heap_free_last_full_GC", "size_heap_free_last_GC")) val program_fields: Fields = ("Program", List("size_code", "size_stacks")) val threads_fields: Fields = ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) val time_fields: Fields = ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC")) val speed_fields: Fields = ("Speed", List("speed_CPU", "speed_GC")) private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") val java_heap_fields: Fields = ("Java heap", List("java_heap_size", "java_heap_used")) val java_thread_fields: Fields = ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) val main_fields: List[Fields] = List(heap_fields, tasks_fields, workers_fields) val other_fields: List[Fields] = List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, java_heap_fields, java_thread_fields) val all_fields: List[Fields] = main_fields ::: other_fields /* content interpretation */ final case class Entry(time: Double, data: Map[String, Double]) { def get(field: String): Double = data.getOrElse(field, 0.0) } val empty: ML_Statistics = apply(Nil) def apply(ml_statistics0: List[Properties.T], heading: String = "", domain: String => Boolean = (key: String) => true): ML_Statistics = { require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field") val ml_statistics = ml_statistics0.sortBy(now) val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start val fields = SortedSet.empty[String] ++ (for { props <- ml_statistics.iterator (x, _) <- props.iterator if x != Now.name && domain(x) } yield x) val content = { var last_edge = Map.empty[String, (Double, Double, Double)] val result = new mutable.ListBuffer[ML_Statistics.Entry] for (props <- ml_statistics) { val time = now(props) - time_start // rising edges -- relative speed val speeds = (for { (key, value) <- props.iterator key1 <- time_speed.get(key) if domain(key1) } yield { val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0)) val x1 = time val y1 = java.lang.Double.parseDouble(value) val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) if (y1 > y0) { last_edge += (key -> (x1, y1, s1)) (key1, s1.toString) } else (key1, s0.toString) }).toList val data = SortedMap.empty[String, Double] ++ (for { (x, y) <- props.iterator ++ speeds.iterator if x != Now.name && domain(x) z = java.lang.Double.parseDouble(y) if z != 0.0 } yield { (x.intern, mem_field_scale(x, z)) }) result += ML_Statistics.Entry(time, data) } result.toList } new ML_Statistics(heading, fields, content, time_start, duration) } } final class ML_Statistics private( val heading: String, val fields: Set[String], val content: List[ML_Statistics.Entry], val time_start: Double, val duration: Double) { /* content */ def maximum(field: String): Double = content.foldLeft(0.0) { case (m, e) => m max e.get(field) } def average(field: String): Double = { @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = list match { case Nil => acc case e :: es => val t = e.time sum(t, es, (t - t0) * e.get(field) + acc) } content match { case Nil => 0.0 case List(e) => e.get(field) case e :: es => sum(e.time, es, 0.0) / duration } } /* charts */ def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit = { data.removeAllSeries for (field <- selected_fields) { val series = new XYSeries(field) content.foreach(entry => series.add(entry.time, entry.get(field))) data.addSeries(series) } } def chart(title: String, selected_fields: List[String]): JFreeChart = { val data = new XYSeriesCollection update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } def chart(fields: ML_Statistics.Fields): JFreeChart = chart(fields._1, fields._2) def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = fields.map(chart).foreach(c => GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = heading contents = Component.wrap(new ChartPanel(c)) visible = true } }) } diff --git a/src/Pure/System/isabelle_platform.scala b/src/Pure/System/isabelle_platform.scala --- a/src/Pure/System/isabelle_platform.scala +++ b/src/Pure/System/isabelle_platform.scala @@ -1,67 +1,64 @@ /* Title: Pure/System/isabelle_platform.scala Author: Makarius General hardware and operating system type for Isabelle system tools. */ package isabelle object Isabelle_Platform { val settings: List[String] = List( "ISABELLE_PLATFORM_FAMILY", "ISABELLE_PLATFORM64", "ISABELLE_WINDOWS_PLATFORM32", "ISABELLE_WINDOWS_PLATFORM64", "ISABELLE_APPLE_PLATFORM64") def apply(ssh: Option[SSH.Session] = None): Isabelle_Platform = { ssh match { case None => new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a)))) case Some(ssh) => val script = File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" + settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n") val result = ssh.execute("bash -c " + Bash.string(script)).check new Isabelle_Platform( result.out_lines.map(line => - space_explode('=', line) match { - case List(a, b) => (a, b) - case _ => error("Bad output: " + quote(result.out)) - })) + Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out)))) } } lazy val self: Isabelle_Platform = apply() } class Isabelle_Platform private(val settings: List[(String, String)]) { private def get(name: String): String = settings.collectFirst({ case (a, b) if a == name => b }). getOrElse(error("Bad platform settings variable: " + quote(name))) val ISABELLE_PLATFORM_FAMILY: String = get("ISABELLE_PLATFORM_FAMILY") val ISABELLE_PLATFORM64: String = get("ISABELLE_PLATFORM64") val ISABELLE_WINDOWS_PLATFORM64: String = get("ISABELLE_WINDOWS_PLATFORM64") val ISABELLE_APPLE_PLATFORM64: String = get("ISABELLE_APPLE_PLATFORM64") def is_arm: Boolean = ISABELLE_PLATFORM64.startsWith("arm64-") || ISABELLE_APPLE_PLATFORM64.startsWith("arm64-") def is_linux: Boolean = ISABELLE_PLATFORM_FAMILY == "linux" def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos" def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows" def arch_64: String = if (is_arm) "arm64" else "x86_64" def arch_64_32: String = if (is_arm) "arm64_32" else "x86_64_32" def os_name: String = if (is_macos) "darwin" else ISABELLE_PLATFORM_FAMILY override def toString: String = ISABELLE_PLATFORM_FAMILY }