author | wenzelm |
Tue, 04 May 2021 20:02:08 +0200 | |
changeset 73625 | f8f065e20837 |
parent 73522 | b219774a71ae |
child 73987 | fc363a3b690a |
permissions | -rw-r--r-- |
64188 | 1 |
/* Title: Pure/Admin/other_isabelle.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Manage other Isabelle distributions. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67045 | 10 |
object Other_Isabelle |
11 |
{ |
|
12 |
def apply(isabelle_home: Path, |
|
67046 | 13 |
isabelle_identifier: String = "", |
73522 | 14 |
user_home: Path = Path.USER_HOME, |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
15 |
progress: Progress = new Progress): Other_Isabelle = |
69408
fb26935838c7
more robust, notably for macos /var vs. /private/var;
wenzelm
parents:
69404
diff
changeset
|
16 |
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress) |
67045 | 17 |
} |
18 |
||
19 |
class Other_Isabelle( |
|
20 |
val isabelle_home: Path, |
|
21 |
val isabelle_identifier: String, |
|
67046 | 22 |
user_home: Path, |
67045 | 23 |
progress: Progress) |
64188 | 24 |
{ |
25 |
other_isabelle => |
|
26 |
||
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
27 |
override def toString: String = isabelle_home.toString |
67046 | 28 |
|
29 |
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) |
|
30 |
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") |
|
31 |
||
64188 | 32 |
|
33 |
/* static system */ |
|
34 |
||
65930 | 35 |
def bash( |
36 |
script: String, |
|
37 |
redirect: Boolean = false, |
|
38 |
echo: Boolean = false, |
|
39 |
strict: Boolean = true): Process_Result = |
|
67046 | 40 |
progress.bash( |
41 |
"export USER_HOME=" + File.bash_path(user_home) + "\n" + |
|
42 |
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, |
|
65930 | 43 |
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) |
64188 | 44 |
|
65930 | 45 |
def apply( |
46 |
cmdline: String, |
|
47 |
redirect: Boolean = false, |
|
48 |
echo: Boolean = false, |
|
49 |
strict: Boolean = true): Process_Result = |
|
50 |
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) |
|
64188 | 51 |
|
52 |
def resolve_components(echo: Boolean): Unit = |
|
73243
7f55a3e28c88
more robust: resolve historic components via current tool to access current server;
wenzelm
parents:
73240
diff
changeset
|
53 |
other_isabelle( |
7f55a3e28c88
more robust: resolve historic components via current tool to access current server;
wenzelm
parents:
73240
diff
changeset
|
54 |
"env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) + |
7f55a3e28c88
more robust: resolve historic components via current tool to access current server;
wenzelm
parents:
73240
diff
changeset
|
55 |
" isabelle components -a", redirect = true, echo = echo).check |
64188 | 56 |
|
69166 | 57 |
def getenv(name: String): String = |
58 |
other_isabelle("getenv -b " + Bash.string(name)).check.out |
|
59 |
||
60 |
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER")) |
|
64188 | 61 |
|
68754 | 62 |
val etc: Path = isabelle_home_user + Path.explode("etc") |
63 |
val etc_settings: Path = etc + Path.explode("settings") |
|
64 |
val etc_preferences: Path = etc + Path.explode("preferences") |
|
64188 | 65 |
|
73625
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
66 |
|
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
67 |
/* NEWS */ |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
68 |
|
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
69 |
def make_news(): Unit = |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
70 |
{ |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
71 |
val doc_dir = isabelle_home + Path.explode("doc") |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
72 |
val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts")) |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
73 |
|
71601 | 74 |
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true). |
73625
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
75 |
foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir)) |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
76 |
|
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
77 |
HTML.write_document(doc_dir, "NEWS.html", |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
78 |
List(HTML.title("NEWS")), |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
79 |
List( |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
80 |
HTML.chapter("NEWS"), |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
81 |
HTML.source(Symbol.decode(File.read(isabelle_home + Path.explode("NEWS")))))) |
f8f065e20837
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents:
73522
diff
changeset
|
82 |
} |
64188 | 83 |
|
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
84 |
|
69388 | 85 |
/* components */ |
86 |
||
87 |
def init_components( |
|
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
88 |
component_repository: String = Components.default_component_repository, |
69434 | 89 |
components_base: Path = Components.default_components_base, |
69396 | 90 |
catalogs: List[String] = Nil, |
91 |
components: List[String] = Nil): List[String] = |
|
69388 | 92 |
{ |
69404
de88761edbe2
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents:
69401
diff
changeset
|
93 |
val dir = Components.admin(isabelle_home) |
73240
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
94 |
|
3e963d68d394
more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;
wenzelm
parents:
72375
diff
changeset
|
95 |
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) :: |
69396 | 96 |
catalogs.map(name => |
69434 | 97 |
"init_components " + File.bash_path(components_base) + " " + |
98 |
File.bash_path(dir + Path.basic(name))) ::: |
|
69396 | 99 |
components.map(name => |
69434 | 100 |
"init_component " + File.bash_path(components_base + Path.basic(name))) |
69388 | 101 |
} |
102 |
||
103 |
||
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
104 |
/* settings */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
105 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
106 |
def clean_settings(): Boolean = |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
107 |
if (!etc_settings.is_file) true |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
108 |
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
109 |
etc_settings.file.delete; true |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
110 |
} |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
111 |
else false |
64188 | 112 |
|
73340 | 113 |
def init_settings(settings: List[String]): Unit = |
64188 | 114 |
{ |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
115 |
if (!clean_settings()) |
64188 | 116 |
error("Cannot proceed with existing user settings file: " + etc_settings) |
117 |
||
72375 | 118 |
Isabelle_System.make_directory(etc_settings.dir) |
64188 | 119 |
File.write(etc_settings, |
120 |
"# generated by Isabelle " + Date.now() + "\n" + |
|
69388 | 121 |
"#-*- shell-script -*- :mode=shellscript:\n" + |
122 |
settings.mkString("\n", "\n", "\n")) |
|
64188 | 123 |
} |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
124 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
125 |
|
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
126 |
/* cleanup */ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
127 |
|
73340 | 128 |
def cleanup(): Unit = |
69168
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
129 |
{ |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
130 |
clean_settings() |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
131 |
etc.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
132 |
isabelle_home_user.file.delete |
68816d1c73a7
eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents:
69166
diff
changeset
|
133 |
} |
64188 | 134 |
} |