author | wenzelm |
Fri, 25 Nov 2022 14:44:22 +0100 | |
changeset 76530 | 2bf13b30b98e |
parent 76528 | bf537a75e872 |
child 77553 | 570f65953173 |
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 |
75906
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75644
diff
changeset
|
17 |
try { file.isFile && file.canRead && file.canExecute && !File.is_backup(name) } |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
18 |
catch { case _: SecurityException => false } |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
19 |
} |
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 |
private def find_external(name: String): Option[List[String] => Unit] = |
75394 | 22 |
dirs().collectFirst( |
23 |
{ |
|
24 |
case dir if is_external(dir, name) => |
|
25 |
{ (args: List[String]) => |
|
26 |
val tool = dir + Path.explode(name) |
|
27 |
val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) |
|
28 |
sys.exit(result.print_stdout.rc) |
|
29 |
} |
|
30 |
}) |
|
62830 | 31 |
|
32 |
||
33 |
/* internal tools */ |
|
34 |
||
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
35 |
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
|
36 |
Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) |
62830 | 37 |
|
38 |
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
|
39 |
internal_tools.collectFirst({ |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
40 |
case tool if tool.name == name => |
71632 | 41 |
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
|
42 |
}) |
62831 | 43 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
44 |
|
72763 | 45 |
/* list tools */ |
46 |
||
75393 | 47 |
abstract class Entry { |
72763 | 48 |
def name: String |
49 |
def position: Properties.T |
|
50 |
def description: String |
|
51 |
def print: String = |
|
52 |
description match { |
|
53 |
case "" => name |
|
54 |
case descr => name + " - " + descr |
|
55 |
} |
|
56 |
} |
|
57 |
||
75393 | 58 |
sealed case class External(name: String, path: Path) extends Entry { |
72763 | 59 |
def position: Properties.T = Position.File(path.absolute.implode) |
75393 | 60 |
def description: String = { |
72763 | 61 |
val Pattern = """.*\bDESCRIPTION: *(.*)""".r |
62 |
split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse "" |
|
63 |
} |
|
64 |
} |
|
65 |
||
75393 | 66 |
def external_tools(): List[External] = { |
72763 | 67 |
for { |
68 |
dir <- dirs() if dir.is_dir |
|
75642
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
69 |
name <- File.read_dir(dir) if is_external(dir, name) |
bb048086468a
discontinued Isabelle tools implemented as .scala scripts;
wenzelm
parents:
75628
diff
changeset
|
70 |
} yield External(name, dir + Path.explode(name)) |
72763 | 71 |
} |
72 |
||
73 |
def isabelle_tools(): List[Entry] = |
|
74 |
(external_tools() ::: internal_tools).sortBy(_.name) |
|
75 |
||
75393 | 76 |
object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") { |
72763 | 77 |
val here = Scala_Project.here |
78 |
def apply(arg: String): String = |
|
79 |
if (arg.nonEmpty) error("Bad argument: " + quote(arg)) |
|
80 |
else { |
|
81 |
val result = isabelle_tools().map(entry => (entry.name, entry.position)) |
|
82 |
val body = { import XML.Encode._; list(pair(string, properties))(result) } |
|
83 |
YXML.string_of_body(body) |
|
84 |
} |
|
85 |
} |
|
86 |
||
87 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
88 |
/* command line entry point */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
89 |
|
75393 | 90 |
def main(args: Array[String]): Unit = { |
71632 | 91 |
Command_Line.tool { |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
92 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
93 |
case Nil | List("-?") => |
72763 | 94 |
val tool_descriptions = isabelle_tools().map(_.print) |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
95 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
96 |
Usage: isabelle TOOL [ARGS ...] |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
97 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
98 |
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
|
99 |
|
73367 | 100 |
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
|
101 |
case tool_name :: tool_args => |
62830 | 102 |
find_external(tool_name) orElse find_internal(tool_name) match { |
103 |
case Some(tool) => tool(tool_args) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
104 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
105 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
106 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
107 |
} |
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 |
} |
62830 | 110 |
|
72763 | 111 |
sealed case class Isabelle_Tool( |
112 |
name: String, |
|
113 |
description: String, |
|
114 |
here: Scala_Project.Here, |
|
75393 | 115 |
body: List[String] => Unit |
116 |
) extends Isabelle_Tool.Entry { |
|
72763 | 117 |
def position: Position.T = here.position |
118 |
} |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
119 |
|
71736 | 120 |
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
|
121 |
|
69810 | 122 |
class Tools extends Isabelle_Scala_Tools( |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
123 |
Build.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
124 |
Build_Docker.isabelle_tool, |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72767
diff
changeset
|
125 |
Build_Job.isabelle_tool, |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
76075
diff
changeset
|
126 |
CI_Build.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
127 |
Doc.isabelle_tool, |
73718 | 128 |
Document_Build.isabelle_tool, |
76480 | 129 |
Dotnet_Setup.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
130 |
Dump.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
131 |
Export.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
132 |
ML_Process.isabelle_tool, |
75474 | 133 |
Mercurial.isabelle_tool1, |
134 |
Mercurial.isabelle_tool2, |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
135 |
Mkroot.isabelle_tool, |
73399 | 136 |
Logo.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
137 |
Options.isabelle_tool, |
70967 | 138 |
Phabricator.isabelle_tool1, |
139 |
Phabricator.isabelle_tool2, |
|
71097 | 140 |
Phabricator.isabelle_tool3, |
71109
8c1c717a830b
configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents:
71097
diff
changeset
|
141 |
Phabricator.isabelle_tool4, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
142 |
Profiling_Report.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
143 |
Server.isabelle_tool, |
71808 | 144 |
Sessions.isabelle_tool, |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71312
diff
changeset
|
145 |
Scala_Project.isabelle_tool, |
75555
197a5b3a1ea2
promote "isabelle sync" to regular user-space tool, with proper documentation;
wenzelm
parents:
75549
diff
changeset
|
146 |
Sync.isabelle_tool, |
69557 | 147 |
Update.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
148 |
Update_Cartouches.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
149 |
Update_Comments.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
150 |
Update_Header.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
151 |
Update_Then.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
152 |
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
|
153 |
isabelle.mirabelle.Mirabelle.isabelle_tool, |
75562 | 154 |
isabelle.vscode.Language_Server.isabelle_tool, |
155 |
isabelle.vscode.VSCode_Main.isabelle_tool) |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
156 |
|
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
157 |
class Admin_Tools extends Isabelle_Scala_Tools( |
72414
af24c0dd6975
build Isabelle CSDP component from official downloads;
wenzelm
parents:
72411
diff
changeset
|
158 |
Build_CSDP.isabelle_tool, |
76017 | 159 |
Build_CVC5.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
160 |
Build_Cygwin.isabelle_tool, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
161 |
Build_Doc.isabelle_tool, |
72363
fc5f10691147
build Isabelle E prover component from official downloads;
wenzelm
parents:
72346
diff
changeset
|
162 |
Build_E.isabelle_tool, |
76396 | 163 |
Build_Easychair.isabelle_tool, |
76478 | 164 |
Build_EPTCS.isabelle_tool, |
76399 | 165 |
Build_Foiltex.isabelle_tool, |
69339 | 166 |
Build_Fonts.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
167 |
Build_JDK.isabelle_tool, |
73653
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents:
73565
diff
changeset
|
168 |
Build_JEdit.isabelle_tool, |
76395
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76348
diff
changeset
|
169 |
Build_LIPIcs.isabelle_tool, |
76443 | 170 |
Build_LLNCS.isabelle_tool, |
74482
bd5998580edb
build minisat, using recent fork from original sources;
wenzelm
parents:
73718
diff
changeset
|
171 |
Build_Minisat.isabelle_tool, |
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75083
diff
changeset
|
172 |
Build_PDFjs.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
173 |
Build_PolyML.isabelle_tool1, |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
174 |
Build_PolyML.isabelle_tool2, |
76075
2e7211754ef1
tool to build Isabelle component for PostgreSQL JDBC;
wenzelm
parents:
76017
diff
changeset
|
175 |
Build_PostgreSQL.isabelle_tool, |
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
76480
diff
changeset
|
176 |
Build_Prismjs.isabelle_tool, |
72411
b8cc129ece05
build Isabelle SPASS component from unofficial download;
wenzelm
parents:
72363
diff
changeset
|
177 |
Build_SPASS.isabelle_tool, |
72346
93e533198bf6
build Isabelle sqlite-jdbc component from official download;
wenzelm
parents:
72159
diff
changeset
|
178 |
Build_SQLite.isabelle_tool, |
75377
4ce7d95612cb
build Isabelle Scala component from official downloads (for scala-3.1.1);
wenzelm
parents:
75292
diff
changeset
|
179 |
Build_Scala.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
180 |
Build_Status.isabelle_tool, |
72886
ac64b753a65f
build Isabelle Vampire component from repository;
wenzelm
parents:
72858
diff
changeset
|
181 |
Build_Vampire.isabelle_tool, |
72439
7f6800b2e8c2
build Isabelle veriT component from official download;
wenzelm
parents:
72414
diff
changeset
|
182 |
Build_VeriT.isabelle_tool, |
72466
04403e1ef176
build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
72439
diff
changeset
|
183 |
Build_Zipperposition.isabelle_tool, |
76348 | 184 |
Build_Zstd.isabelle_tool, |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69168
diff
changeset
|
185 |
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
|
186 |
Components.isabelle_tool, |
75083 | 187 |
isabelle.vscode.Build_VSCode.isabelle_tool, |
75249
8142e75320f6
patch VSCode source tree to support isabelle_encoding.ts;
wenzelm
parents:
75247
diff
changeset
|
188 |
isabelle.vscode.Build_VSCodium.isabelle_tool1, |
75562 | 189 |
isabelle.vscode.Build_VSCodium.isabelle_tool2) |