diff --git a/etc/components b/etc/components --- a/etc/components +++ b/etc/components @@ -1,11 +1,10 @@ #built-in components src/Tools/jEdit src/Tools/Graphview src/Tools/VSCode src/HOL/Mirabelle src/HOL/Mutabelle src/HOL/Library/Sum_of_Squares src/HOL/SPARK src/HOL/Tools -src/HOL/Tools/ATP src/HOL/TPTP diff --git a/src/Doc/System/Scala.thy b/src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy +++ b/src/Doc/System/Scala.thy @@ -1,339 +1,337 @@ (*:maxLineLen=78:*) theory Scala imports Base begin chapter \Isabelle/Scala systems programming \label{sec:scala}\ text \ Isabelle/ML and Isabelle/Scala are the two main implementation languages of the Isabelle environment: \<^item> Isabelle/ML is for \<^emph>\mathematics\, to develop tools within the context of symbolic logic, e.g.\ for constructing proofs or defining domain-specific formal languages. See the \<^emph>\Isabelle/Isar implementation manual\ @{cite "isabelle-implementation"} for more details. \<^item> Isabelle/Scala is for \<^emph>\physics\, to connect with the world of systems and services, including editors and IDE frameworks. There are various ways to access Isabelle/Scala modules and operations: \<^item> Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate Java process. \<^item> Isabelle/ML antiquotations access Isabelle/Scala functions (\secref{sec:scala-functions}) via the PIDE protocol: execution happens within the running Java process underlying Isabelle/Scala. \<^item> The \<^verbatim>\Console/Scala\ plugin of Isabelle/jEdit @{cite "isabelle-jedit"} operates on the running Java application, using the Scala read-eval-print-loop (REPL). The main Isabelle/Scala functionality is provided by \<^verbatim>\Pure.jar\, but further add-ons are bundled with Isabelle, e.g.\ to access SQLite or PostgreSQL using JDBC (Java Database Connectivity). Other components may augment the system environment by providing a suitable \<^path>\etc/settings\ shell script in the component directory. Some shell functions are available to help with that: \<^item> Function \<^bash_function>\classpath\ adds \<^verbatim>\jar\ files in Isabelle path notation (POSIX). On Windows, this is converted to native path names before invoking @{tool java} or @{tool scala} (\secref{sec:scala-tools}). \<^item> Function \<^bash_function>\isabelle_scala_service\ registers global service providers as subclasses of \<^scala_type>\isabelle.Isabelle_System.Service\, using the raw Java name according to @{scala_method (in java.lang.Object) getClass} (it should be enclosed in single quotes to avoid special characters like \<^verbatim>\$\ to be interpreted by the shell). Particular Isabelle/Scala services require particular subclasses: instances are filtered according to their dynamic type. For example, class \<^scala_type>\isabelle.Isabelle_Scala_Tools\ collects Scala command-line tools, and class \<^scala_type>\isabelle.Scala.Functions\ collects Scala functions (\secref{sec:scala-functions}). \ section \Command-line tools \label{sec:scala-tools}\ subsection \Java Runtime Environment \label{sec:tool-java}\ text \ The @{tool_def java} tool is a direct wrapper for the Java Runtime Environment, within the regular Isabelle settings environment (\secref{sec:settings}) and Isabelle classpath. The command line arguments are that of the bundled Java distribution: see option \<^verbatim>\-help\ in particular. The \<^verbatim>\java\ executable is taken from @{setting ISABELLE_JDK_HOME}, according to the standard directory layout for regular distributions of OpenJDK. The shell function \<^bash_function>\isabelle_jdk\ allows shell scripts to invoke other Java tools robustly (e.g.\ \<^verbatim>\isabelle_jdk jar\), without depending on accidental operating system installations. \ subsection \Scala toplevel \label{sec:tool-scala}\ text \ The @{tool_def scala} tool is a direct wrapper for the Scala toplevel, similar to @{tool java} above. The command line arguments are that of the bundled Scala distribution: see option \<^verbatim>\-help\ in particular. This allows to interact with Isabelle/Scala interactively. \ subsubsection \Example\ text \ Explore the Isabelle system environment in Scala: @{verbatim [display, indent = 2] \$ isabelle scala\} @{scala [display, indent = 2] \import isabelle._ val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") val options = Options.init() options.bool("browser_info") options.string("document")\} \ subsection \Scala compiler \label{sec:tool-scalac}\ text \ The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see also @{tool scala} above. The command line arguments are that of the bundled Scala distribution. This allows to compile further Scala modules, depending on existing Isabelle/Scala functionality. The resulting \<^verbatim>\class\ or \<^verbatim>\jar\ files can be added to the Java classpath using the shell function \<^bash_function>\classpath\. Thus add-on components can register themselves in a modular manner, see also \secref{sec:components}. Note that Isabelle/jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding plugin components. This needs special attention, since it overrides the standard Java class loader. \ subsection \Scala script wrapper\ text \ The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run Isabelle/Scala source files stand-alone programs, by using a suitable ``hash-bang'' line and executable file permissions. For example: @{verbatim [display, indent = 2] \#!/usr/bin/env isabelle_scala_script\} @{scala [display, indent = 2] \val options = isabelle.Options.init() Console.println("browser_info = " + options.bool("browser_info")) Console.println("document = " + options.string("document"))\} This assumes that the executable may be found via the @{setting PATH} from the process environment: this is the case when Isabelle settings are active, e.g.\ in the context of the main Isabelle tool wrapper \secref{sec:isabelle-tool}. Alternatively, the full \<^file>\$ISABELLE_HOME/bin/isabelle_scala_script\ may be specified in expanded form. \ subsection \Project setup for common Scala IDEs\ text \ The @{tool_def scala_project} tool creates a project configuration for Isabelle/Scala/jEdit: @{verbatim [display] \Usage: isabelle scala_project [OPTIONS] PROJECT_DIR Options are: -L make symlinks to original scala files Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs such as IntelliJ IDEA.\} The generated configuration is for Gradle\<^footnote>\\<^url>\https://gradle.org\\, but the main purpose is to import it into common Scala IDEs, such as IntelliJ IDEA\<^footnote>\\<^url>\https://www.jetbrains.com/idea\\. This allows to explore the sources with static analysis and other hints in real-time. The specified project directory needs to be fresh. The generated files refer to physical file-system locations, using the path notation of the underlying OS platform. Thus the project needs to be recreated whenever the Isabelle installation is changed or moved. \<^medskip> By default, Scala sources are \<^emph>\copied\ from the Isabelle distribution and editing them within the IDE has no permanent effect. Option \<^verbatim>\-L\ produces \<^emph>\symlinks\ to the original files: this allows to develop Isabelle/Scala/jEdit within an external Scala IDE. Note that building the result always requires \<^verbatim>\isabelle jedit -b\ on the command-line. \ section \Registered Isabelle/Scala functions \label{sec:scala-functions}\ subsection \Defining functions in Isabelle/Scala\ text \ A Scala functions of type \<^scala_type>\String => String\ may be wrapped as \<^scala_type>\isabelle.Scala.Fun\ and collected via an instance of the class \<^scala_type>\isabelle.Scala.Functions\. A system component can then register that class via \<^bash_function>\isabelle_scala_service\ in \<^path>\etc/settings\ (\secref{sec:components}). An example is the predefined collection of \<^scala_type>\isabelle.Scala.Functions\ in Isabelle/\<^verbatim>\Pure.jar\ with the following line in \<^file>\$ISABELLE_HOME/etc/settings\: @{verbatim [display, indent = 2] \isabelle_scala_service 'isabelle.Functions'\} The overall list of registered functions is accessible in Isabelle/Scala as \<^scala_object>\isabelle.Scala.functions\. \ subsection \Invoking functions in Isabelle/ML\ text \ Isabelle/PIDE provides a protocol to invoke registered Scala functions in ML: this works both within the Prover IDE and in batch builds. The subsequent ML antiquotations refer to Scala functions in a formally-checked manner. \begin{matharray}{rcl} @{ML_antiquotation_def "scala_function"} & : & \ML_antiquotation\ \\ @{ML_antiquotation_def "scala"} & : & \ML_antiquotation\ \\ - @{ML_antiquotation_def "scala_thread"} & : & \ML_antiquotation\ \\ \end{matharray} \<^rail>\ (@{ML_antiquotation scala_function} | - @{ML_antiquotation scala} | - @{ML_antiquotation scala_thread}) @{syntax embedded} + @{ML_antiquotation scala}) @{syntax embedded} \ \<^descr> \@{scala_function name}\ inlines the checked function name as ML string literal. \<^descr> \@{scala name}\ and \@{scala_thread name}\ invoke the checked function via the PIDE protocol. In Isabelle/ML this appears as a function of type \<^ML_type>\string -> string\, which is subject to interrupts within the ML runtime environment as usual. A \<^scala>\null\ result in Scala raises an exception \<^ML>\Scala.Null\ in ML. The execution of \@{scala}\ works via a Scala future on a bounded thread farm, while \@{scala_thread}\ always forks a separate Java thread. The standard approach of representing datatypes via strings works via XML in YXML transfer syntax. See Isabelle/ML operations and modules @{ML YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode}, @{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols may have to be recoded via Scala operations \<^scala_method>\isabelle.Symbol.decode\ and \<^scala_method>\isabelle.Symbol.encode\. \ subsubsection \Examples\ text \ Invoke the predefined Scala function \<^scala_function>\echo\: \ ML \ val s = "test"; val s' = \<^scala>\echo\ s; \<^assert> (s = s') \ text \ Let the Scala compiler process some toplevel declarations, producing a list of errors: \ ML \ val source = "class A(a: Int, b: Boolean)" val errors = \<^scala>\scala_toplevel\ source |> YXML.parse_body |> let open XML.Decode in list string end; \<^assert> (null errors)\ text \ The above is merely for demonstration. See \<^ML>\Scala_Compiler.toplevel\ for a more convenient version with builtin decoding and treatment of errors. \ section \Documenting Isabelle/Scala entities\ text \ The subsequent document antiquotations help to document Isabelle/Scala entities, with formal checking of names against the Isabelle classpath. \begin{matharray}{rcl} @{antiquotation_def "scala"} & : & \antiquotation\ \\ @{antiquotation_def "scala_object"} & : & \antiquotation\ \\ @{antiquotation_def "scala_type"} & : & \antiquotation\ \\ @{antiquotation_def "scala_method"} & : & \antiquotation\ \\ \end{matharray} \<^rail>\ (@@{antiquotation scala} | @@{antiquotation scala_object}) @{syntax embedded} ; @@{antiquotation scala_type} @{syntax embedded} types ; @@{antiquotation scala_method} class @{syntax embedded} types args ; class: ('(' @'in' @{syntax name} types ')')? ; types: ('[' (@{syntax name} ',' +) ']')? ; args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')? \ \<^descr> \@{scala s}\ is similar to \@{verbatim s}\, but the given source text is checked by the Scala compiler as toplevel declaration (without evaluation). This allows to write Isabelle/Scala examples that are statically checked. \<^descr> \@{scala_object x}\ checks the given Scala object name (simple value or ground module) and prints the result verbatim. \<^descr> \@{scala_type T[A]}\ checks the given Scala type name (with optional type parameters) and prints the result verbatim. \<^descr> \@{scala_method (in c[A]) m[B](n)}\ checks the given Scala method \m\ in the context of class \c\. The method argument slots are either specified by a number \n\ or by a list of (optional) argument types; this may refer to type variables specified for the class or method: \A\ or \B\ above. Everything except for the method name \m\ is optional. The absence of the class context means that this is a static method. The absence of arguments with types means that the method can be determined uniquely as \<^verbatim>\(\\m\\<^verbatim>\ _)\ in Scala (no overloading). \ subsubsection \Examples\ text \ Miscellaneous Isabelle/Scala entities: \<^item> object: \<^scala_object>\isabelle.Isabelle_Process\ \<^item> type without parameter: @{scala_type isabelle.Console_Progress} \<^item> type with parameter: @{scala_type List[A]} \<^item> static method: \<^scala_method>\isabelle.Isabelle_System.bash\ \<^item> class and method with type parameters: @{scala_method (in List[A]) map[B]("A => B")} \<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)} \ end diff --git a/src/HOL/Sledgehammer.thy b/src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy +++ b/src/HOL/Sledgehammer.thy @@ -1,36 +1,37 @@ (* Title: HOL/Sledgehammer.thy Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen *) section \Sledgehammer: Isabelle--ATP Linkup\ theory Sledgehammer imports Presburger SMT keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl begin +ML_file \Tools/ATP/system_on_tptp.ML\ ML_file \Tools/Sledgehammer/async_manager_legacy.ML\ ML_file \Tools/Sledgehammer/sledgehammer_util.ML\ ML_file \Tools/Sledgehammer/sledgehammer_fact.ML\ ML_file \Tools/Sledgehammer/sledgehammer_proof_methods.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_annotate.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_proof.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_preplay.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_compress.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_isar.ML\ ML_file \Tools/Sledgehammer/sledgehammer_atp_systems.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_atp.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_smt.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mepo.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ end diff --git a/src/HOL/Tools/ATP/etc/settings b/src/HOL/Tools/ATP/etc/settings deleted file mode 100644 --- a/src/HOL/Tools/ATP/etc/settings +++ /dev/null @@ -1,3 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -ISABELLE_ATP="$COMPONENT" diff --git a/src/HOL/Tools/ATP/system_on_tptp.ML b/src/HOL/Tools/ATP/system_on_tptp.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/ATP/system_on_tptp.ML @@ -0,0 +1,24 @@ +(* Title: HOL/Tools/ATP/system_on_tptp.ML + Author: Makarius + +Support for remote ATPs via SystemOnTPTP. +*) + +signature SYSTEM_ON_TPTP = +sig + val get_url: unit -> string + val list_systems: unit -> {url: string, systems: string list} +end + +structure SystemOnTPTP: SYSTEM_ON_TPTP = +struct + +fun get_url () = Options.default_string \<^system_option>\SystemOnTPTP\ + +fun list_systems () = + let + val url = get_url () + val systems = split_lines (\<^scala>\SystemOnTPTP.list_systems\ url) + in {url = url, systems = systems} end + +end diff --git a/src/HOL/Tools/ATP/system_on_tptp.scala b/src/HOL/Tools/ATP/system_on_tptp.scala new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/ATP/system_on_tptp.scala @@ -0,0 +1,46 @@ +/* Title: HOL/Tools/ATP/system_on_tptp.scala + Author: Makarius + +Support for remote ATPs via SystemOnTPTP. +*/ + +package isabelle.atp + +import isabelle._ + +import java.net.URL + + +object SystemOnTPTP +{ + /* requests */ + + def get_url(options: Options): URL = Url(options.string("SystemOnTPTP")) + + def post_request( + url: URL, + parameters: List[(String, Any)], + timeout: Time = HTTP.Client.default_timeout): HTTP.Content = + { + val parameters0 = + List("NoHTML" -> 1, "QuietFlag" -> "-q01") + .filterNot(p0 => parameters.exists(p => p0._1 == p._1)) + try { + HTTP.Client.post(url, parameters0 ::: parameters, + timeout = timeout, user_agent = "Sledgehammer") + } + catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) } + } + + + /* list systems */ + + def list_systems(url: URL): List[String] = + post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines + + object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true) + { + val here = Scala_Project.here + def apply(url: String): String = cat_lines(list_systems(Url(url))) + } +} diff --git a/src/HOL/Tools/Nitpick/kodkod.ML b/src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML +++ b/src/HOL/Tools/Nitpick/kodkod.ML @@ -1,1095 +1,1095 @@ (* Title: HOL/Tools/Nitpick/kodkod.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2008-2014 ML interface for Kodkod. *) signature KODKOD = sig type n_ary_index = int * int type setting = string * string datatype tuple = Tuple of int list | TupleIndex of n_ary_index | TupleReg of n_ary_index datatype tuple_set = TupleUnion of tuple_set * tuple_set | TupleDifference of tuple_set * tuple_set | TupleIntersect of tuple_set * tuple_set | TupleProduct of tuple_set * tuple_set | TupleProject of tuple_set * int | TupleSet of tuple list | TupleRange of tuple * tuple | TupleArea of tuple * tuple | TupleAtomSeq of int * int | TupleSetReg of n_ary_index datatype tuple_assign = AssignTuple of n_ary_index * tuple | AssignTupleSet of n_ary_index * tuple_set type bound = (n_ary_index * string) list * tuple_set list type int_bound = int option * tuple_set list datatype formula = All of decl list * formula | Exist of decl list * formula | FormulaLet of expr_assign list * formula | FormulaIf of formula * formula * formula | Or of formula * formula | Iff of formula * formula | Implies of formula * formula | And of formula * formula | Not of formula | Acyclic of n_ary_index | Function of n_ary_index * rel_expr * rel_expr | Functional of n_ary_index * rel_expr * rel_expr | TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr | Subset of rel_expr * rel_expr | RelEq of rel_expr * rel_expr | IntEq of int_expr * int_expr | LT of int_expr * int_expr | LE of int_expr * int_expr | No of rel_expr | Lone of rel_expr | One of rel_expr | Some of rel_expr | False | True | FormulaReg of int and rel_expr = RelLet of expr_assign list * rel_expr | RelIf of formula * rel_expr * rel_expr | Union of rel_expr * rel_expr | Difference of rel_expr * rel_expr | Override of rel_expr * rel_expr | Intersect of rel_expr * rel_expr | Product of rel_expr * rel_expr | IfNo of rel_expr * rel_expr | Project of rel_expr * int_expr list | Join of rel_expr * rel_expr | Closure of rel_expr | ReflexiveClosure of rel_expr | Transpose of rel_expr | Comprehension of decl list * formula | Bits of int_expr | Int of int_expr | Iden | Ints | None | Univ | Atom of int | AtomSeq of int * int | Rel of n_ary_index | Var of n_ary_index | RelReg of n_ary_index and int_expr = Sum of decl list * int_expr | IntLet of expr_assign list * int_expr | IntIf of formula * int_expr * int_expr | SHL of int_expr * int_expr | SHA of int_expr * int_expr | SHR of int_expr * int_expr | Add of int_expr * int_expr | Sub of int_expr * int_expr | Mult of int_expr * int_expr | Div of int_expr * int_expr | Mod of int_expr * int_expr | Cardinality of rel_expr | SetSum of rel_expr | BitOr of int_expr * int_expr | BitXor of int_expr * int_expr | BitAnd of int_expr * int_expr | BitNot of int_expr | Neg of int_expr | Absolute of int_expr | Signum of int_expr | Num of int | IntReg of int and decl = DeclNo of n_ary_index * rel_expr | DeclLone of n_ary_index * rel_expr | DeclOne of n_ary_index * rel_expr | DeclSome of n_ary_index * rel_expr | DeclSet of n_ary_index * rel_expr and expr_assign = AssignFormulaReg of int * formula | AssignRelReg of n_ary_index * rel_expr | AssignIntReg of int * int_expr type 'a fold_expr_funcs = {formula_func: formula -> 'a -> 'a, rel_expr_func: rel_expr -> 'a -> 'a, int_expr_func: int_expr -> 'a -> 'a} val kodkodi_version : unit -> int list val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a type 'a fold_tuple_funcs = {tuple_func: tuple -> 'a -> 'a, tuple_set_func: tuple_set -> 'a -> 'a} val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a val fold_bound : 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a type problem = {comment: string, settings: setting list, univ_card: int, tuple_assigns: tuple_assign list, bounds: bound list, int_bounds: int_bound list, expr_assigns: expr_assign list, formula: formula} type raw_bound = n_ary_index * int list list datatype outcome = Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Error of string * int list exception SYNTAX of string * string val max_arity : int -> int val arity_of_rel_expr : rel_expr -> int val is_problem_trivially_false : problem -> bool val problems_equivalent : problem * problem -> bool val solve_any_problem : bool -> bool -> Time.time -> int -> int -> problem list -> outcome end; structure Kodkod : KODKOD = struct type n_ary_index = int * int type setting = string * string datatype tuple = Tuple of int list | TupleIndex of n_ary_index | TupleReg of n_ary_index datatype tuple_set = TupleUnion of tuple_set * tuple_set | TupleDifference of tuple_set * tuple_set | TupleIntersect of tuple_set * tuple_set | TupleProduct of tuple_set * tuple_set | TupleProject of tuple_set * int | TupleSet of tuple list | TupleRange of tuple * tuple | TupleArea of tuple * tuple | TupleAtomSeq of int * int | TupleSetReg of n_ary_index datatype tuple_assign = AssignTuple of n_ary_index * tuple | AssignTupleSet of n_ary_index * tuple_set type bound = (n_ary_index * string) list * tuple_set list type int_bound = int option * tuple_set list datatype formula = All of decl list * formula | Exist of decl list * formula | FormulaLet of expr_assign list * formula | FormulaIf of formula * formula * formula | Or of formula * formula | Iff of formula * formula | Implies of formula * formula | And of formula * formula | Not of formula | Acyclic of n_ary_index | Function of n_ary_index * rel_expr * rel_expr | Functional of n_ary_index * rel_expr * rel_expr | TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr | Subset of rel_expr * rel_expr | RelEq of rel_expr * rel_expr | IntEq of int_expr * int_expr | LT of int_expr * int_expr | LE of int_expr * int_expr | No of rel_expr | Lone of rel_expr | One of rel_expr | Some of rel_expr | False | True | FormulaReg of int and rel_expr = RelLet of expr_assign list * rel_expr | RelIf of formula * rel_expr * rel_expr | Union of rel_expr * rel_expr | Difference of rel_expr * rel_expr | Override of rel_expr * rel_expr | Intersect of rel_expr * rel_expr | Product of rel_expr * rel_expr | IfNo of rel_expr * rel_expr | Project of rel_expr * int_expr list | Join of rel_expr * rel_expr | Closure of rel_expr | ReflexiveClosure of rel_expr | Transpose of rel_expr | Comprehension of decl list * formula | Bits of int_expr | Int of int_expr | Iden | Ints | None | Univ | Atom of int | AtomSeq of int * int | Rel of n_ary_index | Var of n_ary_index | RelReg of n_ary_index and int_expr = Sum of decl list * int_expr | IntLet of expr_assign list * int_expr | IntIf of formula * int_expr * int_expr | SHL of int_expr * int_expr | SHA of int_expr * int_expr | SHR of int_expr * int_expr | Add of int_expr * int_expr | Sub of int_expr * int_expr | Mult of int_expr * int_expr | Div of int_expr * int_expr | Mod of int_expr * int_expr | Cardinality of rel_expr | SetSum of rel_expr | BitOr of int_expr * int_expr | BitXor of int_expr * int_expr | BitAnd of int_expr * int_expr | BitNot of int_expr | Neg of int_expr | Absolute of int_expr | Signum of int_expr | Num of int | IntReg of int and decl = DeclNo of n_ary_index * rel_expr | DeclLone of n_ary_index * rel_expr | DeclOne of n_ary_index * rel_expr | DeclSome of n_ary_index * rel_expr | DeclSet of n_ary_index * rel_expr and expr_assign = AssignFormulaReg of int * formula | AssignRelReg of n_ary_index * rel_expr | AssignIntReg of int * int_expr type problem = {comment: string, settings: setting list, univ_card: int, tuple_assigns: tuple_assign list, bounds: bound list, int_bounds: int_bound list, expr_assigns: expr_assign list, formula: formula} type raw_bound = n_ary_index * int list list datatype outcome = Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Error of string * int list exception SYNTAX of string * string type 'a fold_expr_funcs = {formula_func: formula -> 'a -> 'a, rel_expr_func: rel_expr -> 'a -> 'a, int_expr_func: int_expr -> 'a -> 'a} fun kodkodi_version () = getenv "KODKODI_VERSION" |> space_explode "." |> map (the_default 0 o Int.fromString) (** Auxiliary functions on Kodkod problems **) fun fold_formula (F : 'a fold_expr_funcs) formula = case formula of All (ds, f) => fold (fold_decl F) ds #> fold_formula F f | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f | FormulaIf (f, f1, f2) => fold_formula F f #> fold_formula F f1 #> fold_formula F f2 | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2 | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2 | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2 | And (f1, f2) => fold_formula F f1 #> fold_formula F f2 | Not f => fold_formula F f | Acyclic x => fold_rel_expr F (Rel x) | Function (x, r1, r2) => fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 | Functional (x, r1, r2) => fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 | TotalOrdering (x, r1, r2, r3) => fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 #> fold_rel_expr F r3 | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | No r => fold_rel_expr F r | Lone r => fold_rel_expr F r | One r => fold_rel_expr F r | Some r => fold_rel_expr F r | False => #formula_func F formula | True => #formula_func F formula | FormulaReg _ => #formula_func F formula and fold_rel_expr F rel_expr = case rel_expr of RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r | RelIf (f, r1, r2) => fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2 | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 | Closure r => fold_rel_expr F r | ReflexiveClosure r => fold_rel_expr F r | Transpose r => fold_rel_expr F r | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f | Bits i => fold_int_expr F i | Int i => fold_int_expr F i | Iden => #rel_expr_func F rel_expr | Ints => #rel_expr_func F rel_expr | None => #rel_expr_func F rel_expr | Univ => #rel_expr_func F rel_expr | Atom _ => #rel_expr_func F rel_expr | AtomSeq _ => #rel_expr_func F rel_expr | Rel _ => #rel_expr_func F rel_expr | Var _ => #rel_expr_func F rel_expr | RelReg _ => #rel_expr_func F rel_expr and fold_int_expr F int_expr = case int_expr of Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i | IntIf (f, i1, i2) => fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2 | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | Cardinality r => fold_rel_expr F r | SetSum r => fold_rel_expr F r | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 | BitNot i => fold_int_expr F i | Neg i => fold_int_expr F i | Absolute i => fold_int_expr F i | Signum i => fold_int_expr F i | Num _ => #int_expr_func F int_expr | IntReg _ => #int_expr_func F int_expr and fold_decl F decl = case decl of DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r and fold_expr_assign F assign = case assign of AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i type 'a fold_tuple_funcs = {tuple_func: tuple -> 'a -> 'a, tuple_set_func: tuple_set -> 'a -> 'a} fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F fun fold_tuple_set F tuple_set = case tuple_set of TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 | TupleProject (ts, _) => fold_tuple_set F ts | TupleSet ts => fold (fold_tuple F) ts | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 | TupleAtomSeq _ => #tuple_set_func F tuple_set | TupleSetReg _ => #tuple_set_func F tuple_set fun fold_tuple_assign F assign = case assign of AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t | AssignTupleSet (x, ts) => fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts fun fold_bound expr_F tuple_F (zs, tss) = fold (fold_rel_expr expr_F) (map (Rel o fst) zs) #> fold (fold_tuple_set tuple_F) tss fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss fun max_arity univ_card = floor (Math.ln 2147483647.0 / Math.ln (Real.fromInt univ_card)) fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2 | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1 | arity_of_rel_expr (Project (_, is)) = length is | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2 | arity_of_rel_expr (Closure _) = 2 | arity_of_rel_expr (ReflexiveClosure _) = 2 | arity_of_rel_expr (Transpose _) = 2 | arity_of_rel_expr (Comprehension (ds, _)) = fold (curry op + o arity_of_decl) ds 0 | arity_of_rel_expr (Bits _) = 1 | arity_of_rel_expr (Int _) = 1 | arity_of_rel_expr Iden = 2 | arity_of_rel_expr Ints = 1 | arity_of_rel_expr None = 1 | arity_of_rel_expr Univ = 1 | arity_of_rel_expr (Atom _) = 1 | arity_of_rel_expr (AtomSeq _) = 1 | arity_of_rel_expr (Rel (n, _)) = n | arity_of_rel_expr (Var (n, _)) = n | arity_of_rel_expr (RelReg (n, _)) = n and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 and arity_of_decl (DeclNo ((n, _), _)) = n | arity_of_decl (DeclLone ((n, _), _)) = n | arity_of_decl (DeclOne ((n, _), _)) = n | arity_of_decl (DeclSome ((n, _), _)) = n | arity_of_decl (DeclSet ((n, _), _)) = n fun is_problem_trivially_false ({formula = False, ...} : problem) = true | is_problem_trivially_false _ = false val chop_solver = take 2 o space_explode "," fun settings_equivalent ([], []) = true | settings_equivalent ((key1, value1) :: settings1, (key2, value2) :: settings2) = key1 = key2 andalso (value1 = value2 orelse key1 = "delay" orelse (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso settings_equivalent (settings1, settings2) | settings_equivalent _ = false fun problems_equivalent (p1 : problem, p2 : problem) = #univ_card p1 = #univ_card p2 andalso #formula p1 = #formula p2 andalso #bounds p1 = #bounds p2 andalso #expr_assigns p1 = #expr_assigns p2 andalso #tuple_assigns p1 = #tuple_assigns p2 andalso #int_bounds p1 = #int_bounds p2 andalso settings_equivalent (#settings p1, #settings p2) (** Serialization of problem **) fun base_name j = if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j fun atom_name j = "A" ^ base_name j fun atom_seq_name (k, 0) = "u" ^ base_name k | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0 fun formula_reg_name j = "$f" ^ base_name j fun rel_reg_name j = "$e" ^ base_name j fun int_reg_name j = "$i" ^ base_name j fun tuple_name x = n_ary_name x "A" "P" "T" fun rel_name x = n_ary_name x "s" "r" "m" fun var_name x = n_ary_name x "S" "R" "M" fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t" fun inline_comment "" = "" | inline_comment comment = " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^ " */" fun block_comment "" = "" | block_comment comment = prefix_lines "// " comment ^ "\n" fun commented_rel_name (x, s) = rel_name x ^ inline_comment s fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]" | string_for_tuple (TupleIndex x) = tuple_name x | string_for_tuple (TupleReg x) = tuple_reg_name x val no_prec = 100 val prec_TupleUnion = 1 val prec_TupleIntersect = 2 val prec_TupleProduct = 3 val prec_TupleProject = 4 fun precedence_ts (TupleUnion _) = prec_TupleUnion | precedence_ts (TupleDifference _) = prec_TupleUnion | precedence_ts (TupleIntersect _) = prec_TupleIntersect | precedence_ts (TupleProduct _) = prec_TupleProduct | precedence_ts (TupleProject _) = prec_TupleProject | precedence_ts _ = no_prec fun string_for_tuple_set tuple_set = let fun sub tuple_set outer_prec = let val prec = precedence_ts tuple_set val need_parens = (prec < outer_prec) in (if need_parens then "(" else "") ^ (case tuple_set of TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1) | TupleDifference (ts1, ts2) => sub ts1 prec ^ " - " ^ sub ts2 (prec + 1) | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]" | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}" | TupleRange (t1, t2) => "{" ^ string_for_tuple t1 ^ (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}" | TupleArea (t1, t2) => "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}" | TupleAtomSeq x => atom_seq_name x | TupleSetReg x => tuple_set_reg_name x) ^ (if need_parens then ")" else "") end in sub tuple_set 0 end fun string_for_tuple_assign (AssignTuple (x, t)) = tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n" | string_for_tuple_assign (AssignTupleSet (x, ts)) = tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n" fun string_for_bound (zs, tss) = "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^ (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^ (if length tss = 1 then "" else "]") ^ "\n" fun int_string_for_bound (opt_n, tss) = (case opt_n of SOME n => signed_string_of_int n ^ ": " | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" val prec_All = 1 val prec_Or = 2 val prec_Iff = 3 val prec_Implies = 4 val prec_And = 5 val prec_Not = 6 val prec_Eq = 7 val prec_Some = 8 val prec_SHL = 9 val prec_Add = 10 val prec_Mult = 11 val prec_Override = 12 val prec_Intersect = 13 val prec_Product = 14 val prec_IfNo = 15 val prec_Project = 17 val prec_Join = 18 val prec_BitNot = 19 fun precedence_f (All _) = prec_All | precedence_f (Exist _) = prec_All | precedence_f (FormulaLet _) = prec_All | precedence_f (FormulaIf _) = prec_All | precedence_f (Or _) = prec_Or | precedence_f (Iff _) = prec_Iff | precedence_f (Implies _) = prec_Implies | precedence_f (And _) = prec_And | precedence_f (Not _) = prec_Not | precedence_f (Acyclic _) = no_prec | precedence_f (Function _) = no_prec | precedence_f (Functional _) = no_prec | precedence_f (TotalOrdering _) = no_prec | precedence_f (Subset _) = prec_Eq | precedence_f (RelEq _) = prec_Eq | precedence_f (IntEq _) = prec_Eq | precedence_f (LT _) = prec_Eq | precedence_f (LE _) = prec_Eq | precedence_f (No _) = prec_Some | precedence_f (Lone _) = prec_Some | precedence_f (One _) = prec_Some | precedence_f (Some _) = prec_Some | precedence_f False = no_prec | precedence_f True = no_prec | precedence_f (FormulaReg _) = no_prec and precedence_r (RelLet _) = prec_All | precedence_r (RelIf _) = prec_All | precedence_r (Union _) = prec_Add | precedence_r (Difference _) = prec_Add | precedence_r (Override _) = prec_Override | precedence_r (Intersect _) = prec_Intersect | precedence_r (Product _) = prec_Product | precedence_r (IfNo _) = prec_IfNo | precedence_r (Project _) = prec_Project | precedence_r (Join _) = prec_Join | precedence_r (Closure _) = prec_BitNot | precedence_r (ReflexiveClosure _) = prec_BitNot | precedence_r (Transpose _) = prec_BitNot | precedence_r (Comprehension _) = no_prec | precedence_r (Bits _) = no_prec | precedence_r (Int _) = no_prec | precedence_r Iden = no_prec | precedence_r Ints = no_prec | precedence_r None = no_prec | precedence_r Univ = no_prec | precedence_r (Atom _) = no_prec | precedence_r (AtomSeq _) = no_prec | precedence_r (Rel _) = no_prec | precedence_r (Var _) = no_prec | precedence_r (RelReg _) = no_prec and precedence_i (Sum _) = prec_All | precedence_i (IntLet _) = prec_All | precedence_i (IntIf _) = prec_All | precedence_i (SHL _) = prec_SHL | precedence_i (SHA _) = prec_SHL | precedence_i (SHR _) = prec_SHL | precedence_i (Add _) = prec_Add | precedence_i (Sub _) = prec_Add | precedence_i (Mult _) = prec_Mult | precedence_i (Div _) = prec_Mult | precedence_i (Mod _) = prec_Mult | precedence_i (Cardinality _) = no_prec | precedence_i (SetSum _) = no_prec | precedence_i (BitOr _) = prec_Intersect | precedence_i (BitXor _) = prec_Intersect | precedence_i (BitAnd _) = prec_Intersect | precedence_i (BitNot _) = prec_BitNot | precedence_i (Neg _) = prec_BitNot | precedence_i (Absolute _) = prec_BitNot | precedence_i (Signum _) = prec_BitNot | precedence_i (Num _) = no_prec | precedence_i (IntReg _) = no_prec fun write_problem out problems = let fun out_outmost_f (And (f1, f2)) = (out_outmost_f f1; out "\n && "; out_outmost_f f2) | out_outmost_f f = out_f f prec_And and out_f formula outer_prec = let val prec = precedence_f formula val need_parens = (prec < outer_prec) in (if need_parens then out "(" else ()); (case formula of All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec) | Exist (ds, f) => (out "some ["; out_decls ds; out "] | "; out_f f prec) | FormulaLet (bs, f) => (out "let ["; out_assigns bs; out "] | "; out_f f prec) | FormulaIf (f, f1, f2) => (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else "; out_f f2 prec) | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec) | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec) | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec) | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec) | Not f => (out "! "; out_f f prec) | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")") | Function (x, r1, r2) => (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one "; out_r r2 0; out ")") | Functional (x, r1, r2) => (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone "; out_r r2 0; out ")") | TotalOrdering (x, r1, r2, r3) => (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", "; out_r r2 0; out ", "; out_r r3 0; out ")") | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec) | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec) | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec) | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec) | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec) | No r => (out "no "; out_r r prec) | Lone r => (out "lone "; out_r r prec) | One r => (out "one "; out_r r prec) | Some r => (out "some "; out_r r prec) | False => out "false" | True => out "true" | FormulaReg j => out (formula_reg_name j)); (if need_parens then out ")" else ()) end and out_r rel_expr outer_prec = let val prec = precedence_r rel_expr val need_parens = (prec < outer_prec) in (if need_parens then out "(" else ()); (case rel_expr of RelLet (bs, r) => (out "let ["; out_assigns bs; out "] | "; out_r r prec) | RelIf (f, r1, r2) => (out "if "; out_f f prec; out " then "; out_r r1 prec; out " else "; out_r r2 prec) | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1)) | Difference (r1, r2) => (out_r r1 prec; out " - "; out_r r2 (prec + 1)) | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec) | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec) | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec) | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec) | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]") | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1)) | Closure r => (out "^"; out_r r prec) | ReflexiveClosure r => (out "*"; out_r r prec) | Transpose r => (out "~"; out_r r prec) | Comprehension (ds, f) => (out "{["; out_decls ds; out "] | "; out_f f 0; out "}") | Bits i => (out "Bits["; out_i i 0; out "]") | Int i => (out "Int["; out_i i 0; out "]") | Iden => out "iden" | Ints => out "ints" | None => out "none" | Univ => out "univ" | Atom j => out (atom_name j) | AtomSeq x => out (atom_seq_name x) | Rel x => out (rel_name x) | Var x => out (var_name x) | RelReg (_, j) => out (rel_reg_name j)); (if need_parens then out ")" else ()) end and out_i int_expr outer_prec = let val prec = precedence_i int_expr val need_parens = (prec < outer_prec) in (if need_parens then out "(" else ()); (case int_expr of Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec) | IntLet (bs, i) => (out "let ["; out_assigns bs; out "] | "; out_i i prec) | IntIf (f, i1, i2) => (out "if "; out_f f prec; out " then "; out_i i1 prec; out " else "; out_i i2 prec) | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1)) | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1)) | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1)) | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1)) | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1)) | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1)) | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1)) | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1)) | Cardinality r => (out "#("; out_r r 0; out ")") | SetSum r => (out "sum("; out_r r 0; out ")") | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec) | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec) | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec) | BitNot i => (out "~"; out_i i prec) | Neg i => (out "-"; out_i i prec) | Absolute i => (out "abs "; out_i i prec) | Signum i => (out "sgn "; out_i i prec) | Num k => out (signed_string_of_int k) | IntReg j => out (int_reg_name j)); (if need_parens then out ")" else ()) end and out_decls [] = () | out_decls [d] = out_decl d | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds) and out_decl (DeclNo (x, r)) = (out (var_name x); out " : no "; out_r r 0) | out_decl (DeclLone (x, r)) = (out (var_name x); out " : lone "; out_r r 0) | out_decl (DeclOne (x, r)) = (out (var_name x); out " : one "; out_r r 0) | out_decl (DeclSome (x, r)) = (out (var_name x); out " : some "; out_r r 0) | out_decl (DeclSet (x, r)) = (out (var_name x); out " : set "; out_r r 0) and out_assigns [] = () | out_assigns [b] = out_assign b | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs) and out_assign (AssignFormulaReg (j, f)) = (out (formula_reg_name j); out " := "; out_f f 0) | out_assign (AssignRelReg ((_, j), r)) = (out (rel_reg_name j); out " := "; out_r r 0) | out_assign (AssignIntReg (j, i)) = (out (int_reg_name j); out " := "; out_i i 0) and out_columns [] = () | out_columns [i] = out_i i 0 | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is) and out_problem {comment, settings, univ_card, tuple_assigns, bounds, int_bounds, expr_assigns, formula} = (out ("\n" ^ block_comment comment ^ implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n") settings) ^ "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^ implode (map string_for_tuple_assign tuple_assigns) ^ implode (map string_for_bound bounds) ^ (if int_bounds = [] then "" else "int_bounds: " ^ commas (map int_string_for_bound int_bounds) ^ "\n")); List.app (fn b => (out_assign b; out ";")) expr_assigns; out "solve "; out_outmost_f formula; out ";\n") in out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ "// " ^ ATP_Util.timestamp () ^ "\n"); List.app out_problem problems end (** Parsing of solution **) fun is_ident_char s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "_" orelse s = "'" orelse s = "$" fun strip_blanks [] = [] | strip_blanks (" " :: ss) = strip_blanks ss | strip_blanks [s1, " "] = [s1] | strip_blanks (s1 :: " " :: s2 :: ss) = if is_ident_char s1 andalso is_ident_char s2 then s1 :: " " :: strip_blanks (s2 :: ss) else strip_blanks (s1 :: s2 :: ss) | strip_blanks (s :: ss) = s :: strip_blanks ss val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> (the o Int.fromString o implode) val scan_rel_name = ($$ "s" |-- scan_nat >> pair 1 || $$ "r" |-- scan_nat >> pair 2 || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'") >> (fn ((n, j), SOME _) => (n, ~j - 1) | ((n, j), NONE) => (n, j)) val scan_atom = $$ "A" |-- scan_nat fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan) fun parse_list scan = parse_non_empty_list scan || Scan.succeed [] val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]" val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]" val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set val parse_instance = Scan.this_string "relations:" |-- $$ "{" |-- parse_list parse_assignment --| $$ "}" val extract_instance = fst o Scan.finite Symbol.stopper (Scan.error (!! (fn _ => raise SYNTAX ("Kodkod.extract_instance", "ill-formed Kodkodi output")) parse_instance)) o strip_blanks o raw_explode val problem_marker = "*** PROBLEM " val outcome_marker = "---OUTCOME---\n" val instance_marker = "---INSTANCE---\n" fun read_section_body marker = Substring.string o fst o Substring.position "\n\n" o Substring.triml (size marker) fun read_next_instance s = let val s = Substring.position instance_marker s |> snd in if Substring.isEmpty s then raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker") else read_section_body instance_marker s |> extract_instance end fun read_next_outcomes j (s, ps, js) = let val (s1, s2) = Substring.position outcome_marker s in if Substring.isEmpty s2 orelse not (Substring.isEmpty (Substring.position problem_marker s1 |> snd)) then (s, ps, js) else let val outcome = read_section_body outcome_marker s2 val s = Substring.triml (size outcome_marker) s2 in if String.isSuffix "UNSATISFIABLE" outcome then read_next_outcomes j (s, ps, j :: js) else if String.isSuffix "SATISFIABLE" outcome then read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js) else raise SYNTAX ("Kodkod.read_next_outcomes", "unknown outcome " ^ quote outcome) end end fun read_next_problems (s, ps, js) = let val s = Substring.position problem_marker s |> snd in if Substring.isEmpty s then (ps, js) else let val s = Substring.triml (size problem_marker) s val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string |> Int.fromString |> the val j = j_plus_1 - 1 in read_next_problems (read_next_outcomes j (s, ps, js)) end end handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", "expected number after \"PROBLEM\"") (** Main Kodkod entry point **) fun serial_string_and_temporary_dir overlord = if overlord then ("", getenv "ISABELLE_HOME_USER") else (serial_string (), getenv "ISABELLE_TMP") (* The fudge term below is to account for Kodkodi's slow start-up time, which is partly due to the JVM and partly due to the ML "bash" function. *) val fudge_ms = 250 fun uncached_solve_any_problem overlord deadline max_threads0 max_solutions problems = let val j = find_index (curry (op =) True o #formula) problems val indexed_problems = if j >= 0 then [(j, nth problems j)] else filter_out (is_problem_trivially_false o snd) (0 upto length problems - 1 ~~ problems) val triv_js = filter_out (AList.defined (op =) indexed_problems) (0 upto length problems - 1) val reindex = fst o nth indexed_problems val max_threads = if max_threads0 = 0 then Options.default_int \<^system_option>\kodkod_max_threads\ else max_threads0 val external_process = not (Options.default_bool \<^system_option>\kodkod_scala\) orelse overlord val timeout0 = Time.toMilliseconds (deadline - Time.now ()) val timeout = if external_process then timeout0 - fudge_ms else timeout0 val solve_all = max_solutions > 1 in if null indexed_problems then Normal ([], triv_js, "") else if timeout <= 0 then TimedOut triv_js else let val kki = let val buf = Unsynchronized.ref Buffer.empty fun out s = Unsynchronized.change buf (Buffer.add s) val _ = write_problem out (map snd indexed_problems) in Buffer.content (! buf) end val (rc, out, err) = if external_process then let val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) val kki_path = path_for "kki" val out_path = path_for "out" val err_path = path_for "err" fun remove_temporary_files () = if overlord then () else List.app (ignore o try File.rm) [kki_path, out_path, err_path] in let val _ = File.write kki_path kki val rc = Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\ \\"$KODKODI/bin/kodkodi\"" ^ (" -max-msecs " ^ string_of_int timeout) ^ (if solve_all then " -solve-all" else "") ^ " -max-solutions " ^ string_of_int max_solutions ^ (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^ " < " ^ File.bash_path kki_path ^ " > " ^ File.bash_path out_path ^ " 2> " ^ File.bash_path err_path) val out = File.read out_path val err = File.read err_path val _ = remove_temporary_files () in (rc, out, err) end handle exn => (remove_temporary_files (); Exn.reraise exn) end else (timeout, (solve_all, (max_solutions, (max_threads, kki)))) |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end |> YXML.string_of_body - |> \<^scala_thread>\kodkod\ + |> \<^scala>\kodkod\ |> YXML.parse_body |> let open XML.Decode in triple int string string end val (ps, nontriv_js) = read_next_problems (Substring.full out, [], []) |>> rev ||> rev |> apfst (map (apfst reindex)) |> apsnd (map reindex) val js = triv_js @ nontriv_js val first_error = trim_split_lines err |> map (perhaps (try (unsuffix ".")) #> perhaps (try (unprefix "Solve error: ")) #> perhaps (try (unprefix "Error: "))) |> find_first (fn line => line <> "" andalso line <> "EXIT") |> the_default "" in if not (null ps) orelse rc = 0 then Normal (ps, js, first_error) else if rc = 2 then TimedOut js else if rc = 130 then raise Exn.Interrupt else Error (if first_error = "" then "Unknown error" else first_error, js) end end val cached_outcome = Synchronized.var "Kodkod.cached_outcome" (NONE : ((int * problem list) * outcome) option) fun solve_any_problem debug overlord deadline max_threads max_solutions problems = let fun do_solve () = uncached_solve_any_problem overlord deadline max_threads max_solutions problems in if debug orelse overlord then do_solve () else case AList.lookup (fn ((max1, ps1), (max2, ps2)) => max1 = max2 andalso length ps1 = length ps2 andalso forall problems_equivalent (ps1 ~~ ps2)) (the_list (Synchronized.value cached_outcome)) (max_solutions, problems) of SOME outcome => outcome | NONE => let val outcome = do_solve () in (case outcome of Normal (_, _, "") => Synchronized.change cached_outcome (K (SOME ((max_solutions, problems), outcome))) | _ => ()); outcome end end end; diff --git a/src/HOL/Tools/Nitpick/kodkod.scala b/src/HOL/Tools/Nitpick/kodkod.scala --- a/src/HOL/Tools/Nitpick/kodkod.scala +++ b/src/HOL/Tools/Nitpick/kodkod.scala @@ -1,178 +1,178 @@ /* Title: HOL/Tools/Nitpick/kodkod.scala Author: Makarius Scala interface for Kodkod. */ package isabelle.nitpick import isabelle._ import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor} import org.antlr.runtime.{ANTLRInputStream, RecognitionException} import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser} object Kodkod { /** result **/ sealed case class Result(rc: Int, out: String, err: String) { def ok: Boolean = rc == 0 def check: String = if (ok) out else error(if (err.isEmpty) "Error" else err) def encode: XML.Body = { import XML.Encode._ triple(int, string, string)((rc, out, err)) } } /** execute **/ def execute(source: String, solve_all: Boolean = false, prove: Boolean = false, max_solutions: Int = Integer.MAX_VALUE, cleanup_inst: Boolean = false, timeout: Time = Time.zero, max_threads: Int = 0): Result = { /* executor */ val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads val executor: ThreadPoolExecutor = new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy) val executor_killed = Synchronized(false) def executor_kill(): Unit = executor_killed.change(b => if (b) b else { Isabelle_Thread.fork() { executor.shutdownNow() }; true }) /* system context */ class Exit extends Exception("EXIT") class Exec_Context extends Context { private var rc = 0 private val out = new StringBuilder private val err = new StringBuilder def return_code(i: Int): Unit = synchronized { rc = rc max i} override def output(s: String): Unit = synchronized { Exn.Interrupt.expose() out ++= s out += '\n' } override def error(s: String): Unit = synchronized { Exn.Interrupt.expose() err ++= s err += '\n' } override def exit(i: Int): Unit = synchronized { return_code(i) executor_kill() throw new Exit } def result(): Result = synchronized { Result(rc, out.toString, err.toString) } } val context = new Exec_Context /* main */ try { val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream())) val parser = KodkodiParser.create(context, executor, false, solve_all, prove, max_solutions, cleanup_inst, lexer) val timeout_request = if (timeout.is_zero) None else { Some(Event_Timer.request(Time.now() + timeout) { context.error("Ran out of time") context.return_code(2) executor_kill() }) } try { parser.problems() } catch { case exn: RecognitionException => parser.reportError(exn) } timeout_request.foreach(_.cancel()) if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) { context.error("Error: trailing tokens") context.exit(1) } if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) { context.exit(1) } } catch { case _: Exit => case exn: Throwable => val message = exn.getMessage context.error(if (message.isEmpty) exn.toString else "Error: " + message) context.return_code(1) } executor.shutdownNow() context.result() } /** protocol handler **/ def warmup(): String = execute( "solver: \"MiniSat\"\n" + File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check class Handler extends Session.Protocol_Handler { override def init(session: Session): Unit = warmup() } /** scala function **/ - object Fun extends Scala.Fun("kodkod") + object Fun extends Scala.Fun("kodkod", thread = true) { val here = Scala_Project.here def apply(args: String): String = { val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) = { import XML.Decode._ pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args)) } val result = execute(kki, solve_all = solve_all, max_solutions = max_solutions, timeout = Time.ms(timeout), max_threads = max_threads) YXML.string_of_body(result.encode) } } } class Scala_Functions extends Scala.Functions(Kodkod.Fun) diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML @@ -1,742 +1,738 @@ (* Title: HOL/Tools/ATP/atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature SLEDGEHAMMER_ATP_SYSTEMS = sig type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int val force_sos : bool Config.T val term_order : string Config.T val e_smartN : string val e_autoN : string val e_fun_weightN : string val e_sym_offset_weightN : string val e_selection_heuristic : string Config.T val e_default_fun_weight : real Config.T val e_fun_weight_base : real Config.T val e_fun_weight_span : real Config.T val e_default_sym_offs_weight : real Config.T val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T val spass_H1SOS : string val spass_H2 : string val spass_H2LR0LT0 : string val spass_H2NuVS0 : string val spass_H2NuVS0Red2 : string val spass_H2SOS : string val is_vampire_noncommercial_license_accepted : unit -> bool option val remote_atp : string -> string -> string list -> (string * string) list -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val effective_term_order : Proof.context -> string -> term_order end; structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate (* ATP configuration *) val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} (* "best_slices" must be found empirically, taking a holistic approach since the ATPs are run in parallel. Each slice has the format (time_frac, ((max_facts, fact_filter), format, type_enc, lam_trans, uncurried_aliases), extra) where time_frac = faction of the time available given to the slice (which should add up to 1.0) extra = extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the time available if the other slices fail early and also because it is used if slicing is disabled (e.g., by the minimizer). *) val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val tstp_proof_delims = [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")] val known_perl_failures = [(CantConnect, "HTTP error"), (NoPerl, "env: perl"), (NoLibwwwPerl, "Can't locate HTTP")] fun known_szs_failures wrap = [(Unprovable, wrap "CounterSatisfiable"), (Unprovable, wrap "Satisfiable"), (GaveUp, wrap "GaveUp"), (GaveUp, wrap "Unknown"), (GaveUp, wrap "Incomplete"), (ProofMissing, wrap "Theorem"), (ProofMissing, wrap "Unsatisfiable"), (TimedOut, wrap "Timeout"), (Inappropriate, wrap "Inappropriate"), (OutOfResources, wrap "ResourceOut"), (OutOfResources, wrap "MemoryOut"), (Interrupted, wrap "Forced"), (Interrupted, wrap "User")] val known_szs_status_failures = known_szs_failures (prefix "SZS status ") val known_says_failures = known_szs_failures (prefix " says ") structure Data = Theory_Data ( type T = ((unit -> atp_config) * stamp) Symtab.table val empty = Symtab.empty val extend = I fun merge data : T = Symtab.merge (eq_snd (op =)) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) ) fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) val sosN = "sos" val no_sosN = "no_sos" val force_sos = Attrib.setup_config_bool \<^binding>\atp_force_sos\ (K false) val smartN = "smart" (* val kboN = "kbo" *) val lpoN = "lpo" val xweightsN = "_weights" val xprecN = "_prec" val xsimpN = "_simp" (* SPASS-specific *) (* Possible values for "atp_term_order": "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) val term_order = Attrib.setup_config_string \<^binding>\atp_term_order\ (K smartN) (* agsyHOL *) val agsyhol_config : atp_config = {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val agsyhol = (agsyholN, fn () => agsyhol_config) (* Alt-Ergo *) val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [], known_failures = [(ProofMissing, ": Valid"), (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) val e_smartN = "smart" val e_autoN = "auto" val e_fun_weightN = "fun_weight" val e_sym_offset_weightN = "sym_offset_weight" val e_selection_heuristic = Attrib.setup_config_string \<^binding>\atp_e_selection_heuristic\ (K e_smartN) (* FUDGE *) val e_default_fun_weight = Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) val e_fun_weight_base = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_base\ (K 0.0) val e_fun_weight_span = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_span\ (K 40.0) val e_default_sym_offs_weight = Attrib.setup_config_real \<^binding>\atp_e_default_sym_offs_weight\ (K 1.0) val e_sym_offs_weight_base = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_base\ (K ~20.0) val e_sym_offs_weight_span = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_span\ (K 60.0) fun e_selection_heuristic_case heuristic fw sow = if heuristic = e_fun_weightN then fw else if heuristic = e_sym_offset_weightN then sow else raise Fail ("unexpected " ^ quote heuristic) fun scaled_e_selection_weight ctxt heuristic w = w * Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_span e_sym_offs_weight_span) + Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int fun e_selection_weight_arguments ctxt heuristic sel_weights = if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS," ^ (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_selection_weight ctxt heuristic w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))' " else "-xAuto " val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," fun e_ord_precedence [_] = "" | e_ord_precedence info = info |> map fst |> space_implode "<" fun e_term_order_info_arguments false false _ = "" | e_term_order_info_arguments gen_weights gen_prec ord_info = let val ord_info = ord_info () in (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") end val e_config : atp_config = {exec = (["E_HOME"], ["eprover"]), arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--auto-schedule --tstp-in --tstp-out --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name, proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, best_slices = fn ctxt => let val heuristic = Config.get ctxt e_selection_heuristic val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS val (format, enc) = if modern then (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher_fool") else (TFF (Without_FOOL, Monomorphic), "mono_native") in (* FUDGE *) if heuristic = e_smartN then [(0.15, (((128, meshN), format, enc, combsN, false), e_fun_weightN)), (0.15, (((128, mashN), format, enc, combsN, false), e_sym_offset_weightN)), (0.15, (((91, mepoN), format, enc, combsN, false), e_autoN)), (0.15, (((1000, meshN), format, "poly_guards??", combsN, false), e_sym_offset_weightN)), (0.15, (((256, mepoN), format, enc, liftingN, false), e_fun_weightN)), (0.25, (((64, mashN), format, enc, combsN, false), e_fun_weightN))] else [(1.0, (((500, ""), format, enc, combsN, false), heuristic))] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e = (eN, fn () => e_config) (* iProver *) val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$E_HOME\"/eprover " ^ "--clausifier_options \"--tstp-format --silent --cnf\" " ^ "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val iprover = (iproverN, fn () => iprover_config) (* LEO-II *) val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo.opt", "leo"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo2 = (leo2N, fn () => leo2_config) (* Leo-III *) (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = {exec = (["LEO3_HOME"], ["leo3"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--nleq --naeq " else ""), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo3 = (leo3N, fn () => leo3_config) (* Satallax *) (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => (case getenv "E_HOME" of "" => "" | home => "-E " ^ home ^ "/eprover ") ^ "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val satallax = (satallaxN, fn () => satallax_config) (* SPASS *) val spass_H1SOS = "-Heuristic=1 -SOS" val spass_H2 = "-Heuristic=2" val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0" val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0" val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = let val format = DFG Monomorphic in {exec = (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(GaveUp, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), (InternalError, "Please report this error")] @ known_perl_failures, prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) [(0.1667, (((150, meshN), format, "mono_native", combsN, true), "")), (0.1667, (((500, meshN), format, "mono_native", liftingN, true), spass_H2SOS)), (0.1666, (((50, meshN), format, "mono_native", liftingN, true), spass_H2LR0LT0)), (0.1000, (((250, meshN), format, "mono_native", combsN, true), spass_H2NuVS0)), (0.1000, (((1000, mepoN), format, "mono_native", liftingN, true), spass_H1SOS)), (0.1000, (((150, meshN), format, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), (0.1000, (((300, meshN), format, "mono_native", combsN, true), spass_H2SOS)), (0.1000, (((100, meshN), format, "mono_native", combs_and_liftingN, true), spass_H2))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end val spass = (spassN, fn () => spass_config) (* Vampire *) fun is_vampire_noncommercial_license_accepted () = let val flag = Options.default_string \<^system_option>\vampire_noncommercial\ |> String.map Char.toLower in if flag = "yes" then SOME true else if flag = "no" then SOME false else NONE end fun check_vampire_noncommercial () = (case is_vampire_noncommercial_license_accepted () of SOME true => () | SOME false => error (Pretty.string_of (Pretty.para "The Vampire prover may be used only for noncommercial applications")) | NONE => error (Pretty.string_of (Pretty.para "The Vampire prover is not activated; to activate it, set the Isabelle system option \ \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \ \/ Isabelle / General)"))) val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS" val vampire_full_proof_options = " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0" val remote_vampire_command = "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s" val vampire_config : atp_config = let val format = TFF (Without_FOOL, Monomorphic) in {exec = (["VAMPIRE_HOME"], ["vampire"]), arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => (check_vampire_noncommercial (); vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name |> sos = sosN ? prefix "--sos on "), proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")] @ tstp_proof_delims, known_failures = [(GaveUp, "UNPROVABLE"), (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = fn ctxt => (* FUDGE *) [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)), (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)), (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))] |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} end val vampire = (vampireN, fn () => vampire_config) (* Z3 with TPTP syntax (half experimental, half legacy) *) val z3_tptp_config : atp_config = let val format = TFF (Without_FOOL, Monomorphic) in {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, proof_delims = [("SZS status Theorem", "")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")), (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")), (0.125, (((62, mashN), format, "mono_native", combsN, false), "")), (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} end val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) (* Zipperposition *) val zipperposition_blsimp = "--mode ho-pragmatic --max-inferences 3 --ho-max-app-projections 0 --ho-max-elims 0 --ho-max-rigid-imitations 2 --ho-max-identifications 0 --ho-unif-max-depth 2 --boolean-reasoning no-cases --ext-rules ext-family --ext-rules-max-depth 1 --kbo-weight-fun invdocc --ho-prim-enum tf --ho-prim-enum-early-bird true --tptp-def-as-rewrite --ho-unif-level pragmatic-framework -q '1|const|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)' -q '1|prefer-sos|staggered(1)' -q '2|prefer-fo|default' -q '1|prefer-neg-unit|orient-lmax(2,1,2,1,1)' -q '2|prefer-easy-ho|conjecture-relative-struct(1.5,3.5,2,3)' --ho-elim-leibniz 2 --ho-fixpoint-decider true --ho-pattern-decider false --ho-solid-decider true --ho-max-solidification 12 --select e-selection11 --solve-formulas true --sup-at-vars false --sup-at-var-headed false --lazy-cnf true --lazy-cnf-kind simp --lazy-cnf-renaming-threshold 4 --sine 50 --sine-tolerance 1.7 --sine-depth-max 3 --sine-depth-min 1 --sine-trim-implications true --ho-selection-restriction none --sup-from-var-headed false --sine-trim-implications true" val zipperposition_s6 = "--tptp-def-as-rewrite --rewrite-before-cnf true --mode ho-competitive --boolean-reasoning no-cases --ext-rules off --ho-prim-enum none --recognize-injectivity true --ho-elim-leibniz off --ho-unif-level full-framework --no-max-vars -q '3|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-ho-steps|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|fifo' -q '3|by-app-var-num|pnrefined(2,1,1,1,2,2,2)' --select ho-selection5 --prec-gen-fun unary_first --solid-subsumption false --ignore-orphans false --ho-solid-decider true --ho-fixpoint-decider true --ho-pattern-decider true --sup-at-vars false --sup-at-var-headed false --sup-from-var-headed false --ho-neg-ext-simpl true" val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -q '6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)' -q '6|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-processed|fifo' -q '1|prefer-non-goals|conjecture-relative-var(1,l,f)' -q '4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)' --select e-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank" val zipperposition_config : atp_config = let val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice) in {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)), (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} end val zipperposition = (zipperpositionN, fn () => zipperposition_config) (* Remote ATP invocation via SystemOnTPTP *) -val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list) +val no_remote_systems = {url = "", systems = [] : string list} +val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems fun get_remote_systems () = - Timeout.apply (seconds 10.0) (fn () => - (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of - (output, 0) => split_lines output - | (output, _) => - (warning - (case extract_known_atp_failure known_perl_failures output of - SOME failure => string_of_atp_failure failure - | NONE => output); []))) () - handle Timeout.TIMEOUT _ => [] + Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems () + handle ERROR msg => (warning msg; no_remote_systems) + | Timeout.TIMEOUT _ => no_remote_systems fun find_remote_system name [] systems = find_first (String.isPrefix (name ^ "---")) systems | find_remote_system name (version :: versions) systems = case find_first (String.isPrefix (name ^ "---" ^ version)) systems of NONE => find_remote_system name versions systems | res => res fun get_remote_system name versions = - Synchronized.change_result remote_systems (fn systems => - (if null systems then get_remote_systems () else systems) - |> `(`(find_remote_system name versions))) + Synchronized.change_result remote_systems (fn remote => + (if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote) + then get_remote_systems () else remote) |> ` #systems) + |> `(find_remote_system name versions) fun the_remote_system name versions = (case get_remote_system name versions of (SOME sys, _) => sys | (NONE, []) => error "SystemOnTPTP is currently not available" | (NONE, syss) => (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of [] => error "SystemOnTPTP is currently not available" | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) | syss => error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ => (if command <> "" then "-c " ^ quote command ^ " " else "") ^ "-s " ^ the_remote_system system_name system_versions ^ " " ^ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ " " ^ file_name, proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, prem_role = prem_role, best_slices = fn ctxt => [(1.0, best_slice ctxt)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions best_slice ({proof_delims, known_failures, prem_role, ...} : atp_config) = remote_config system_name system_versions proof_delims known_failures prem_role best_slice fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice = (remote_prefix ^ name, fn () => remote_config system_name system_versions proof_delims known_failures prem_role best_slice) fun remotify_atp (name, config) system_name system_versions best_slice = (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) fun gen_remote_waldmeister name type_enc = remote_atp name "Waldmeister" ["710"] tstp_proof_delims ([(OutOfResources, "Too many function symbols"), (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["THF-4.4"] (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.0"] (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) (* Dummy prover *) fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K (K ""))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, best_slices = K [(1.0, (((200, ""), format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val dummy_tfx_format = TFF (With_FOOL, Polymorphic) val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config) (* Setup *) fun add_atp (name, config) thy = Data.map (Symtab.update_new (name, (config, stamp ()))) thy handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) fun get_atp thy name = fst (the (Symtab.lookup (Data.get thy) name)) handle Option.Option => error ("Unknown ATP: " ^ name) val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in exists (fn var => getenv var <> "") (fst exec) end fun refresh_systems_on_tptp () = Synchronized.change remote_systems (fn _ => get_remote_systems ()) fun effective_term_order ctxt atp = let val ord = Config.get ctxt term_order in if ord = smartN then {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), gen_simp = false} else let val is_lpo = String.isSubstring lpoN ord in {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} end end val atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx] val _ = Theory.setup (fold add_atp atps) end; diff --git a/src/HOL/Tools/etc/options b/src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options +++ b/src/HOL/Tools/etc/options @@ -1,45 +1,48 @@ (* :mode=isabelle-options: *) section "Automatically tried tools" public option auto_time_start : real = 1.0 -- "initial delay for automatically tried tools (seconds)" public option auto_time_limit : real = 2.0 -- "time limit for automatically tried tools (seconds > 0)" public option auto_nitpick : bool = false -- "run Nitpick automatically" public option auto_sledgehammer : bool = false -- "run Sledgehammer automatically" public option auto_methods : bool = false -- "try standard proof methods automatically" public option auto_quickcheck : bool = true -- "run Quickcheck automatically" public option auto_solve_direct : bool = true -- "run solve_direct automatically" section "Miscellaneous Tools" public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" -- "provers for Sledgehammer (separated by blanks)" public option sledgehammer_timeout : int = 30 -- "provers will be interrupted after this time (in seconds)" public option vampire_noncommercial : string = "unknown" -- "status of Vampire activation for noncommercial use (yes, no, unknown)" +public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply" + -- "URL for SystemOnTPTP service" + public option MaSh : string = "sml" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" public option kodkod_scala : bool = true -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" public option kodkod_max_threads : int = 0 -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" diff --git a/src/HOL/Tools/etc/settings b/src/HOL/Tools/etc/settings --- a/src/HOL/Tools/etc/settings +++ b/src/HOL/Tools/etc/settings @@ -1,4 +1,6 @@ # -*- shell-script -*- :mode=shellscript: isabelle_scala_service 'isabelle.nitpick.Kodkod$Handler' isabelle_scala_service 'isabelle.nitpick.Scala_Functions' + +ISABELLE_ATP="$COMPONENT/ATP" diff --git a/src/Pure/Admin/components.scala b/src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala +++ b/src/Pure/Admin/components.scala @@ -1,354 +1,353 @@ /* Title: Pure/Admin/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} object Components { /* archive name */ object Archive { val suffix: String = ".tar.gz" def apply(name: String): String = if (name == "") error("Bad component name: " + quote(name)) else name + suffix def unapply(archive: String): Option[String] = { for { name0 <- Library.try_unsuffix(suffix, archive) name <- proper_string(name0) } yield name } def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) } /* component collections */ def default_component_repository: String = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + name) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check name } def resolve(base_dir: Path, names: List[String], target_dir: Option[Path] = None, copy_dir: Option[Path] = None, progress: Progress = new Progress): Unit = { Isabelle_System.make_directory(base_dir) for (name <- names) { val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) if (!archive.is_file) { val remote = Components.default_component_repository + "/" + archive_name - progress.echo("Getting " + remote) - Bytes.write(archive, Url.read_bytes(Url(remote))) + Isabelle_System.download(remote, archive, progress = progress) } for (dir <- copy_dir) { Isabelle_System.make_directory(dir) Isabelle_System.copy_file(archive, dir) } unpack(target_dir getOrElse base_dir, archive, progress = progress) } } def purge(dir: Path, platform: Platform.Family.Value): Unit = { def purge_platforms(platforms: String*): Set[String] = platforms.flatMap(name => List("arm64-" + name, "x86-" + name, "x86_64_32-" + name, "x86_64-" + name)).toSet + "ppc-darwin" + "arm64-linux" val purge_set = platform match { case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows") case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows") case Platform.Family.windows => purge_platforms("linux", "darwin") } File.find_files(dir.file, (file: JFile) => file.isDirectory && purge_set(file.getName), include_dirs = true).foreach(Isabelle_System.rm_tree) } /* component directory content */ def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") def check_dir(dir: Path): Boolean = settings(dir).is_file || components(dir).is_file def read_components(dir: Path): List[String] = split_lines(File.read(components(dir))).filter(_.nonEmpty) def write_components(dir: Path, lines: List[String]): Unit = File.write(components(dir), terminate_lines(lines)) /* component repository content */ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") sealed case class SHA1_Digest(sha1: String, file_name: String) { override def toString: String = sha1 + " " + file_name } def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => Word.explode(line) match { case Nil => None case List(sha1, name) => Some(SHA1_Digest(sha1, name)) case _ => error("Bad components.sha1 entry: " + quote(line)) }) def write_components_sha1(entries: List[SHA1_Digest]): Unit = File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) /** manage user components **/ val components_path = Path.explode("$ISABELLE_HOME_USER/etc/components") def read_components(): List[String] = if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) else Nil def write_components(lines: List[String]): Unit = { Isabelle_System.make_directory(components_path.dir) File.write(components_path, Library.terminate_lines(lines)) } def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { val path = path0.expand.absolute if (!(path + Path.explode("etc/settings")).is_file && !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path) val lines1 = read_components() val lines2 = lines1.filter(line => line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) val lines3 = if (add) lines2 ::: List(path.implode) else lines2 if (lines1 != lines3) write_components(lines3) val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" progress.echo(prefix + " component " + path) } /* main entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { for (arg <- args) { val add = if (arg.startsWith("+")) true else if (arg.startsWith("-")) false else error("Bad argument: " + quote(arg)) val path = Path.explode(arg.substring(1)) update_components(add, path, progress = new Console_Progress) } } } /** build and publish components **/ def build_components( options: Options, components: List[Path], progress: Progress = new Progress, publish: Boolean = false, force: Boolean = false, update_components_sha1: Boolean = false): Unit = { val archives: List[Path] = for (path <- components) yield { path.file_name match { case Archive(_) => path case name => if (!path.is_dir) error("Bad component directory: " + path) else if (!check_dir(path)) { error("Malformed component directory: " + path + "\n (requires " + settings() + " or " + Components.components() + ")") } else { val component_path = path.expand val archive_dir = component_path.dir val archive_name = Archive(name) val archive = archive_dir + Path.explode(archive_name) if (archive.is_file && !force) { error("Component archive already exists: " + archive) } progress.echo("Packaging " + archive_name) Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), dir = archive_dir).check archive } } } if ((publish && archives.nonEmpty) || update_components_sha1) { options.string("isabelle_components_server") match { case SSH.Target(user, host) => using(SSH.open_session(options, host = host, user = user))(ssh => { val components_dir = Path.explode(options.string("isabelle_components_dir")) val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { error("Bad remote directory: " + dir) } if (publish) { for (archive <- archives) { val archive_name = archive.file_name val name = Archive.get_name(archive_name) val remote_component = components_dir + archive.base val remote_contrib = contrib_dir + Path.explode(name) // component archive if (ssh.is_file(remote_component) && !force) { error("Remote component archive already exists: " + remote_component) } progress.echo("Uploading " + archive_name) ssh.write_file(remote_component, archive) // contrib directory val is_standard_component = Isabelle_System.with_tmp_dir("component")(tmp_dir => { Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check check_dir(tmp_dir + Path.explode(name)) }) if (is_standard_component) { if (ssh.is_dir(remote_contrib)) { if (force) ssh.rm_tree(remote_contrib) else error("Remote component directory already exists: " + remote_contrib) } progress.echo("Unpacking remote " + archive_name) ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + ssh.bash_path(remote_component)).check } else { progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } } // remote SHA1 digests if (update_components_sha1) { val lines = for { entry <- ssh.read_dir(components_dir) if entry.is_file && entry.name.endsWith(Archive.suffix) } yield { progress.echo("Digesting remote " + entry.name) ssh.execute("cd " + ssh.bash_path(components_dir) + "; sha1sum " + Bash.string(entry.name)).check.out } write_components_sha1(read_components_sha1(lines)) } }) case s => error("Bad isabelle_components_server: " + quote(s)) } } // local SHA1 digests { val new_entries = for (archive <- archives) yield { val file_name = archive.file_name progress.echo("Digesting local " + file_name) val sha1 = SHA1.digest(archive).rep SHA1_Digest(sha1, file_name) } val new_names = new_entries.map(_.file_name).toSet write_components_sha1( new_entries ::: read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) } } /* Isabelle tool wrapper */ private val relevant_options = List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") val isabelle_tool = Isabelle_Tool("build_components", "build and publish Isabelle components", Scala_Project.here, args => { var publish = false var update_components_sha1 = false var force = false var options = Options.init() def show_options: String = cat_lines(relevant_options.map(name => options.options(name).print)) val getopts = Getopts(""" Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... Options are: -P publish on SSH server (see options below) -f force: overwrite existing component archives and directories -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u update all SHA1 keys in Isabelle repository Admin/components Build and publish Isabelle components as .tar.gz archives on SSH server, depending on system options: """ + Library.prefix_lines(" ", show_options) + "\n", "P" -> (_ => publish = true), "f" -> (_ => force = true), "o:" -> (arg => options = options + arg), "u" -> (_ => update_components_sha1 = true)) val more_args = getopts(args) if (more_args.isEmpty && !update_components_sha1) getopts.usage() val progress = new Console_Progress build_components(options, more_args.map(Path.explode), progress = progress, publish = publish, force = force, update_components_sha1 = update_components_sha1) }) } diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala +++ b/src/Pure/General/bytes.scala @@ -1,214 +1,215 @@ /* Title: Pure/General/bytes.scala Author: Makarius Immutable byte vectors versus UTF8 strings. */ package isabelle import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream, OutputStream, InputStream, FileInputStream, FileOutputStream} import java.net.URL import java.util.Base64 import org.tukaani.xz.{XZInputStream, XZOutputStream} object Bytes { val empty: Bytes = new Bytes(Array[Byte](), 0, 0) def apply(s: CharSequence): Bytes = { val str = s.toString if (str.isEmpty) empty else { val b = UTF8.bytes(str) new Bytes(b, 0, b.length) } } def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length) def apply(a: Array[Byte], offset: Int, length: Int): Bytes = if (length == 0) empty else { val b = new Array[Byte](length) System.arraycopy(a, offset, b, 0, length) new Bytes(b, 0, b.length) } val newline: Bytes = apply("\n") def base64(s: String): Bytes = { val a = Base64.getDecoder.decode(s) new Bytes(a, 0, a.length) } /* read */ def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes = if (limit == 0) empty else { - val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit) + val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024 + val out = new ByteArrayOutputStream(out_size) val buf = new Array[Byte](8192) var m = 0 do { m = stream.read(buf, 0, buf.size min (limit - out.size)) if (m != -1) out.write(buf, 0, m) } while (m != -1 && limit > out.size) new Bytes(out.toByteArray, 0, out.size) } def read(file: JFile): Bytes = { val length = file.length val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt using(new FileInputStream(file))(read_stream(_, limit = limit)) } def read(path: Path): Bytes = read(path.file) def read(url: URL): Bytes = using(url.openStream)(read_stream(_)) /* write */ def write(file: JFile, bytes: Bytes): Unit = using(new FileOutputStream(file))(bytes.write_stream(_)) def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes) } final class Bytes private( protected val bytes: Array[Byte], protected val offset: Int, val length: Int) extends CharSequence { /* equality */ override def equals(that: Any): Boolean = { that match { case other: Bytes => if (this eq other) true else if (length != other.length) false else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i)) case _ => false } } private lazy val hash: Int = { var h = 0 for (i <- offset until offset + length) { val b = bytes(i).asInstanceOf[Int] & 0xFF h = 31 * h + b } h } override def hashCode(): Int = hash /* content */ lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes) def is_empty: Boolean = length == 0 def iterator: Iterator[Byte] = for (i <- (offset until (offset + length)).iterator) yield bytes(i) def array: Array[Byte] = { val a = new Array[Byte](length) System.arraycopy(bytes, offset, a, 0, length) a } def text: String = UTF8.decode_chars(s => s, bytes, offset, offset + length).toString def base64: String = { val b = if (offset == 0 && length == bytes.length) bytes else Bytes(bytes, offset, length).bytes Base64.getEncoder.encodeToString(b) } def maybe_base64: (Boolean, String) = { val s = text if (this == Bytes(s)) (false, s) else (true, base64) } override def toString: String = "Bytes(" + length + ")" def proper: Option[Bytes] = if (is_empty) None else Some(this) def proper_text: Option[String] = if (is_empty) None else Some(text) def +(other: Bytes): Bytes = if (other.is_empty) this else if (is_empty) other else { val new_bytes = new Array[Byte](length + other.length) System.arraycopy(bytes, offset, new_bytes, 0, length) System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length) new Bytes(new_bytes, 0, new_bytes.length) } /* CharSequence operations */ def charAt(i: Int): Char = if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char] else throw new IndexOutOfBoundsException def subSequence(i: Int, j: Int): Bytes = { if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i) else throw new IndexOutOfBoundsException } def trim_line: Bytes = if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) subSequence(0, length - 2) else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) subSequence(0, length - 1) else this /* streams */ def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length) def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length) /* XZ data compression */ def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes = using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length)) def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = { val result = new ByteArrayOutputStream(length) using(new XZOutputStream(result, options, cache))(write_stream(_)) new Bytes(result.toByteArray, 0, result.size) } def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()) : (Boolean, Bytes) = { val compressed = compress(options = options, cache = cache) if (compressed.length < length) (true, compressed) else (false, this) } } 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,166 +1,301 @@ /* Title: Pure/General/http.scala Author: Makarius HTTP server support. */ package isabelle -import java.net.{InetAddress, InetSocketAddress, URI} +import java.io.{File => JFile} +import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection} import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} -import scala.collection.immutable.SortedMap - 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) + { + def text: String = new String(bytes.array, encoding) + def text_lines: List[String] = Library.trim_split_lines(text) + } + + 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.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 + using(connection.getInputStream)(stream => + { + val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) + 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) + }) + } + + 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 = "application/octet-stream"): Response = + content_type: String = mime_type_bytes): Response = new Response(bytes, content_type) val empty: Response = apply() - def text(s: String): Response = apply(Bytes(s), "text/plain; charset=utf-8") - def html(s: String): Response = apply(Bytes(s), "text/html; charset=utf-8") + 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 */ - - class Handler private[HTTP](val root: String, val handler: HttpHandler) - { - override def toString: String = root - } - - def handler(root: String, body: Exchange => Unit): Handler = - new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) }) - - - /* particular methods */ + /* 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)) }) } - def method(name: String, root: String, body: Arg => Option[Response]): Handler = - handler(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 + object Handler + { + def apply(root: String, body: Exchange => Unit): Handler = + new Handler(root, + new HttpHandler { def handle(x: HttpExchange): Unit = 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) - }) + 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) + 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 */ val welcome: Handler = - get("/", arg => + Handler.get("/", arg => if (arg.uri.toString == "/") { val id = Isabelle_System.isabelle_id() Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) } else None) /* fonts */ private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(hidden = true) def fonts(root: String = "/fonts"): Handler = - get(root, arg => + 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/General/url.scala b/src/Pure/General/url.scala --- a/src/Pure/General/url.scala +++ b/src/Pure/General/url.scala @@ -1,110 +1,106 @@ /* Title: Pure/General/url.scala Author: Makarius Basic URL operations. */ package isabelle import java.io.{File => JFile} import java.nio.file.{Paths, FileSystemNotFoundException} import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder} import java.util.Locale import java.util.zip.GZIPInputStream object Url { /* special characters */ def escape_special(c: Char): String = if ("!#$&'()*+,/:;=?@[]".contains(c)) { String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt)) } else c.toString def escape_special(s: String): String = s.iterator.map(escape_special).mkString def escape_name(name: String): String = name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString /* make and check URLs */ def apply(name: String): URL = { try { new URL(name) } catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } } def is_wellformed(name: String): Boolean = try { Url(name); true } catch { case ERROR(_) => false } def is_readable(name: String): Boolean = try { Url(name).openStream.close(); true } catch { case ERROR(_) => false } - /* trim index */ + /* file name */ + + def file_name(url: URL): String = + Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString def trim_index(url: URL): URL = { Library.try_unprefix("/index.html", url.toString) match { case Some(u) => Url(u) case None => Library.try_unprefix("/index.php", url.toString) match { case Some(u) => Url(u) case None => url } } } /* strings */ def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name) def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name) /* read */ private def read(url: URL, gzip: Boolean): String = using(url.openStream)(stream => File.read_stream(if (gzip) new GZIPInputStream(stream) else stream)) def read(url: URL): String = read(url, false) def read_gzip(url: URL): String = read(url, true) def read(name: String): String = read(Url(name), false) def read_gzip(name: String): String = read(Url(name), true) - def read_bytes(url: URL): Bytes = - { - val connection = url.openConnection - val length = connection.getContentLength - using(connection.getInputStream)(Bytes.read_stream(_, hint = length)) - } - /* file URIs */ def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString def print_file_name(name: String): String = print_file(new JFile(name)) def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile def is_wellformed_file(uri: String): Boolean = try { parse_file(uri); true } catch { case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException => false } def absolute_file(uri: String): JFile = File.absolute(parse_file(uri)) def absolute_file_name(uri: String): String = absolute_file(uri).getPath def canonical_file(uri: String): JFile = File.canonical(parse_file(uri)) def canonical_file_name(uri: String): String = canonical_file(uri).getPath } diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML +++ b/src/Pure/PIDE/markup.ML @@ -1,786 +1,785 @@ (* Title: Pure/PIDE/markup.ML Author: Makarius Quasi-abstract markup elements. *) signature MARKUP = sig type T = string * Properties.T val empty: T val is_empty: T -> bool val properties: Properties.T -> T -> T val nameN: string val name: string -> T -> T val xnameN: string val xname: string -> T -> T val kindN: string val serialN: string val serial_properties: int -> Properties.T val instanceN: string val meta_titleN: string val meta_title: T val meta_creatorN: string val meta_creator: T val meta_contributorN: string val meta_contributor: T val meta_dateN: string val meta_date: T val meta_licenseN: string val meta_license: T val meta_descriptionN: string val meta_description: T val languageN: string val symbolsN: string val delimitedN: string val is_delimited: Properties.T -> bool val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_Isar: bool -> T val language_method: T val language_attribute: T val language_sort: bool -> T val language_type: bool -> T val language_term: bool -> T val language_prop: bool -> T val language_ML: bool -> T val language_SML: bool -> T val language_document: bool -> T val language_document_marker: T val language_antiquotation: T val language_text: bool -> T val language_verbatim: bool -> T val language_latex: bool -> T val language_rail: T val language_path: bool -> T val language_url: bool -> T val language_mixfix: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val defN: string val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string val end_offsetN: string val fileN: string val idN: string val position_properties: string list val position_property: Properties.entry -> bool val positionN: string val position: T val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T val export_pathN: string val export_path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T val toolN: string val tool: string -> T val markupN: string val consistentN: string val unbreakableN: string val block_properties: string list val indentN: string val widthN: string val blockN: string val block: bool -> int -> T val breakN: string val break: int -> int -> T val fbreakN: string val fbreak: T val itemN: string val item: T val wordsN: string val words: T val hiddenN: string val hidden: T val deleteN: string val delete: T val bash_functionN: string val scala_functionN: string val system_optionN: string val sessionN: string val theoryN: string val classN: string val type_nameN: string val constantN: string val fixedN: string val fixed: string -> T val caseN: string val case_: string -> T val dynamic_factN: string val dynamic_fact: string -> T val literal_factN: string val literal_fact: string -> T val method_modifierN: string val tfreeN: string val tfree: T val tvarN: string val tvar: T val freeN: string val free: T val skolemN: string val skolem: T val boundN: string val bound: T val varN: string val var: T val numeralN: string val numeral: T val literalN: string val literal: T val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T val inner_cartoucheN: string val inner_cartouche: T val token_rangeN: string val token_range: T val sortingN: string val sorting: T val typingN: string val typing: T val class_parameterN: string val class_parameter: T val ML_keyword1N: string val ML_keyword1: T val ML_keyword2N: string val ML_keyword2: T val ML_keyword3N: string val ML_keyword3: T val ML_delimiterN: string val ML_delimiter: T val ML_tvarN: string val ML_tvar: T val ML_numeralN: string val ML_numeral: T val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T val ML_commentN: string val ML_comment: T val ML_defN: string val ML_openN: string val ML_structureN: string val ML_typingN: string val ML_typing: T val ML_breakpointN: string val ML_breakpoint: int -> T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val file_typeN: string val antiquotationN: string val ML_antiquotationN: string val document_antiquotationN: string val document_antiquotation_optionN: string val raw_textN: string val raw_text: T val plain_textN: string val plain_text: T val paragraphN: string val paragraph: T val text_foldN: string val text_fold: T val document_markerN: string val document_marker: T val document_tagN: string val document_tag: string -> T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T val markdown_listN: string val markdown_list: string -> T val itemizeN: string val enumerateN: string val descriptionN: string val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command_properties: T -> T val keywordN: string val keyword_properties: T -> T val stringN: string val string: T val alt_stringN: string val alt_string: T val verbatimN: string val verbatim: T val cartoucheN: string val cartouche: T val commentN: string val comment: T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T val keyword3N: string val keyword3: T val quasi_keywordN: string val quasi_keyword: T val improperN: string val improper: T val operatorN: string val operator: T val comment1N: string val comment1: T val comment2N: string val comment2: T val comment3N: string val comment3: T val elapsedN: string val cpuN: string val gcN: string val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T val parse_command_timing_properties: Properties.T -> ({file: string, offset: int, name: string} * Time.time) option val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T val command_indentN: string val command_indent: int -> T val goalN: string val goal: T val subgoalN: string val subgoal: string -> T val taskN: string val forkedN: string val forked: T val joinedN: string val joined: T val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T val canceledN: string val canceled: T val initializedN: string val initialized: T val finalizedN: string val finalized: T val consolidatingN: string val consolidating: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string val statusN: string val status: T val resultN: string val result: T val writelnN: string val writeln: T val stateN: string val state: T val informationN: string val information: T val tracingN: string val tracing: T val warningN: string val warning: T val legacyN: string val legacy: T val errorN: string val error: T val systemN: string val system: T val protocolN: string val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: unit -> T val intensifyN: string val intensify: T val browserN: string val graphviewN: string val theory_exportsN: string val sendbackN: string val paddingN: string val padding_line: Properties.entry val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string val functionN: string val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T val assign_update: Properties.T val removed_versions: Properties.T - val invoke_scala: string -> string -> bool -> Properties.T + val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T val task_statistics: Properties.entry val command_timing: Properties.entry val theory_timing: Properties.entry val session_timing: Properties.entry val loading_theory: string -> Properties.T val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T val exportN: string type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool} val export: export_args -> Properties.T val debugger_state: string -> Properties.T val debugger_output: string -> Properties.T val simp_trace_panelN: string val simp_trace_logN: string val simp_trace_stepN: string val simp_trace_recurseN: string val simp_trace_hintN: string val simp_trace_ignoreN: string val simp_trace_cancel: serial -> Properties.T type output = Output.output * Output.output val no_output: output val add_mode: string -> (T -> output) -> unit val output: T -> output val enclose: T -> Output.output -> Output.output val markup: T -> string -> string val markups: T list -> string -> string val markup_only: T -> string val markup_report: string -> string end; structure Markup: MARKUP = struct (** markup elements **) (* basic markup *) type T = string * Properties.T; val empty = ("", []); fun is_empty ("", _) = true | is_empty _ = false; fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); fun markup_elem name = (name, (name, []): T); fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); (* misc properties *) val nameN = "name"; fun name a = properties [(nameN, a)]; val xnameN = "xname"; fun xname a = properties [(xnameN, a)]; val kindN = "kind"; val serialN = "serial"; fun serial_properties i = [(serialN, Value.print_int i)]; val instanceN = "instance"; (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *) val (meta_titleN, meta_title) = markup_elem "meta_title"; val (meta_creatorN, meta_creator) = markup_elem "meta_creator"; val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor"; val (meta_dateN, meta_date) = markup_elem "meta_date"; val (meta_licenseN, meta_license) = markup_elem "meta_license"; val (meta_descriptionN, meta_description) = markup_elem "meta_description"; (* embedded languages *) val languageN = "language"; val symbolsN = "symbols"; val antiquotesN = "antiquotes"; val delimitedN = "delimited" fun is_delimited props = Properties.get props delimitedN = SOME "true"; fun language {name, symbols, antiquotes, delimited} = (languageN, [(nameN, name), (symbolsN, Value.print_bool symbols), (antiquotesN, Value.print_bool antiquotes), (delimitedN, Value.print_bool delimited)]); fun language' {name, symbols, antiquotes} delimited = language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; val language_method = language {name = "method", symbols = true, antiquotes = false, delimited = false}; val language_attribute = language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; val language_type = language' {name = "type", symbols = true, antiquotes = false}; val language_term = language' {name = "term", symbols = true, antiquotes = false}; val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; val language_document = language' {name = "document", symbols = false, antiquotes = true}; val language_document_marker = language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; val language_path = language' {name = "path", symbols = false, antiquotes = false}; val language_url = language' {name = "url", symbols = false, antiquotes = false}; val language_mixfix = language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; (* formal entities *) val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; fun entity kind name = (entityN, (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); val defN = "def"; val refN = "ref"; (* completion *) val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; val (updateN, update) = markup_elem "update"; (* position *) val lineN = "line"; val end_lineN = "end_line"; val offsetN = "offset"; val end_offsetN = "end_offset"; val fileN = "file"; val idN = "id"; val position_properties = [lineN, offsetN, end_offsetN, fileN, idN]; fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry); val (positionN, position) = markup_elem "position"; (* expression *) val expressionN = "expression"; fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); (* citation *) val (citationN, citation) = markup_string "citation" nameN; (* external resources *) val (pathN, path) = markup_string "path" nameN; val (export_pathN, export_path) = markup_string "export_path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; val (toolN, tool) = markup_string "tool" nameN; (* pretty printing *) val markupN = "markup"; val consistentN = "consistent"; val unbreakableN = "unbreakable"; val indentN = "indent"; val block_properties = [markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; val blockN = "block"; fun block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val breakN = "break"; fun break w i = (breakN, (if w <> 0 then [(widthN, Value.print_int w)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val (fbreakN, fbreak) = markup_elem "fbreak"; val (itemN, item) = markup_elem "item"; (* text properties *) val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; val (deleteN, delete) = markup_elem "delete"; (* misc entities *) val bash_functionN = "bash_function"; val scala_functionN = "scala_function"; val system_optionN = "system_option"; val sessionN = "session"; val theoryN = "theory"; val classN = "class"; val type_nameN = "type_name"; val constantN = "constant"; val (fixedN, fixed) = markup_string "fixed" nameN; val (caseN, case_) = markup_string "case" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; val method_modifierN = "method_modifier"; (* inner syntax *) val (tfreeN, tfree) = markup_elem "tfree"; val (tvarN, tvar) = markup_elem "tvar"; val (freeN, free) = markup_elem "free"; val (skolemN, skolem) = markup_elem "skolem"; val (boundN, bound) = markup_elem "bound"; val (varN, var) = markup_elem "var"; val (numeralN, numeral) = markup_elem "numeral"; val (literalN, literal) = markup_elem "literal"; val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; val (token_rangeN, token_range) = markup_elem "token_range"; val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; val (class_parameterN, class_parameter) = markup_elem "class_parameter"; (* ML *) val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; val ML_defN = "ML_def"; val ML_openN = "ML_open"; val ML_structureN = "ML_structure"; val (ML_typingN, ML_typing) = markup_elem "ML_typing"; val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; (* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; val file_typeN = "file_type"; val antiquotationN = "antiquotation"; val ML_antiquotationN = "ML_antiquotation"; val document_antiquotationN = "document_antiquotation"; val document_antiquotation_optionN = "document_antiquotation_option"; (* document text *) val (raw_textN, raw_text) = markup_elem "raw_text"; val (plain_textN, plain_text) = markup_elem "plain_text"; val (paragraphN, paragraph) = markup_elem "paragraph"; val (text_foldN, text_fold) = markup_elem "text_fold"; val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; (* Markdown document structure *) val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; val itemizeN = "itemize"; val enumerateN = "enumerate"; val descriptionN = "description"; (* formal input *) val inputN = "input"; fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); (* outer syntax *) val (command_keywordN, command_keyword) = markup_elem "command_keyword"; val commandN = "command"; val command_properties = properties [(kindN, commandN)]; val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; val (keyword1N, keyword1) = markup_elem "keyword1"; val (keyword2N, keyword2) = markup_elem "keyword2"; val (keyword3N, keyword3) = markup_elem "keyword3"; val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; val (improperN, improper) = markup_elem "improper"; val (operatorN, operator) = markup_elem "operator"; val (stringN, string) = markup_elem "string"; val (alt_stringN, alt_string) = markup_elem "alt_string"; val (verbatimN, verbatim) = markup_elem "verbatim"; val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; (* comments *) val (comment1N, comment1) = markup_elem "comment1"; val (comment2N, comment2) = markup_elem "comment2"; val (comment3N, comment3) = markup_elem "comment3"; (* timing *) val elapsedN = "elapsed"; val cpuN = "cpu"; val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = [(elapsedN, Value.print_time elapsed), (cpuN, Value.print_time cpu), (gcN, Value.print_time gc)]; val timingN = "timing"; fun timing t = (timingN, timing_properties t); (* command timing *) fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => SOME ({file = file, offset = Value.parse_int offset, name = name}, Properties.seconds props elapsedN) | _ => NONE); (* indentation *) val (command_indentN, command_indent) = markup_int "command_indent" indentN; (* goals *) val (goalN, goal) = markup_elem "goal"; val (subgoalN, subgoal) = markup_string "subgoal" nameN; (* command status *) val taskN = "task"; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; val (finalizedN, finalized) = markup_elem "finalized"; val (consolidatingN, consolidating) = markup_elem "consolidating"; val (consolidatedN, consolidated) = markup_elem "consolidated"; (* messages *) val exec_idN = "exec_id"; val initN = "init"; val (statusN, status) = markup_elem "status"; val (resultN, result) = markup_elem "result"; val (writelnN, writeln) = markup_elem "writeln"; val (stateN, state) = markup_elem "state" val (informationN, information) = markup_elem "information"; val (tracingN, tracing) = markup_elem "tracing"; val (warningN, warning) = markup_elem "warning"; val (legacyN, legacy) = markup_elem "legacy"; val (errorN, error) = markup_elem "error"; val (systemN, system) = markup_elem "system"; val protocolN = "protocol"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; val badN = "bad"; fun bad () = (badN, serial_properties (serial ())); val (intensifyN, intensify) = markup_elem "intensify"; (* active areas *) val browserN = "browser" val graphviewN = "graphview"; val theory_exportsN = "theory_exports"; val sendbackN = "sendback"; val paddingN = "padding"; val padding_line = (paddingN, "line"); val padding_command = (paddingN, "command"); val dialogN = "dialog"; fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); val jedit_actionN = "jedit_action"; (* protocol message functions *) val functionN = "function" fun ML_statistics {pid, stats_dir} = [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; val commands_accepted = [(functionN, "commands_accepted")]; val assign_update = [(functionN, "assign_update")]; val removed_versions = [(functionN, "removed_versions")]; -fun invoke_scala name id thread = - [(functionN, "invoke_scala"), (nameN, name), (idN, id), ("thread", Value.print_bool thread)]; +fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; val task_statistics = (functionN, "task_statistics"); val command_timing = (functionN, "command_timing"); val theory_timing = (functionN, "theory_timing"); val session_timing = (functionN, "session_timing"); fun loading_theory name = [("function", "loading_theory"), (nameN, name)]; val build_session_finished = [("function", "build_session_finished")]; val print_operationsN = "print_operations"; val print_operations = [(functionN, print_operationsN)]; (* export *) val exportN = "export"; type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), (nameN, name), ("executable", Value.print_bool executable), ("compress", Value.print_bool compress), ("strict", Value.print_bool strict)]; (* debugger *) fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; (* simplifier trace *) val simp_trace_panelN = "simp_trace_panel"; val simp_trace_logN = "simp_trace_log"; val simp_trace_stepN = "simp_trace_step"; val simp_trace_recurseN = "simp_trace_recurse"; val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; (** print mode operations **) type output = Output.output * Output.output; val no_output = ("", ""); local val default = {output = Output_Primitives.markup_fn}; val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); in fun add_mode name output = Synchronized.change modes (fn tab => (if not (Symtab.defined tab name) then () else Output.warning ("Redefining markup mode " ^ quote name); Symtab.update (name, {output = output}) tab)); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output m = if is_empty m then no_output else #output (get_mode ()) m; val enclose = output #-> Library.enclose; fun markup m = let val (bg, en) = output m in Library.enclose (Output.escape bg) (Output.escape en) end; val markups = fold_rev markup; fun markup_only m = markup m ""; fun markup_report "" = "" | markup_report txt = markup report txt; end; diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala +++ b/src/Pure/PIDE/markup.scala @@ -1,740 +1,739 @@ /* Title: Pure/PIDE/markup.scala Author: Makarius Quasi-abstract markup elements. */ package isabelle object Markup { /* elements */ object Elements { def apply(elems: Set[String]): Elements = new Elements(elems) def apply(elems: String*): Elements = apply(Set(elems: _*)) val empty: Elements = apply() val full: Elements = new Elements(Set.empty) { override def apply(elem: String): Boolean = true override def toString: String = "Elements.full" } } sealed class Elements private[Markup](private val rep: Set[String]) { def apply(elem: String): Boolean = rep.contains(elem) def + (elem: String): Elements = new Elements(rep + elem) def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep) def - (elem: String): Elements = new Elements(rep - elem) def -- (elems: Elements): Elements = new Elements(rep -- elems.rep) override def toString: String = rep.mkString("Elements(", ",", ")") } /* properties */ val NAME = "name" val Name = new Properties.String(NAME) val XNAME = "xname" val XName = new Properties.String(XNAME) val KIND = "kind" val Kind = new Properties.String(KIND) val CONTENT = "content" val Content = new Properties.String(CONTENT) val SERIAL = "serial" val Serial = new Properties.Long(SERIAL) val INSTANCE = "instance" val Instance = new Properties.String(INSTANCE) /* basic markup */ val Empty: Markup = Markup("", Nil) val Broken: Markup = Markup("broken", Nil) class Markup_String(val name: String, prop: String) { private val Prop = new Properties.String(prop) def apply(s: String): Markup = Markup(name, Prop(s)) def unapply(markup: Markup): Option[String] = if (markup.name == name) Prop.unapply(markup.properties) else None } class Markup_Int(val name: String, prop: String) { private val Prop = new Properties.Int(prop) def apply(i: Int): Markup = Markup(name, Prop(i)) def unapply(markup: Markup): Option[Int] = if (markup.name == name) Prop.unapply(markup.properties) else None } class Markup_Long(val name: String, prop: String) { private val Prop = new Properties.Long(prop) def apply(i: Long): Markup = Markup(name, Prop(i)) def unapply(markup: Markup): Option[Long] = if (markup.name == name) Prop.unapply(markup.properties) else None } /* meta data */ val META_TITLE = "meta_title" val META_CREATOR = "meta_creator" val META_CONTRIBUTOR = "meta_contributor" val META_DATE = "meta_date" val META_LICENSE = "meta_license" val META_DESCRIPTION = "meta_description" /* formal entities */ val BINDING = "binding" val ENTITY = "entity" val Def = new Properties.Long("def") val Ref = new Properties.Long("ref") object Entity { object Def { def unapply(markup: Markup): Option[Long] = if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None } object Ref { def unapply(markup: Markup): Option[Long] = if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None } object Occ { def unapply(markup: Markup): Option[Long] = Def.unapply(markup) orElse Ref.unapply(markup) } def unapply(markup: Markup): Option[(String, String)] = markup match { case Markup(ENTITY, props) => val kind = Kind.unapply(props).getOrElse("") val name = Name.unapply(props).getOrElse("") Some((kind, name)) case _ => None } } /* completion */ val COMPLETION = "completion" val NO_COMPLETION = "no_completion" val UPDATE = "update" /* position */ val LINE = "line" val END_LINE = "line" val OFFSET = "offset" val END_OFFSET = "end_offset" val FILE = "file" val ID = "id" val DEF_LINE = "def_line" val DEF_OFFSET = "def_offset" val DEF_END_OFFSET = "def_end_offset" val DEF_FILE = "def_file" val DEF_ID = "def_id" val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1) val POSITION = "position" /* expression */ val EXPRESSION = "expression" object Expression { def unapply(markup: Markup): Option[String] = markup match { case Markup(EXPRESSION, Kind(kind)) => Some(kind) case Markup(EXPRESSION, _) => Some("") case _ => None } } /* citation */ val CITATION = "citation" val Citation = new Markup_String(CITATION, NAME) /* embedded languages */ val Symbols = new Properties.Boolean("symbols") val Antiquotes = new Properties.Boolean("antiquotes") val Delimited = new Properties.Boolean("delimited") val LANGUAGE = "language" object Language { val DOCUMENT = "document" val ML = "ML" val SML = "SML" val PATH = "path" val UNKNOWN = "unknown" def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] = markup match { case Markup(LANGUAGE, props) => (props, props, props, props) match { case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => Some((name, symbols, antiquotes, delimited)) case _ => None } case _ => None } object Path { def unapply(markup: Markup): Option[Boolean] = markup match { case Language(PATH, _, _, delimited) => Some(delimited) case _ => None } } } /* external resources */ val PATH = "path" val Path = new Markup_String(PATH, NAME) val EXPORT_PATH = "export_path" val Export_Path = new Markup_String(EXPORT_PATH, NAME) val URL = "url" val Url = new Markup_String(URL, NAME) val DOC = "doc" val Doc = new Markup_String(DOC, NAME) /* pretty printing */ val Consistent = new Properties.Boolean("consistent") val Indent = new Properties.Int("indent") val Width = new Properties.Int("width") object Block { val name = "block" def apply(c: Boolean, i: Int): Markup = Markup(name, (if (c) Consistent(c) else Nil) ::: (if (i != 0) Indent(i) else Nil)) def unapply(markup: Markup): Option[(Boolean, Int)] = if (markup.name == name) { val c = Consistent.unapply(markup.properties).getOrElse(false) val i = Indent.unapply(markup.properties).getOrElse(0) Some((c, i)) } else None } object Break { val name = "break" def apply(w: Int, i: Int): Markup = Markup(name, (if (w != 0) Width(w) else Nil) ::: (if (i != 0) Indent(i) else Nil)) def unapply(markup: Markup): Option[(Int, Int)] = if (markup.name == name) { val w = Width.unapply(markup.properties).getOrElse(0) val i = Indent.unapply(markup.properties).getOrElse(0) Some((w, i)) } else None } val ITEM = "item" val BULLET = "bullet" val SEPARATOR = "separator" /* text properties */ val WORDS = "words" val HIDDEN = "hidden" val DELETE = "delete" /* misc entities */ val THEORY = "theory" val CLASS = "class" val TYPE_NAME = "type_name" val FIXED = "fixed" val CASE = "case" val CONSTANT = "constant" val DYNAMIC_FACT = "dynamic_fact" /* inner syntax */ val TFREE = "tfree" val TVAR = "tvar" val FREE = "free" val SKOLEM = "skolem" val BOUND = "bound" val VAR = "var" val NUMERAL = "numeral" val LITERAL = "literal" val DELIMITER = "delimiter" val INNER_STRING = "inner_string" val INNER_CARTOUCHE = "inner_cartouche" val TOKEN_RANGE = "token_range" val SORTING = "sorting" val TYPING = "typing" val CLASS_PARAMETER = "class_parameter" val ATTRIBUTE = "attribute" val METHOD = "method" /* antiquotations */ val ANTIQUOTED = "antiquoted" val ANTIQUOTE = "antiquote" val ML_ANTIQUOTATION = "ML_antiquotation" val DOCUMENT_ANTIQUOTATION = "document_antiquotation" val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option" /* document text */ val RAW_TEXT = "raw_text" val PLAIN_TEXT = "plain_text" val PARAGRAPH = "paragraph" val TEXT_FOLD = "text_fold" object Document_Tag { val ELEMENT = "document_tag" val IMPORTANT = "important" val UNIMPORTANT = "unimportant" def unapply(markup: Markup): Option[String] = markup match { case Markup(ELEMENT, Name(name)) => Some(name) case _ => None } } /* Markdown document structure */ val MARKDOWN_PARAGRAPH = "markdown_paragraph" val MARKDOWN_ITEM = "markdown_item" val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") val Markdown_List = new Markup_String("markdown_list", "kind") val ITEMIZE = "itemize" val ENUMERATE = "enumerate" val DESCRIPTION = "description" /* ML */ val ML_KEYWORD1 = "ML_keyword1" val ML_KEYWORD2 = "ML_keyword2" val ML_KEYWORD3 = "ML_keyword3" val ML_DELIMITER = "ML_delimiter" val ML_TVAR = "ML_tvar" val ML_NUMERAL = "ML_numeral" val ML_CHAR = "ML_char" val ML_STRING = "ML_string" val ML_COMMENT = "ML_comment" val ML_DEF = "ML_def" val ML_OPEN = "ML_open" val ML_STRUCTURE = "ML_structure" val ML_TYPING = "ML_typing" val ML_BREAKPOINT = "ML_breakpoint" /* outer syntax */ val COMMAND = "command" val KEYWORD = "keyword" val KEYWORD1 = "keyword1" val KEYWORD2 = "keyword2" val KEYWORD3 = "keyword3" val QUASI_KEYWORD = "quasi_keyword" val IMPROPER = "improper" val OPERATOR = "operator" val STRING = "string" val ALT_STRING = "alt_string" val VERBATIM = "verbatim" val CARTOUCHE = "cartouche" val COMMENT = "comment" val LOAD_COMMAND = "load_command" /* comments */ val COMMENT1 = "comment1" val COMMENT2 = "comment2" val COMMENT3 = "comment3" /* timing */ val Elapsed = new Properties.Double("elapsed") val CPU = new Properties.Double("cpu") val GC = new Properties.Double("gc") object Timing_Properties { def apply(timing: isabelle.Timing): Properties.T = Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds) def unapply(props: Properties.T): Option[isabelle.Timing] = (props, props, props) match { case (Elapsed(elapsed), CPU(cpu), GC(gc)) => Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) case _ => None } def parse(props: Properties.T): isabelle.Timing = unapply(props) getOrElse isabelle.Timing.zero } val TIMING = "timing" object Timing { def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing)) def unapply(markup: Markup): Option[isabelle.Timing] = markup match { case Markup(TIMING, Timing_Properties(timing)) => Some(timing) case _ => None } } /* process result */ val Return_Code = new Properties.Int("return_code") object Process_Result { def apply(result: Process_Result): Properties.T = Return_Code(result.rc) ::: (if (result.timing.is_zero) Nil else Timing_Properties(result.timing)) def unapply(props: Properties.T): Option[Process_Result] = props match { case Return_Code(rc) => val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero) Some(isabelle.Process_Result(rc, timing = timing)) case _ => None } } /* command indentation */ object Command_Indent { val name = "command_indent" def unapply(markup: Markup): Option[Int] = if (markup.name == name) Indent.unapply(markup.properties) else None } /* goals */ val GOAL = "goal" val SUBGOAL = "subgoal" /* command status */ val TASK = "task" val ACCEPTED = "accepted" val FORKED = "forked" val JOINED = "joined" val RUNNING = "running" val FINISHED = "finished" val FAILED = "failed" val CANCELED = "canceled" val INITIALIZED = "initialized" val FINALIZED = "finalized" val CONSOLIDATING = "consolidating" val CONSOLIDATED = "consolidated" /* interactive documents */ val VERSION = "version" val ASSIGN = "assign" /* prover process */ val PROVER_COMMAND = "prover_command" val PROVER_ARG = "prover_arg" /* messages */ val INIT = "init" val STATUS = "status" val REPORT = "report" val RESULT = "result" val WRITELN = "writeln" val STATE = "state" val INFORMATION = "information" val TRACING = "tracing" val WARNING = "warning" val LEGACY = "legacy" val ERROR = "error" val NODES_STATUS = "nodes_status" val PROTOCOL = "protocol" val SYSTEM = "system" val STDOUT = "stdout" val STDERR = "stderr" val EXIT = "exit" val WRITELN_MESSAGE = "writeln_message" val STATE_MESSAGE = "state_message" val INFORMATION_MESSAGE = "information_message" val TRACING_MESSAGE = "tracing_message" val WARNING_MESSAGE = "warning_message" val LEGACY_MESSAGE = "legacy_message" val ERROR_MESSAGE = "error_message" val messages = Map( WRITELN -> WRITELN_MESSAGE, STATE -> STATE_MESSAGE, INFORMATION -> INFORMATION_MESSAGE, TRACING -> TRACING_MESSAGE, WARNING -> WARNING_MESSAGE, LEGACY -> LEGACY_MESSAGE, ERROR -> ERROR_MESSAGE) val message: String => String = messages.withDefault((s: String) => s) val NO_REPORT = "no_report" val BAD = "bad" val INTENSIFY = "intensify" /* active areas */ val BROWSER = "browser" val GRAPHVIEW = "graphview" val THEORY_EXPORTS = "theory_exports" val SENDBACK = "sendback" val PADDING = "padding" val PADDING_LINE = (PADDING, "line") val PADDING_COMMAND = (PADDING, "command") val DIALOG = "dialog" val Result = new Properties.String(RESULT) val JEDIT_ACTION = "jedit_action" /* protocol message functions */ val FUNCTION = "function" class Function(val name: String) { val PROPERTY: Properties.Entry = (FUNCTION, name) } class Properties_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[Properties.T] = props match { case PROPERTY :: args => Some(args) case _ => None } } class Name_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[String] = props match { case List(PROPERTY, (NAME, a)) => Some(a) case _ => None } } object ML_Statistics extends Function("ML_statistics") { def unapply(props: Properties.T): Option[(Long, String)] = props match { case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => Some((pid, stats_dir)) case _ => None } } val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name) def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1) object Command_Timing extends Properties_Function("command_timing") object Theory_Timing extends Properties_Function("theory_timing") object Session_Timing extends Properties_Function("session_timing") { val Threads = new Properties.Int("threads") } object Task_Statistics extends Properties_Function("task_statistics") object Loading_Theory extends Properties_Function("loading_theory") object Build_Session_Finished extends Function("build_session_finished") object Commands_Accepted extends Function("commands_accepted") object Assign_Update extends Function("assign_update") object Removed_Versions extends Function("removed_versions") object Invoke_Scala extends Function("invoke_scala") { - def unapply(props: Properties.T): Option[(String, String, Boolean)] = + def unapply(props: Properties.T): Option[(String, String)] = props match { - case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) => - Some((name, id, thread)) + case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) case _ => None } } object Cancel_Scala extends Function("cancel_scala") { def unapply(props: Properties.T): Option[String] = props match { case List(PROPERTY, (ID, id)) => Some(id) case _ => None } } val PRINT_OPERATIONS = "print_operations" /* export */ val EXPORT = "export" val THEORY_NAME = "theory_name" val EXECUTABLE = "executable" val COMPRESS = "compress" val STRICT = "strict" /* debugger output */ val DEBUGGER_STATE = "debugger_state" object Debugger_State { def unapply(props: Properties.T): Option[String] = props match { case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) case _ => None } } val DEBUGGER_OUTPUT = "debugger_output" object Debugger_Output { def unapply(props: Properties.T): Option[String] = props match { case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name) case _ => None } } /* simplifier trace */ val SIMP_TRACE_PANEL = "simp_trace_panel" val SIMP_TRACE_LOG = "simp_trace_log" val SIMP_TRACE_STEP = "simp_trace_step" val SIMP_TRACE_RECURSE = "simp_trace_recurse" val SIMP_TRACE_HINT = "simp_trace_hint" val SIMP_TRACE_IGNORE = "simp_trace_ignore" val SIMP_TRACE_CANCEL = "simp_trace_cancel" object Simp_Trace_Cancel { def unapply(props: Properties.T): Option[Long] = props match { case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i) case _ => None } } /* XML data representation */ def encode: XML.Encode.T[Markup] = (markup: Markup) => { import XML.Encode._ pair(string, properties)((markup.name, markup.properties)) } def decode: XML.Decode.T[Markup] = (body: XML.Body) => { import XML.Decode._ val (name, props) = pair(string, properties)(body) Markup(name, props) } } sealed case class Markup(name: String, properties: Properties.T) { def markup(s: String): String = YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) def update_properties(more_props: Properties.T): Markup = if (more_props.isEmpty) this else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) }) def + (entry: Properties.Entry): Markup = Markup(name, Properties.put(properties, entry)) } diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,439 +1,435 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, scala_functions: (string * Position.T) list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: string -> unit val init_session_file: Path.T -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time val scala_functions: unit -> string list val check_scala_function: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, scala_functions = Symtab.empty: Position.T Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, session_chapters, bibtex_entries, command_timings, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (session_chapters, (bibtex_entries, (command_timings, (scala_functions, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) (pair (list (pair string properties)) (pair (list (pair string string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, command_timings = command_timings, scala_functions = map (apsnd Position.of_properties) scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_file path = init_session_yxml (File.read path) before File.rm path; fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)) (get_session_base1 #session_positions) ctxt arg; fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name); fun last_timing tr = get_timings (get_session_base1 #timings) tr; (* Scala functions *) (*raw bootstrap environment*) fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); (*regular resources*) fun scala_function_pos name = (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name)); fun check_scala_function ctxt arg = Completion.check_entity Markup.scala_functionN (scala_functions () |> sort_strings |> map scala_function_pos) ctxt arg; val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) check_scala_function #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => let val name = check_scala_function ctxt arg - in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #> - ML_Antiquotation.value_embedded \<^binding>\scala_thread\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => - let val name = check_scala_function ctxt arg - in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end))); + in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); val extend = I; fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => (case Token.get_files tok of [] => let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos delimited) src_paths end | files => map Exn.release files)); val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ : Path.T = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => let val _ = check ctxt NONE source; val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)); in Latex.enclose_block "\\isatt{" "}" [latex] end); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala +++ b/src/Pure/System/bash.scala @@ -1,235 +1,235 @@ /* Title: Pure/System/bash.scala Author: Makarius GNU bash processes, with propagation of interrupts. */ package isabelle import java.io.{File => JFile, BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter} import scala.annotation.tailrec object Bash { /* concrete syntax */ private def bash_chr(c: Byte): String = { val ch = c.toChar ch match { case '\t' => "$'\\t'" case '\n' => "$'\\n'" case '\f' => "$'\\f'" case '\r' => "$'\\r'" case _ => if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) Symbol.ascii(ch) else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" else "\\" + ch } } def string(s: String): String = if (s == "") "\"\"" else UTF8.bytes(s).iterator.map(bash_chr).mkString def strings(ss: List[String]): String = ss.iterator.map(Bash.string).mkString(" ") /* process and result */ type Watchdog = (Time, Process => Boolean) def process(script: String, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = new Process(script, cwd, env, redirect, cleanup) class Process private[Bash]( script: String, cwd: JFile, env: Map[String, String], redirect: Boolean, cleanup: () => Unit) { private val timing_file = Isabelle_System.tmp_file("bash_timing") private val timing = Synchronized[Option[Timing]](None) def get_timing: Timing = timing.value getOrElse Timing.zero private val script_file = Isabelle_System.tmp_file("bash_script") File.write(script_file, script) private val proc = Isabelle_System.process( List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", File.standard_path(timing_file), "bash", File.standard_path(script_file)), cwd = cwd, env = env, redirect = redirect) // channels val stdin: BufferedWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) val stdout: BufferedReader = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) val stderr: BufferedReader = new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) // signals private val pid = stdout.readLine @tailrec private def kill(signal: String, count: Int = 1): Boolean = { count <= 0 || { Isabelle_System.kill(signal, pid) val running = Isabelle_System.kill("0", pid)._2 == 0 if (running) { Time.seconds(0.1).sleep kill(signal, count - 1) } else false } } def terminate(): Unit = Isabelle_Thread.try_uninterruptible { kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") proc.destroy() do_cleanup() } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { Isabelle_System.kill("INT", pid) } // JVM shutdown hook private val shutdown_hook = Isabelle_Thread.create(() => terminate()) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } // cleanup private def do_cleanup(): Unit = { try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } script_file.delete timing.change { case None => if (timing_file.isFile) { val t = Word.explode(File.read(timing_file)) match { case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero } timing_file.delete Some(t) } else Some(Timing.zero) case some => some } cleanup() } // join def join: Int = { val rc = proc.waitFor do_cleanup() rc } // result def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Watchdog] = None, strict: Boolean = true): Process_Result = { stdin.close() val out_lines = Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } val err_lines = Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } val watchdog_thread = for ((time, check) <- watchdog) yield { Future.thread("bash_watchdog") { while (proc.isAlive) { time.sleep if (check(this)) interrupt() } } } val rc = try { join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } watchdog_thread.foreach(_.cancel()) if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join, get_timing) } } /* Scala function */ - object Process extends Scala.Fun("bash_process") + object Process extends Scala.Fun("bash_process", thread = true) { val here = Scala_Project.here def apply(script: String): String = { val result = Exn.capture { Isabelle_System.bash(script) } val is_interrupt = result match { case Exn.Res(res) => res.rc == Exn.Interrupt.return_code case Exn.Exn(exn) => Exn.is_interrupt(exn) } result match { case _ if is_interrupt => "" case Exn.Exn(exn) => Exn.message(exn) case Exn.Res(res) => Library.cat_strings0( res.rc.toString :: res.timing.elapsed.ms.toString :: res.timing.cpu.ms.toString :: res.out_lines.length.toString :: res.out_lines ::: res.err_lines) } } } } diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,117 +1,117 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val make_directory: Path.T -> Path.T val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val rm_tree: Path.T -> unit val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> Path.T -> unit end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_process script = - Scala.function_thread "bash_process" + Scala.function "bash_process" ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> split_strings0 |> (fn [] => raise Exn.Interrupt | [err] => error err | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); val (out_lines, err_lines) = chop (Value.parse_int d) lines; in Process_Result.make {rc = rc, out_lines = out_lines, err_lines = err_lines, timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end | _ => raise Fail "Malformed Isabelle/Scala result"); val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let val res = bash_process s; val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = bash_process "declare -Fx" |> Process_Result.check |> Process_Result.out_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory and file operations *) val absolute_path = Path.implode o File.absolute_path; fun scala_function0 name = ignore o Scala.function name o cat_strings0; fun scala_function name = scala_function0 name o map absolute_path; fun make_directory path = (scala_function "make_directory" [path]; path); fun copy_dir src dst = scala_function "copy_dir" [src, dst]; fun copy_file src dst = scala_function "copy_file" [src, dst]; fun copy_file_base (base_dir, src) target_dir = scala_function0 "copy_file_base" [absolute_path base_dir, Path.implode src, absolute_path target_dir]; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun rm_tree path = scala_function "rm_tree" [path]; fun with_tmp_dir name f = let val path = create_tmp_path name "" in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; (* download file *) fun download url file = - ignore (Scala.function_thread "download" (cat_strings0 [url, absolute_path file])); + ignore (Scala.function "download" (cat_strings0 [url, absolute_path file])); end; diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,568 +1,568 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root(): Unit = { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ /* scala functions */ private def apply_paths(arg: String, fun: List[Path] => Unit): String = { fun(Library.split_strings0(arg).map(Path.explode)); "" } private def apply_paths1(arg: String, fun: Path => Unit): String = apply_paths(arg, { case List(path) => fun(path) }) private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.file.toPath) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } object Make_Directory extends Scala.Fun("make_directory") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, make_directory) } object Copy_Dir extends Scala.Fun("copy_dir") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed top copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun("copy_file") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_file) } object Copy_File_Base extends Scala.Fun("copy_file_base") { val here = Scala_Project.here def apply(arg: String): String = apply_paths3(arg, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun("rm_tree") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear() for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close() val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close() proc.getErrorStream.close() proc.destroy() Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def require_command(cmds: String*): Unit = { for (cmd <- cmds) { if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd)) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, file: Path, progress: Progress = new Progress): Unit = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) - val bytes = - try { Url.read_bytes(url) } + val content = + try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } - Bytes.write(file, bytes) + Bytes.write(file, content.bytes) } - object Download extends Scala.Fun("download") + object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here def apply(arg: String): String = Library.split_strings0(arg) match { case List(url, file) => download(url, Path.explode(file)); "" } } } diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,70 +1,66 @@ (* Title: Pure/System/scala.ML Author: Makarius Invoke Scala functions from the ML runtime. *) signature SCALA = sig exception Null val function: string -> string -> string - val function_thread: string -> string -> string end; structure Scala: SCALA = struct exception Null; local val new_id = string_of_int o Counter.make (); val results = Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table); val _ = Protocol_Command.define "Scala.result" (fn [id, tag, res] => let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail ("Bad tag: " ^ tag)); in Synchronized.change results (Symtab.map_entry id (K result)) end); -fun gen_function thread name arg = +in + +fun function name arg = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val id = new_id (); fun invoke () = (Synchronized.change results (Symtab.update (id, Exn.Exn Match)); - Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]); + Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]); fun cancel () = (Synchronized.change results (Symtab.delete_safe id); Output.protocol_message (Markup.cancel_scala id) []); fun await_result () = Synchronized.guarded_access results (fn tab => (case Symtab.lookup tab id of SOME (Exn.Exn Match) => NONE | SOME result => SOME (result, Symtab.delete id tab) | NONE => SOME (Exn.Exn Exn.Interrupt, tab))); in invoke (); Exn.release (restore_attributes await_result ()) handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) end) (); -in - -val function = gen_function false; -val function_thread = gen_function true; - end; end; diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,255 +1,263 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.io.{File => JFile, StringWriter, PrintWriter} import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.{IMain, Results} import scala.tools.nsc.interpreter.shell.ReplReporterImpl object Scala { /** registered functions **/ - abstract class Fun(val name: String) extends Function[String, String] + abstract class Fun(val name: String, val thread: Boolean = false) + extends Function[String, String] { override def toString: String = name def position: Properties.T = here.position def here: Scala_Project.Here def apply(arg: String): String } class Functions(val functions: Fun*) extends Isabelle_System.Service lazy val functions: List[Fun] = Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions) /** demo functions **/ object Echo extends Fun("echo") { val here = Scala_Project.here def apply(arg: String): String = arg } object Sleep extends Fun("sleep") { val here = Scala_Project.here def apply(seconds: String): String = { val t = seconds match { case Value.Double(s) => Time.seconds(s) case _ => error("Malformed argument: " + quote(seconds)) } val t0 = Time.now() t.sleep val t1 = Time.now() (t1 - t0).toString } } /** compiler **/ object Compiler { def context( error: String => Unit = Exn.error, jar_dirs: List[JFile] = Nil): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val class_path = for { prop <- List("isabelle.scala.classpath", "java.class.path") path = System.getProperty(prop, "") if path != "\"\"" elem <- space_explode(JFile.pathSeparatorChar, path) } yield elem val settings = new GenericRunnerSettings(error) settings.classpath.value = (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) new Context(settings) } def default_print_writer: PrintWriter = new NewLinePrintWriter(new ConsoleWriter, true) class Context private [Compiler](val settings: GenericRunnerSettings) { override def toString: String = settings.toString def interpreter( print_writer: PrintWriter = default_print_writer, class_loader: ClassLoader = null): IMain = { new IMain(settings, new ReplReporterImpl(settings, print_writer)) { override def parentClassLoader: ClassLoader = if (class_loader == null) super.parentClassLoader else class_loader } } def toplevel(interpret: Boolean, source: String): List[String] = { val out = new StringWriter val interp = interpreter(new PrintWriter(out)) val marker = '\u000b' val ok = interp.withLabel(marker.toString) { if (interpret) interp.interpret(source) == Results.Success else (new interp.ReadEvalPrint).compile(source) } out.close() val Error = """(?s)^\S* error: (.*)$""".r val errors = space_explode(marker, Library.strip_ansi_color(out.toString)). collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) if (!ok && errors.isEmpty) List("Error") else errors } } } object Toplevel extends Fun("scala_toplevel") { val here = Scala_Project.here def apply(arg: String): String = { val (interpret, source) = YXML.parse_body(arg) match { case Nil => (false, "") case List(XML.Text(source)) => (false, source) case body => import XML.Decode._; pair(bool, string)(body) } val errors = try { Compiler.context().toplevel(interpret, source) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } } /** invoke Scala functions from ML **/ /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } - def function(name: String, arg: String): (Tag.Value, String) = + def function_thread(name: String): Boolean = + functions.find(fun => fun.name == name) match { + case Some(fun) => fun.thread + case None => false + } + + def function_body(name: String, arg: String): (Tag.Value, String) = functions.find(fun => fun.name == name) match { case Some(fun) => Exn.capture { fun(arg) } match { case Exn.Res(null) => (Tag.NULL, "") case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) } case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name)) } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def result(id: String, tag: Scala.Tag.Value, res: String): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command("Scala.result", id, tag.id.toString, res) futures -= id } } private def cancel(id: String, future: Future[Unit]): Unit = { future.cancel() result(id, Scala.Tag.INTERRUPT, "") } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { - case Markup.Invoke_Scala(name, id, thread) => + case Markup.Invoke_Scala(name, id) => def body: Unit = { - val (tag, res) = Scala.function(name, msg.text) + val (tag, res) = Scala.function_body(name, msg.text) result(id, tag, res) } val future = - if (thread) { + if (Scala.function_thread(name)) { Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body) } else Future.fork(body) futures += (id -> future) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } override val functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } } class Scala_Functions extends Scala.Functions( Scala.Echo, Scala.Sleep, Scala.Toplevel, Doc.Doc_Names, Bash.Process, Bibtex.Check_Database, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, Isabelle_System.Copy_File, Isabelle_System.Copy_File_Base, Isabelle_System.Rm_Tree, Isabelle_System.Download, - Isabelle_Tool.Isabelle_Tools) + Isabelle_Tool.Isabelle_Tools, + isabelle.atp.SystemOnTPTP.List_Systems) diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,1084 +1,1084 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 18.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages_ubuntu_18_04: List[String] = Build_Docker.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-xml", "php-zip", "python-pygments", "ssh", "subversion", "python-pygments", // mercurial build packages "make", "gcc", "python", "python-dev", "python-docutils", "python-openssl") val packages_ubuntu_20_04: List[String] = packages_ubuntu_18_04.map( { case "python-pygments" => "python3-pygments" case "python-dev" => "python2-dev" case name => name }) def packages: List[String] = { val release = Linux.Release() if (release.is_ubuntu_18_04) packages_ubuntu_18_04 else if (release.is_ubuntu_20_04) packages_ubuntu_20_04 else error("Bad Linux version: expected Ubuntu 18.04 or 20.04 LTS") } /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config: Path = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port: Int = SSH.default_port val alternative_system_port = 222 val default_server_port = 2222 val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" /** global configuration **/ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) def global_config_script( init: String = "", body: String = "", exit: String = ""): String = { """#!/bin/bash """ + (if (init.nonEmpty) "\n" + init else "") + """ { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" { """ + Library.prefix_lines(" ", body) + """ } < /dev/null done } < """ + File.bash_path(global_config) + "\n" + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]): Unit = { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** administrative tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", Scala_Project.here, args => { var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } else { val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) if (!result.ok) error(result.print_return_code) } }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit = { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def command_setup(name: String, init: String = "", body: String = "", exit: String = ""): Path = { val command = Path.explode("/usr/local/bin") + Path.basic(name) File.write(command, global_config_script(init = init, body = body, exit = exit)) Isabelle_System.chmod("755", command) Isabelle_System.chown("root:root", command) command } def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = { progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...") Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => { val archive = if (Url.is_wellformed(mercurial_source)) { val archive = tmp_dir + Path.basic("mercurial.tar.gz") - Bytes.write(archive, Url.read_bytes(Url(mercurial_source))) + Isabelle_System.download(mercurial_source, archive) archive } else Path.explode(mercurial_source) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir)) progress.bash("make all && make install", cwd = build_dir.file, echo = true).check }) } def phabricator_setup( options: Options, name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, mercurial_source: String = "", progress: Progress = new Progress): Unit = { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() if (mercurial_source.nonEmpty) { for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } { error("Cannot install Mercurial from source:\n" + "package package " + quote(name) + " already installed") } mercurial_setup(mercurial_source, progress = progress) } /* users */ if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) || Set("", "ssh", "phd", "dump", daemon_user).contains(name)) { error("Bad installation name: " + quote(name)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path) Isabelle_System.chmod("755", root_path) progress.bash(cwd = root_path.file, echo = true, script = """ set -e echo "Cloning distribution repositories:" git clone --branch stable https://github.com/phacility/arcanist.git git -C arcanist reset --hard """ + Bash.string(options.string("phabricator_version_arcanist")) + """ git clone --branch stable https://github.com/phacility/phabricator.git git -C phabricator reset --hard """ + Bash.string(options.string("phabricator_version_phabricator")) + """ """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name)) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.chmod("440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex, which: String): String = { val conf = Path.explode("/etc/mysql/debian.cnf") split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match { case Some(res) => res case None => error("Cannot determine " + which + " from " + conf) } } val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name") val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password") val mysql_name = phabricator_name(name = name).replace("-", "_") val mysql_user_string = SQL.string(mysql_name) + "@'localhost'" val mysql_password = Linux.generate_password() Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) + " --password=" + Bash.string(mysql_root_password) + " --execute=" + Bash.string( """DROP USER IF EXISTS """ + mysql_user_string + "; " + """CREATE USER """ + mysql_user_string + """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ + """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") + """`.* TO """ + mysql_user_string + ";" + """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check config.execute("config set mysql.user " + Bash.string(mysql_name)) config.execute("config set mysql.pass " + Bash.string(mysql_password)) config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name)) config.execute("config set storage.default-namespace " + Bash.string(mysql_name)) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* database dump */ val dump_name = isabelle_phabricator_name(name = "dump") command_setup(dump_name, body = """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database" [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz" echo -n "Creating $ROOT/database/dump.sql.gz ..." "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """) /* Phabricator upgrade */ command_setup(isabelle_phabricator_name(name = "upgrade"), init = """BRANCH="${1:-stable}" if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ] then echo "Bad branch: \"$BRANCH\"" exit 1 fi systemctl stop isabelle-phabricator-phd systemctl stop apache2 """, body = """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..." for REPO in arcanist phabricator do cd "$ROOT/$REPO" echo -e "\nUpdating \"$REPO\" ..." git checkout "$BRANCH" git pull done echo -e "\nUpgrading storage ..." "$ROOT/phabricator/bin/storage" upgrade --force """, exit = """systemctl start apache2 systemctl start isabelle-phabricator-phd""") /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n" + "max_execution_time = 120\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log CustomLog ${APACHE_LOG_DIR}/access.log combined RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") progress.echo("\nFurther manual configuration via " + server_url) /* PHP daemon */ progress.echo("\nPHP daemon setup ...") val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd")) Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path) Isabelle_System.chmod("755", phd_log_path) config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") val phd_name = isabelle_phabricator_name(name = "phd") Linux.service_shutdown(phd_name) val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """) try { Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + phd_command.implode + """ start --force ExecStop=""" + phd_command.implode + """ stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) } catch { case ERROR(msg) => progress.bash("bin/phd status", cwd = config.home.file, echo = true).check error(msg) } } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", Scala_Project.here, args => { var mercurial_source = "" var repo = "" var package_update = false var name = default_name var options = Options.init() var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -M SOURCE install Mercurial from source: local PATH, or URL, or ":" for """ + standard_mercurial_source + """ -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)), "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "o:" -> (arg => options = options + arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup(options, name = name, root = root, repo = repo, package_update = package_update, mercurial_source = mercurial_source, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = new Progress): Unit = { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail: Unit = { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo("Please invoke the tool again, after providing details in\n " + default_config_file.implode + "\n") } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", Scala_Project.here, args => { var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(SSH.default_port) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, progress: Progress = new Progress): Unit = { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") val ssh_command = command_setup(ssh_name, body = """if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi""", exit = "exit 1") File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port") } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", Scala_Project.here, args => { var server_port = default_server_port var system_port = default_system_port val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) /** conduit API **/ object API { /* user information */ sealed case class User( id: Long, phid: String, name: String, real_name: String, roles: List[String]) { def is_valid: Boolean = roles.contains("verified") && roles.contains("approved") && roles.contains("activated") def is_admin: Boolean = roles.contains("admin") def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list")) } /* repository information */ sealed case class Repository( vcs: VCS.Value, id: Long, phid: String, name: String, callsign: String, short_name: String, importing: Boolean, ssh_url: String) { def is_hg: Boolean = vcs == VCS.hg } object VCS extends Enumeration { val hg, git, svn = Value def read(s: String): Value = try { withName(s) } catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] = List(JSON.Object("type" -> typ, "value" -> value)) def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = value.toList.flatMap(edits(typ, _)) /* result with optional error */ sealed case class Result(result: JSON.T, error: Option[String]) { def ok: Boolean = error.isEmpty def get: JSON.T = if (ok) result else Exn.error(error.get) def get_value[A](unapply: JSON.T => Option[A]): A = unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result)) def get_string: String = get_value(JSON.Value.String.unapply) } def make_result(json: JSON.T): Result = { val result = JSON.value(json, "result").getOrElse(JSON.Object.empty) val error_info = JSON.string(json, "error_info") val error_code = JSON.string(json, "error_code") Result(result, error_info orElse error_code) } /* context for operations */ def apply(user: String, host: String, port: Int = SSH.default_port): API = new API(user, host, port) } final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) { /* connection */ require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port") private def ssh_user_prefix: String = SSH.user_prefix(ssh_user) private def ssh_port_suffix: String = SSH.port_suffix(ssh_port) override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix /* execute methods */ def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = { Isabelle_System.with_tmp_file("params", "json")(params_file => { File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) }) } def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result = API.make_result(execute_raw(method, params = params)) def execute_search[A]( method: String, params: JSON.Object.T, unapply: JSON.T => Option[A]): List[A] = { val results = new mutable.ListBuffer[A] var after = "" do { val result = execute(method, params = params ++ JSON.optional("after" -> proper_string(after))) results ++= result.get_value(JSON.list(_, "data", unapply)) after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after"))) } while (after.nonEmpty) results.toList } def ping(): String = execute("conduit.ping").get_string /* users */ lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid")) lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName")) def get_users( all: Boolean = false, phid: String = "", name: String = ""): List[API.User] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("user.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "username") real_name <- JSON.string0(fields, "realName") roles <- JSON.strings(fields, "roles") } yield API.User(id, phid, name, real_name, roles))) } def the_user(phid: String): API.User = get_users(phid = phid) match { case List(user) => user case _ => error("Bad user PHID " + quote(phid)) } /* repositories */ def get_repositories( all: Boolean = false, phid: String = "", callsign: String = "", short_name: String = ""): List[API.Repository] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("diffusion.repository.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { vcs_name <- JSON.string(fields, "vcs") id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "name") callsign <- JSON.string0(fields, "callsign") short_name <- JSON.string0(fields, "shortName") importing <- JSON.bool(fields, "isImporting") } yield { val vcs = API.VCS.read(vcs_name) val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name val ssh_url = vcs match { case API.VCS.hg => hg_url + url_path case API.VCS.git => hg_url + url_path + ".git" case API.VCS.svn => "" } API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url) })) } def the_repository(phid: String): API.Repository = get_repositories(phid = phid) match { case List(repo) => repo case _ => error("Bad repository PHID " + quote(phid)) } def create_repository( name: String, callsign: String = "", // unique name, UPPERCASE short_name: String = "", // unique name description: String = "", public: Boolean = false, vcs: API.VCS.Value = API.VCS.hg): API.Repository = { require(name.nonEmpty, "bad repository name") val transactions = API.edits("vcs", vcs.toString) ::: API.edits("name", name) ::: API.opt_edits("callsign", proper_string(callsign)) ::: API.opt_edits("shortName", proper_string(short_name)) ::: API.opt_edits("description", proper_string(description)) ::: (if (public) Nil else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) ::: API.edits("status", "active") val phid = execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions)) .get_value(JSON.value(_, "object", JSON.string(_, "phid"))) execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get the_repository(phid) } } } diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala +++ b/src/Pure/Tools/scala_project.scala @@ -1,192 +1,193 @@ /* Title: Pure/Tools/scala_project.scala Author: Makarius Setup Gradle project for Isabelle/Scala/jEdit. */ package isabelle object Scala_Project { /* groovy syntax */ def groovy_string(s: String): String = { s.map(c => c match { case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c case _ => c.toString }).mkString("'", "", "'") } /* file and directories */ lazy val isabelle_files: List[String] = { val files1 = { val isabelle_home = Path.explode("~~").canonical Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")). map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode) } val files2 = (for { path <- List( Path.explode("~~/lib/classes/Pure.shasum"), Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum")) if path.is_file line <- Library.trim_split_lines(File.read(path)) name = if (line.length > 42 && line(41) == '*') line.substring(42) else error("Bad shasum entry: " + quote(line)) if name != "lib/classes/Pure.jar" && name != "src/Tools/jEdit/dist/jedit.jar" && name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit-base.jar" && name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" } yield name) files1 ::: files2 } lazy val isabelle_scala_files: Map[String, Path] = isabelle_files.foldLeft(Map.empty[String, Path]) { case (map, name) => if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) { val path = Path.explode("~~/" + name) val base = path.base.implode map.get(base) match { case None => map + (base -> path) case Some(path1) => error("Conflicting base names: " + path + " vs. " + path1) } } else map } val isabelle_dirs: List[(String, Path)] = List( "src/Pure/" -> Path.explode("isabelle"), "src/Tools/Graphview/" -> Path.explode("isabelle.graphview"), "src/Tools/VSCode/" -> Path.explode("isabelle.vscode"), "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"), "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"), "src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"), + "src/HOL/Tools/ATP" -> Path.explode("isabelle.atp"), "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick")) /* compile-time position */ def here: Here = { val exn = new Exception exn.getStackTrace.toList match { case _ :: caller :: _ => val name = proper_string(caller.getFileName).getOrElse("") val line = caller.getLineNumber new Here(name, line) case _ => new Here("", 0) } } class Here private[Scala_Project](name: String, line: Int) { override def toString: String = name + ":" + line def position: Position.T = isabelle_scala_files.get(name) match { case Some(path) => Position.Line_File(line, path.implode) case None => Position.none } } /* scala project */ def scala_project(project_dir: Path, symlinks: Boolean = false): Unit = { if (symlinks && Platform.is_windows) error("Cannot create symlinks on Windows") if (project_dir.is_file || project_dir.is_dir) error("Project directory already exists: " + project_dir) val src_dir = project_dir + Path.explode("src/main/scala") val java_src_dir = project_dir + Path.explode("src/main/java") val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala")) Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir) val files = isabelle_files isabelle_scala_files for (file <- files if file.endsWith(".scala")) { val (path, target) = isabelle_dirs.collectFirst({ case (prfx, p) if file.startsWith(prfx) => (Path.explode("~~") + Path.explode(file), scala_src_dir + p) }).getOrElse(error("Unknown directory prefix for " + quote(file))) Isabelle_System.make_directory(target) if (symlinks) Isabelle_System.symlink(path, target) else Isabelle_System.copy_file(path, target) } val jars = for (file <- files if file.endsWith(".jar")) yield { if (file.startsWith("/")) file else Isabelle_System.getenv("ISABELLE_HOME") + "/" + file } File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n") File.write(project_dir + Path.explode("build.gradle"), """plugins { id 'scala' } repositories { mavenCentral() } dependencies { implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """' compile files( """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") + """ } """) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit", Scala_Project.here, args => { var symlinks = false val getopts = Getopts(""" Usage: isabelle scala_project [OPTIONS] PROJECT_DIR Options are: -L make symlinks to original scala files Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs such as IntelliJ IDEA. """, "L" -> (_ => symlinks = true)) val more_args = getopts(args) val project_dir = more_args match { case List(dir) => Path.explode(dir) case _ => getopts.usage() } scala_project(project_dir, symlinks = symlinks) }) } diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,324 +1,325 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( src/HOL/SPARK/Tools/spark.scala + src/HOL/Tools/ATP/system_on_tptp.scala src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala src/Pure/Admin/build_cygwin.scala src/Pure/Admin/build_doc.scala src/Pure/Admin/build_e.scala src/Pure/Admin/build_fonts.scala src/Pure/Admin/build_history.scala src/Pure/Admin/build_jdk.scala src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala src/Pure/Admin/build_spass.scala src/Pure/Admin/build_sqlite.scala src/Pure/Admin/build_status.scala src/Pure/Admin/build_vampire.scala src/Pure/Admin/build_verit.scala src/Pure/Admin/build_zipperposition.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala src/Pure/Concurrent/mailbox.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/synchronized.scala src/Pure/GUI/color_value.scala src/Pure/GUI/desktop_app.scala src/Pure/GUI/gui.scala src/Pure/GUI/gui_thread.scala src/Pure/GUI/popup.scala src/Pure/GUI/wrap_panel.scala src/Pure/General/antiquote.scala src/Pure/General/bytes.scala src/Pure/General/cache.scala src/Pure/General/codepoint.scala src/Pure/General/comment.scala src/Pure/General/completion.scala src/Pure/General/csv.scala src/Pure/General/date.scala src/Pure/General/exn.scala src/Pure/General/file.scala src/Pure/General/file_watcher.scala src/Pure/General/graph.scala src/Pure/General/graph_display.scala src/Pure/General/graphics_file.scala src/Pure/General/http.scala src/Pure/General/json.scala src/Pure/General/linear_set.scala src/Pure/General/logger.scala src/Pure/General/long_name.scala src/Pure/General/mailman.scala src/Pure/General/mercurial.scala src/Pure/General/multi_map.scala src/Pure/General/output.scala src/Pure/General/path.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/General/properties.scala src/Pure/General/rdf.scala src/Pure/General/scan.scala src/Pure/General/sha1.scala src/Pure/General/sql.scala src/Pure/General/ssh.scala src/Pure/General/symbol.scala src/Pure/General/time.scala src/Pure/General/timing.scala src/Pure/General/untyped.scala src/Pure/General/url.scala src/Pure/General/utf8.scala src/Pure/General/uuid.scala src/Pure/General/value.scala src/Pure/General/word.scala src/Pure/General/xz.scala src/Pure/Isar/document_structure.scala src/Pure/Isar/keyword.scala src/Pure/Isar/line_structure.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.scala src/Pure/Isar/token.scala src/Pure/ML/ml_console.scala src/Pure/ML/ml_lex.scala src/Pure/ML/ml_process.scala src/Pure/ML/ml_statistics.scala src/Pure/ML/ml_syntax.scala src/Pure/PIDE/byte_message.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.scala src/Pure/PIDE/document_status.scala src/Pure/PIDE/editor.scala src/Pure/PIDE/headless.scala src/Pure/PIDE/line.scala src/Pure/PIDE/markup.scala src/Pure/PIDE/markup_tree.scala src/Pure/PIDE/protocol.scala src/Pure/PIDE/protocol_handlers.scala src/Pure/PIDE/protocol_message.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/query_operation.scala src/Pure/PIDE/rendering.scala src/Pure/PIDE/resources.scala src/Pure/PIDE/session.scala src/Pure/PIDE/text.scala src/Pure/PIDE/xml.scala src/Pure/PIDE/yxml.scala src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala src/Pure/System/cygwin.scala src/Pure/System/distribution.scala src/Pure/System/executable.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_platform.scala src/Pure/System/isabelle_process.scala src/Pure/System/isabelle_system.scala src/Pure/System/isabelle_tool.scala src/Pure/System/java_statistics.scala src/Pure/System/linux.scala src/Pure/System/mingw.scala src/Pure/System/numa.scala src/Pure/System/options.scala src/Pure/System/platform.scala src/Pure/System/posix_interrupt.scala src/Pure/System/process_result.scala src/Pure/System/progress.scala src/Pure/System/scala.scala src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala src/Pure/Thy/html.scala src/Pure/Thy/latex.scala src/Pure/Thy/presentation.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_element.scala src/Pure/Thy/thy_header.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/build_docker.scala src/Pure/Tools/build_job.scala src/Pure/Tools/check_keywords.scala src/Pure/Tools/debugger.scala src/Pure/Tools/doc.scala src/Pure/Tools/dump.scala src/Pure/Tools/fontforge.scala src/Pure/Tools/java_monitor.scala src/Pure/Tools/logo.scala src/Pure/Tools/main.scala src/Pure/Tools/mkroot.scala src/Pure/Tools/phabricator.scala src/Pure/Tools/print_operation.scala src/Pure/Tools/profiling_report.scala src/Pure/Tools/scala_project.scala src/Pure/Tools/server.scala src/Pure/Tools/server_commands.scala src/Pure/Tools/simplifier_trace.scala src/Pure/Tools/spell_checker.scala src/Pure/Tools/task_statistics.scala src/Pure/Tools/update.scala src/Pure/Tools/update_cartouches.scala src/Pure/Tools/update_comments.scala src/Pure/Tools/update_header.scala src/Pure/Tools/update_then.scala src/Pure/Tools/update_theorems.scala src/Pure/library.scala src/Pure/pure_thy.scala src/Pure/term.scala src/Pure/term_xml.scala src/Pure/thm_name.scala src/Tools/Graphview/graph_file.scala src/Tools/Graphview/graph_panel.scala src/Tools/Graphview/graphview.scala src/Tools/Graphview/layout.scala src/Tools/Graphview/main_panel.scala src/Tools/Graphview/metrics.scala src/Tools/Graphview/model.scala src/Tools/Graphview/mutator.scala src/Tools/Graphview/mutator_dialog.scala src/Tools/Graphview/mutator_event.scala src/Tools/Graphview/popups.scala src/Tools/Graphview/shapes.scala src/Tools/Graphview/tree_panel.scala src/Tools/VSCode/src/build_vscode.scala src/Tools/VSCode/src/channel.scala src/Tools/VSCode/src/dynamic_output.scala src/Tools/VSCode/src/language_server.scala src/Tools/VSCode/src/lsp.scala src/Tools/VSCode/src/preview_panel.scala src/Tools/VSCode/src/state_panel.scala src/Tools/VSCode/src/textmate_grammar.scala src/Tools/VSCode/src/vscode_model.scala src/Tools/VSCode/src/vscode_rendering.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/VSCode/src/vscode_spell_checker.scala ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## target TARGET_DIR="lib/classes" TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" function target_shasum() { shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null } function target_clean() { rm -rf "$TARGET_DIR" } [ -n "$FRESH" ] && target_clean ## build target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ "$?" -ne 0 ]; then echo "### Building Isabelle/Scala ..." target_clean BUILD_DIR="$TARGET_DIR/build" mkdir -p "$BUILD_DIR" ( export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ -d "$BUILD_DIR" "${SOURCES[@]}" ) || fail "Failed to compile sources" CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ -C "$BUILD_DIR" META-INF \ -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" rm -rf "$BUILD_DIR" target_shasum > "$TARGET_SHASUM" fi diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala +++ b/src/Tools/jEdit/src/document_model.scala @@ -1,700 +1,700 @@ /* Title: Tools/jEdit/src/document_model.scala Author: Fabian Immler, TU Munich Author: Makarius Document model connected to jEdit buffer or external file: content of theory node or auxiliary file (blob). */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import scala.collection.mutable import scala.annotation.tailrec import org.gjt.sp.jedit.View import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} object Document_Model { /* document models */ sealed case class State( models: Map[Document.Node.Name, Document_Model] = Map.empty, buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty, overlays: Document.Overlays = Document.Overlays.empty) { def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = for { (node_name, model) <- models.iterator if model.isInstanceOf[File_Model] } yield (node_name, model.asInstanceOf[File_Model]) def document_blobs: Document.Blobs = Document.Blobs( (for { (node_name, model) <- models.iterator blob <- model.get_blob } yield (node_name -> blob)).toMap) def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) : (Buffer_Model, State) = { val old_model = models.get(node_name) match { case Some(file_model: File_Model) => Some(file_model) case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) case _ => None } val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) (buffer_model, copy(models = models + (node_name -> buffer_model), buffer_models = buffer_models + (buffer -> buffer_model))) } def close_buffer(buffer: JEditBuffer): State = { buffer_models.get(buffer) match { case None => this case Some(buffer_model) => val file_model = buffer_model.exit() copy(models = models + (file_model.node_name -> file_model), buffer_models = buffer_models - buffer) } } def provide_file(session: Session, node_name: Document.Node.Name, text: String): State = if (models.isDefinedAt(node_name)) this else { val edit = Text.Edit.insert(0, text) val model = File_Model.init(session, node_name, text, pending_edits = List(edit)) copy(models = models + (node_name -> model)) } } private val state = Synchronized(State()) // owned by GUI thread def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name) def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) def document_blobs(): Document.Blobs = state.value.document_blobs /* bibtex */ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = Bibtex.entries_iterator(state.value.models) def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset) : Option[Completion.Result] = Bibtex.completion(history, rendering, caret, state.value.models) /* overlays */ def node_overlays(name: Document.Node.Name): Document.Node.Overlays = state.value.overlays(name) def insert_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args))) def remove_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args))) /* sync external files */ def sync_files(changed_files: Set[JFile]): Boolean = { state.change_result(st => { val changed_models = (for { (node_name, model) <- st.file_models_iterator file <- model.file if changed_files(file) text <- PIDE.resources.read_file_content(node_name) if model.content.text != text } yield { val content = Document_Model.File_Content(text) val edits = Text.Edit.replace(0, model.content.text, text) (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits)) }).toList if (changed_models.isEmpty) (false, st) else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _))) }) } /* syntax */ def syntax_changed(names: List[Document.Node.Name]): Unit = { GUI_Thread.require {} val models = state.value.models for (name <- names.iterator; model <- models.get(name)) { model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => } } } /* init and exit */ def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = { GUI_Thread.require {} state.change_result(st => st.buffer_models.get(buffer) match { case Some(buffer_model) if buffer_model.node_name == node_name => buffer_model.init_token_marker() (buffer_model, st) case _ => val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) buffer.propertiesChanged() res }) } def exit(buffer: Buffer): Unit = { GUI_Thread.require {} state.change(st => if (st.buffer_models.isDefinedAt(buffer)) { val res = st.close_buffer(buffer) buffer.propertiesChanged() res } else st) } def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit = { GUI_Thread.require {} state.change(st => files.foldLeft(st) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) }) } /* required nodes */ def required_nodes(): Set[Document.Node.Name] = (for { (node_name, model) <- state.value.models.iterator if model.node_required } yield node_name).toSet def node_required( name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit = { GUI_Thread.require {} val changed = state.change_result(st => st.models.get(name) match { case None => (false, st) case Some(model) => val required = if (toggle) !model.node_required else set model match { case model1: File_Model if required != model1.node_required => (true, st.copy(models = st.models + (name -> model1.copy(node_required = required)))) case model1: Buffer_Model if required != model1.node_required => model1.set_node_required(required); (true, st) case _ => (false, st) } }) if (changed) { PIDE.plugin.options_changed() PIDE.editor.flush() } } def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit = Document_Model.get(view.getBuffer).foreach(model => node_required(model.node_name, toggle = toggle, set = set)) /* flushed edits */ def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = { GUI_Thread.require {} state.change_result(st => { val doc_blobs = st.document_blobs val buffer_edits = (for { (_, model) <- st.buffer_models.iterator edit <- model.flush_edits(doc_blobs, hidden).iterator } yield edit).toList val file_edits = (for { (node_name, model) <- st.file_models_iterator (edits, model1) <- model.flush_edits(doc_blobs, hidden) } yield (edits, node_name -> model1)).toList val model_edits = buffer_edits ::: file_edits.flatMap(_._1) val purge_edits = if (purge) { val purged = (for ((node_name, model) <- st.file_models_iterator) yield (node_name -> model.purge_edits(doc_blobs))).toList val imports = { val open_nodes = (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList val touched_nodes = model_edits.map(_._1) val pending_nodes = for ((node_name, None) <- purged) yield node_name (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) } val retain = PIDE.resources.dependencies(imports).theories.toSet for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits) yield edit } else Nil val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1)) PIDE.plugin.file_watcher.purge( (for { (_, model) <- st1.file_models_iterator file <- model.file } yield file.getParentFile).toSet) ((doc_blobs, model_edits ::: purge_edits), st1) }) } /* file content */ sealed case class File_Content(text: String) { lazy val bytes: Bytes = Bytes(Symbol.encode(text)) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) lazy val bibtex_entries: List[Text.Info[String]] = try { Bibtex.entries(text) } catch { case ERROR(_) => Nil } } /* HTTP preview */ private val plain_text_prefix = "plain_text=" def open_preview(view: View, plain_text: Boolean): Unit = { Document_Model.get(view.getBuffer) match { case Some(model) => val name = model.node_name val url = PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" + (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) PIDE.editor.hyperlink_url(url).follow(view) case _ => } } def http_handlers(http_root: String): List[HTTP.Handler] = { val fonts_root = http_root + "/fonts" val preview_root = http_root + "/preview" val html = - HTTP.get(preview_root, arg => + HTTP.Handler.get(preview_root, arg => for { query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode) name = Library.perhaps_unprefix(plain_text_prefix, query) model <- get(PIDE.resources.node_name(name)) } yield { val snapshot = model.await_stable_snapshot() val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root)) val document = Presentation.html_document( PIDE.resources, snapshot, html_context, Presentation.elements2, plain_text = query.startsWith(plain_text_prefix)) HTTP.Response.html(document.content) }) List(HTTP.fonts(fonts_root), html) } } sealed abstract class Document_Model extends Document.Model { /* perspective */ def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil def node_perspective( doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) = { GUI_Thread.require {} if (Isabelle.continuous_checking && is_theory) { val snapshot = this.snapshot() val reparse = snapshot.node.load_commands_changed(doc_blobs) val perspective = if (hidden) Text.Perspective.empty else { val view_ranges = document_view_ranges(snapshot) val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node) Text.Perspective(view_ranges ::: load_ranges) } val overlays = PIDE.editor.node_overlays(node_name) (reparse, Document.Node.Perspective(node_required, perspective, overlays)) } else (false, Document.Node.no_perspective_text) } /* snapshot */ @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { PIDE.options.seconds("editor_output_delay").sleep await_stable_snapshot() } else snapshot } } object File_Model { def empty(session: Session): File_Model = File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""), false, Document.Node.no_perspective_text, Nil) def init(session: Session, node_name: Document.Node.Name, text: String, node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, pending_edits: List[Text.Edit] = Nil): File_Model = { val file = JEdit_Lib.check_file(node_name.node) file.foreach(PIDE.plugin.file_watcher.register_parent(_)) val content = Document_Model.File_Content(text) val node_required1 = node_required || File_Format.registry.is_theory(node_name) File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits) } } case class File_Model( session: Session, node_name: Document.Node.Name, file: Option[JFile], content: Document_Model.File_Content, node_required: Boolean, last_perspective: Document.Node.Perspective_Text, pending_edits: List[Text.Edit]) extends Document_Model { /* text */ def get_text(range: Text.Range): Option[String] = range.try_substring(content.text) /* header */ def node_header: Document.Node.Header = PIDE.resources.special_header(node_name) getOrElse PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false) /* content */ def node_position(offset: Text.Offset): Line.Node_Position = Line.Node_Position(node_name.node, Line.Position.zero.advance(content.text.substring(0, offset))) def get_blob: Option[Document.Blob] = if (is_theory) None else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) def bibtex_entries: List[Text.Info[String]] = if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil /* edits */ def update_text(text: String): Option[File_Model] = Text.Edit.replace(0, content.text, text) match { case Nil => None case edits => val content1 = Document_Model.File_Content(text) val pending_edits1 = pending_edits ::: edits Some(copy(content = content1, pending_edits = pending_edits1)) } def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean) : Option[(List[Document.Edit_Text], File_Model)] = { val (reparse, perspective) = node_perspective(doc_blobs, hidden) if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { val edits = node_edits(node_header, pending_edits, perspective) Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) } else None } def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] = if (pending_edits.nonEmpty || !File_Format.registry.is_theory(node_name) && (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None else { val text_edits = List(Text.Edit.remove(0, content.text)) Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text)) } /* snapshot */ def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) } case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) extends Document_Model { /* text */ def get_text(range: Text.Range): Option[String] = JEdit_Lib.get_text(buffer, range) /* header */ def node_header(): Document.Node.Header = { GUI_Thread.require {} PIDE.resources.special_header(node_name) getOrElse JEdit_Lib.buffer_lock(buffer) { PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false) } } /* perspective */ // owned by GUI thread private var _node_required = false def node_required: Boolean = _node_required def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b } def document_view_iterator: Iterator[Document_View] = for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) } yield doc_view override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = { GUI_Thread.require {} (for { doc_view <- document_view_iterator range <- doc_view.perspective(snapshot).ranges.iterator } yield range).toList } /* blob */ // owned by GUI thread private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None private def reset_blob(): Unit = GUI_Thread.require { _blob = None } def get_blob: Option[Document.Blob] = GUI_Thread.require { if (is_theory) None else { val (bytes, text, chunk) = _blob match { case Some(x) => x case None => val bytes = PIDE.resources.make_file_content(buffer) val text = buffer.getText(0, buffer.getLength) val chunk = Symbol.Text_Chunk(text) val x = (bytes, text, chunk) _blob = Some(x) x } val changed = pending_edits.nonEmpty Some(Document.Blob(bytes, text, chunk, changed)) } } /* bibtex entries */ // owned by GUI thread private var _bibtex_entries: Option[List[Text.Info[String]]] = None private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } def bibtex_entries: List[Text.Info[String]] = GUI_Thread.require { if (Bibtex.is_bibtex(node_name.node)) { _bibtex_entries match { case Some(entries) => entries case None => val text = JEdit_Lib.buffer_text(buffer) val entries = try { Bibtex.entries(text) } catch { case ERROR(msg) => Output.warning(msg); Nil } _bibtex_entries = Some(entries) entries } } else Nil } /* pending edits */ private object pending_edits { private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = Document.Node.no_perspective_text def nonEmpty: Boolean = synchronized { pending.nonEmpty } def get_edits: List[Text.Edit] = synchronized { pending.toList } def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective } def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit = synchronized { last_perspective = perspective } def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = synchronized { GUI_Thread.require {} val edits = get_edits val (reparse, perspective) = node_perspective(doc_blobs, hidden) if (reparse || edits.nonEmpty || last_perspective != perspective) { pending.clear() last_perspective = perspective node_edits(node_header(), edits, perspective) } else Nil } def edit(edits: List[Text.Edit]): Unit = synchronized { GUI_Thread.require {} reset_blob() reset_bibtex_entries() for (doc_view <- document_view_iterator) doc_view.rich_text_area.active_reset() pending ++= edits PIDE.editor.invoke() } } def is_stable: Boolean = !pending_edits.nonEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = pending_edits.flush_edits(doc_blobs, hidden) /* buffer listener */ private val buffer_listener: BufferListener = new BufferAdapter { override def contentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int): Unit = { pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit = { pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) } } /* syntax */ def syntax_changed(): Unit = { JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). invoke(text_area) buffer.invalidateCachedFoldLevels() } def init_token_marker(): Unit = { Isabelle.buffer_token_marker(buffer) match { case Some(marker) if marker != buffer.getTokenMarker => buffer.setTokenMarker(marker) syntax_changed() case _ => } } /* init */ def init(old_model: Option[File_Model]): Buffer_Model = { GUI_Thread.require {} old_model match { case None => pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) case Some(file_model) => set_node_required(file_model.node_required) pending_edits.set_last_perspective(file_model.last_perspective) pending_edits.edit( file_model.pending_edits ::: Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) } buffer.addBufferListener(buffer_listener) init_token_marker() this } /* exit */ def exit(): File_Model = { GUI_Thread.require {} buffer.removeBufferListener(buffer_listener) init_token_marker() File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required, pending_edits.get_last_perspective, pending_edits.get_edits) } }