author | wenzelm |
Fri, 01 Jul 2022 19:58:38 +0200 | |
changeset 75644 | 3fad59705ab7 |
parent 75642 | bb048086468a |
child 75906 | 2167b9e3157a |
permissions | -rw-r--r-- |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/System/isabelle_tool.scala |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
3 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle system tools: external executables or internal Scala functions. |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
6 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
8 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
9 |
|
75393 | 10 |
object Isabelle_Tool { |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
11 |
/* external tools */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
12 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
13 |
private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
14 |
|
75642
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
15 |
private def is_external(dir: Path, name: String): Boolean = { |
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
16 |
val file = (dir + Path.explode(name)).file |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
17 |
try { |
75642
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
18 |
file.isFile && file.canRead && file.canExecute && |
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
19 |
!name.endsWith("~") && !name.endsWith(".orig") |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
20 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
21 |
catch { case _: SecurityException => false } |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
22 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
23 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
24 |
private def find_external(name: String): Option[List[String] => Unit] = |
75394 | 25 |
dirs().collectFirst( |
26 |
{ |
|
27 |
case dir if is_external(dir, name) => |
|
28 |
{ (args: List[String]) => |
|
29 |
val tool = dir + Path.explode(name) |
|
30 |
val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) |
|
31 |
sys.exit(result.print_stdout.rc) |
|
32 |
} |
|
33 |
}) |
|
62830 | 34 |
|
35 |
||
36 |
/* internal tools */ |
|
37 |
||
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
38 |
private lazy val internal_tools: List[Isabelle_Tool] = |
72159
40b5ee5889d2
clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents:
71808
diff
changeset
|
39 |
Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) |
62830 | 40 |
|
41 |
private def find_internal(name: String): Option[List[String] => Unit] = |
|
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
42 |
internal_tools.collectFirst({ |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
43 |
case tool if tool.name == name => |
71632 | 44 |
args => Command_Line.tool { tool.body(args) } |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
45 |
}) |
62831 | 46 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
47 |
|
72763 | 48 |
/* list tools */ |
49 |
||
75393 | 50 |
abstract class Entry { |
72763 | 51 |
def name: String |
52 |
def position: Properties.T |
|
53 |
def description: String |
|
54 |
def print: String = |
|
55 |
description match { |
|
56 |
case "" => name |
|
57 |
case descr => name + " - " + descr |
|
58 |
} |
|
59 |
} |
|
60 |
||
75393 | 61 |
sealed case class External(name: String, path: Path) extends Entry { |
72763 | 62 |
def position: Properties.T = Position.File(path.absolute.implode) |
75393 | 63 |
def description: String = { |
72763 | 64 |
val Pattern = """.*\bDESCRIPTION: *(.*)""".r |
65 |
split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse "" |
|
66 |
} |
|
67 |
} |
|
68 |
||
75393 | 69 |
def external_tools(): List[External] = { |
72763 | 70 |
for { |
71 |
dir <- dirs() if dir.is_dir |
|
75642
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
72 |
name <- File.read_dir(dir) if is_external(dir, name) |
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
73 |
} yield External(name, dir + Path.explode(name)) |
72763 | 74 |
} |
75 |
||
76 |
def isabelle_tools(): List[Entry] = |
|
77 |
(external_tools() ::: internal_tools).sortBy(_.name) |
|
78 |
||
75393 | 79 |
object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") { |
72763 | 80 |
val here = Scala_Project.here |
81 |
def apply(arg: String): String = |
|
82 |
if (arg.nonEmpty) error("Bad argument: " + quote(arg)) |
|
83 |
else { |
|
84 |
val result = isabelle_tools().map(entry => (entry.name, entry.position)) |
|
85 |
val body = { import XML.Encode._; list(pair(string, properties))(result) } |
|
86 |
YXML.string_of_body(body) |
|
87 |
} |
|
88 |
} |
|
89 |
||
90 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
91 |
/* command line entry point */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
92 |
|
75393 | 93 |
def main(args: Array[String]): Unit = { |
71632 | 94 |
Command_Line.tool { |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
95 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
96 |
case Nil | List("-?") => |
72763 | 97 |
val tool_descriptions = isabelle_tools().map(_.print) |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
98 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
99 |
Usage: isabelle TOOL [ARGS ...] |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
100 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
101 |
Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
102 |
|
73367 | 103 |
Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage() |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
104 |
case tool_name :: tool_args => |
62830 | 105 |
find_external(tool_name) orElse find_internal(tool_name) match { |
106 |
case Some(tool) => tool(tool_args) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
107 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
108 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
109 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
110 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
111 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
112 |
} |
62830 | 113 |
|
72763 | 114 |
sealed case class Isabelle_Tool( |
115 |
name: String, |
|
116 |
description: String, |
|
117 |
here: Scala_Project.Here, |
|
75393 | 118 |
body: List[String] => Unit |
119 |
) extends Isabelle_Tool.Entry { |
|
72763 | 120 |
def position: Position.T = here.position |
121 |
} |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
122 |
|
71736 | 123 |
class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
124 |
|
69810 | 125 |
class Tools extends Isabelle_Scala_Tools( |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
126 |
Build.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
127 |
Build_Docker.isabelle_tool, |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72767
diff
changeset
|
128 |
Build_Job.isabelle_tool, |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75562
diff
changeset
|
129 |
CI_Build_Benchmark.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
130 |
Doc.isabelle_tool, |
73718 | 131 |
Document_Build.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
132 |
Dump.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
133 |
Export.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
134 |
ML_Process.isabelle_tool, |
75474 | 135 |
Mercurial.isabelle_tool1, |
136 |
Mercurial.isabelle_tool2, |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
137 |
Mkroot.isabelle_tool, |
73399 | 138 |
Logo.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
139 |
Options.isabelle_tool, |
70967 | 140 |
Phabricator.isabelle_tool1, |
141 |
Phabricator.isabelle_tool2, |
|
71097 | 142 |
Phabricator.isabelle_tool3, |
71109
8c1c717a830b
configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents:
71097
diff
changeset
|
143 |
Phabricator.isabelle_tool4, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
144 |
Profiling_Report.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
145 |
Server.isabelle_tool, |
71808 | 146 |
Sessions.isabelle_tool, |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71312
diff
changeset
|
147 |
Scala_Project.isabelle_tool, |
75555
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75549
diff
changeset
|
148 |
Sync.isabelle_tool, |
69557 | 149 |
Update.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
150 |
Update_Cartouches.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
151 |
Update_Comments.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
152 |
Update_Header.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
153 |
Update_Then.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
154 |
Update_Theorems.isabelle_tool, |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73653
diff
changeset
|
155 |
isabelle.mirabelle.Mirabelle.isabelle_tool, |
75562 | 156 |
isabelle.vscode.Language_Server.isabelle_tool, |
157 |
isabelle.vscode.VSCode_Main.isabelle_tool) |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
158 |
|
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
159 |
class Admin_Tools extends Isabelle_Scala_Tools( |
72414
af24c0dd6975
build Isabelle CSDP component from official downloads;
wenzelm
parents:
72411
diff
changeset
|
160 |
Build_CSDP.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
161 |
Build_Cygwin.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
162 |
Build_Doc.isabelle_tool, |
72363
fc5f10691147
build Isabelle E prover component from official downloads;
wenzelm
parents:
72346
diff
changeset
|
163 |
Build_E.isabelle_tool, |
69339 | 164 |
Build_Fonts.isabelle_tool, |
73476
6b480efe1bc3
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
wenzelm
parents:
73399
diff
changeset
|
165 |
Build_JCEF.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
166 |
Build_JDK.isabelle_tool, |
73653
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents:
73565
diff
changeset
|
167 |
Build_JEdit.isabelle_tool, |
74482
bd5998580edb
build minisat, using recent fork from original sources;
wenzelm
parents:
73718
diff
changeset
|
168 |
Build_Minisat.isabelle_tool, |
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75083
diff
changeset
|
169 |
Build_PDFjs.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
170 |
Build_PolyML.isabelle_tool1, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
171 |
Build_PolyML.isabelle_tool2, |
72411
b8cc129ece05
build Isabelle SPASS component from unofficial download;
wenzelm
parents:
72363
diff
changeset
|
172 |
Build_SPASS.isabelle_tool, |
72346
93e533198bf6
build Isabelle sqlite-jdbc component from official download;
wenzelm
parents:
72159
diff
changeset
|
173 |
Build_SQLite.isabelle_tool, |
75377
4ce7d95612cb
build Isabelle Scala component from official downloads (for scala-3.1.1);
wenzelm
parents:
75292
diff
changeset
|
174 |
Build_Scala.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
175 |
Build_Status.isabelle_tool, |
72886
ac64b753a65f
build Isabelle Vampire component from repository;
wenzelm
parents:
72858
diff
changeset
|
176 |
Build_Vampire.isabelle_tool, |
72439
7f6800b2e8c2
build Isabelle veriT component from official download;
wenzelm
parents:
72414
diff
changeset
|
177 |
Build_VeriT.isabelle_tool, |
72466
04403e1ef176
build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
72439
diff
changeset
|
178 |
Build_Zipperposition.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
179 |
Check_Sources.isabelle_tool, |
69429
dc5fbcb07c7b
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents:
69401
diff
changeset
|
180 |
Components.isabelle_tool, |
75083 | 181 |
isabelle.vscode.Build_VSCode.isabelle_tool, |
75249
8142e75320f6
patch VSCode source tree to support isabelle_encoding.ts;
wenzelm
parents:
75247
diff
changeset
|
182 |
isabelle.vscode.Build_VSCodium.isabelle_tool1, |
75562 | 183 |
isabelle.vscode.Build_VSCodium.isabelle_tool2) |