1 /* Title: Pure/Admin/other_isabelle.scala |
|
2 Author: Makarius |
|
3 |
|
4 Manage other Isabelle distributions: support historic versions starting from |
|
5 tag "build_history_base". |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 object Other_Isabelle { |
|
12 def apply( |
|
13 root: Path, |
|
14 isabelle_identifier: String = "", |
|
15 ssh: SSH.System = SSH.Local, |
|
16 progress: Progress = new Progress |
|
17 ): Other_Isabelle = { |
|
18 val (isabelle_home, url_prefix) = |
|
19 ssh match { |
|
20 case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) |
|
21 case _ => |
|
22 if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { |
|
23 error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") |
|
24 } |
|
25 (root.canonical, "") |
|
26 } |
|
27 val isabelle_home_url = url_prefix + isabelle_home.implode |
|
28 new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) |
|
29 } |
|
30 } |
|
31 |
|
32 final class Other_Isabelle private( |
|
33 val isabelle_home: Path, |
|
34 val isabelle_identifier: String, |
|
35 isabelle_home_url: String, |
|
36 ssh: SSH.System, |
|
37 progress: Progress |
|
38 ) { |
|
39 override def toString: String = isabelle_home_url |
|
40 |
|
41 |
|
42 /* static system */ |
|
43 |
|
44 def bash( |
|
45 script: String, |
|
46 redirect: Boolean = false, |
|
47 echo: Boolean = false, |
|
48 strict: Boolean = true |
|
49 ): Process_Result = { |
|
50 ssh.execute( |
|
51 Isabelle_System.export_isabelle_identifier(isabelle_identifier) + |
|
52 "cd " + ssh.bash_path(isabelle_home) + "\n" + script, |
|
53 progress_stdout = progress.echo_if(echo, _), |
|
54 progress_stderr = progress.echo_if(echo, _), |
|
55 redirect = redirect, |
|
56 settings = false, |
|
57 strict = strict) |
|
58 } |
|
59 |
|
60 def getenv(name: String): String = |
|
61 bash("bin/isabelle getenv -b " + Bash.string(name)).check.out |
|
62 |
|
63 val settings: Isabelle_System.Settings = (name: String) => getenv(name) |
|
64 |
|
65 def expand_path(path: Path): Path = path.expand_env(settings) |
|
66 def bash_path(path: Path): String = Bash.string(expand_path(path).implode) |
|
67 |
|
68 val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER")) |
|
69 |
|
70 def etc: Path = isabelle_home_user + Path.explode("etc") |
|
71 def etc_settings: Path = etc + Path.explode("settings") |
|
72 def etc_preferences: Path = etc + Path.explode("preferences") |
|
73 |
|
74 |
|
75 /* components */ |
|
76 |
|
77 def init_components( |
|
78 components_base: String = Components.dynamic_components_base, |
|
79 catalogs: List[String] = Components.default_catalogs, |
|
80 components: List[String] = Nil |
|
81 ): List[String] = { |
|
82 val admin = Components.admin(Path.ISABELLE_HOME).implode |
|
83 |
|
84 catalogs.map(name => |
|
85 "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: |
|
86 components.map(name => |
|
87 "init_component " + quote(components_base) + "/" + name) |
|
88 } |
|
89 |
|
90 def resolve_components( |
|
91 echo: Boolean = false, |
|
92 clean_platforms: Option[List[Platform.Family.Value]] = None, |
|
93 clean_archives: Boolean = false, |
|
94 component_repository: String = Components.static_component_repository |
|
95 ): Unit = { |
|
96 val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) |
|
97 for (path <- missing) { |
|
98 Components.resolve(path.dir, path.file_name, |
|
99 clean_platforms = clean_platforms, |
|
100 clean_archives = clean_archives, |
|
101 component_repository = component_repository, |
|
102 ssh = ssh, |
|
103 progress = if (echo) progress else new Progress) |
|
104 } |
|
105 } |
|
106 |
|
107 def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { |
|
108 if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) |
|
109 |
|
110 val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") |
|
111 val dummy_stty_remote = expand_path(dummy_stty) |
|
112 if (!ssh.is_file(dummy_stty_remote)) { |
|
113 ssh.make_directory(dummy_stty_remote.dir) |
|
114 ssh.write_file(dummy_stty_remote, dummy_stty) |
|
115 ssh.set_executable(dummy_stty_remote) |
|
116 } |
|
117 try { |
|
118 bash( |
|
119 "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" + |
|
120 "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" + |
|
121 "bin/isabelle jedit -b", echo = echo).check |
|
122 } |
|
123 catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) } |
|
124 } |
|
125 |
|
126 |
|
127 /* settings */ |
|
128 |
|
129 def clean_settings(): Boolean = |
|
130 if (!ssh.is_file(etc_settings)) true |
|
131 else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { |
|
132 ssh.delete(etc_settings) |
|
133 true |
|
134 } |
|
135 else false |
|
136 |
|
137 def init_settings(settings: List[String]): Unit = { |
|
138 if (clean_settings()) { |
|
139 ssh.make_directory(etc_settings.dir) |
|
140 ssh.write(etc_settings, |
|
141 "# generated by Isabelle " + Date.now() + "\n" + |
|
142 "#-*- shell-script -*- :mode=shellscript:\n" + |
|
143 settings.mkString("\n", "\n", "\n")) |
|
144 } |
|
145 else error("Cannot proceed with existing user settings file: " + etc_settings) |
|
146 } |
|
147 |
|
148 |
|
149 /* init */ |
|
150 |
|
151 def init( |
|
152 other_settings: List[String] = init_components(), |
|
153 fresh: Boolean = false, |
|
154 echo: Boolean = false, |
|
155 clean_platforms: Option[List[Platform.Family.Value]] = None, |
|
156 clean_archives: Boolean = false, |
|
157 component_repository: String = Components.static_component_repository |
|
158 ): Unit = { |
|
159 init_settings(other_settings) |
|
160 resolve_components( |
|
161 echo = echo, |
|
162 clean_platforms = clean_platforms, |
|
163 clean_archives = clean_archives, |
|
164 component_repository = component_repository) |
|
165 scala_build(fresh = fresh, echo = echo) |
|
166 } |
|
167 |
|
168 |
|
169 /* cleanup */ |
|
170 |
|
171 def cleanup(): Unit = { |
|
172 clean_settings() |
|
173 ssh.delete(etc) |
|
174 ssh.delete(isabelle_home_user) |
|
175 } |
|
176 } |
|