author | wenzelm |
Wed, 29 Mar 2023 22:21:12 +0200 | |
changeset 77753 | 2b5b093a1c08 |
child 77754 | fea7bc828b8b |
permissions | -rw-r--r-- |
77753
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Admin/component_rsync.scala |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
3 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
4 |
Build Isabelle rsync component from official source distribution. |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
6 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
8 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
9 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
10 |
object Component_Rsync { |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
11 |
/* build rsync */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
12 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
13 |
val default_version = "3.2.7" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
14 |
val default_download_url = "https://github.com/WayneD/rsync/archive/refs/tags" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
15 |
val default_build_options = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
16 |
"--disable-openssl --disable-xxhash --disable-zstd --disable-lz4 --disable-md2man" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
17 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
18 |
def build_rsync( |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
19 |
version: String = default_version, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
20 |
download_url: String = default_download_url, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
21 |
progress: Progress = new Progress, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
22 |
target_dir: Path = Path.current, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
23 |
build_options: String = default_build_options |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
24 |
): Unit = { |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
25 |
Isabelle_System.with_tmp_dir("build") { tmp_dir => |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
26 |
/* component */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
27 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
28 |
val component_name = "rsync-" + version |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
29 |
val component_dir = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
30 |
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
31 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
32 |
val platform_name = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
33 |
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
34 |
.getOrElse(error("No 64bit platform")) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
35 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
36 |
val platform_dir = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
37 |
Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name)) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
38 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
39 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
40 |
/* download source */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
41 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
42 |
val archive_name = "v" + version + ".tar.gz" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
43 |
val archive_path = tmp_dir + Path.explode(archive_name) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
44 |
val archive_url = Url.append_path(download_url, archive_name) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
45 |
Isabelle_System.download_file(archive_url, archive_path, progress = progress) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
46 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
47 |
Isabelle_System.extract(archive_path, tmp_dir) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
48 |
val source_dir = File.get_dir(tmp_dir, title = archive_url) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
49 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
50 |
Isabelle_System.extract(archive_path, component_dir.src, strip = true) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
51 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
52 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
53 |
/* build */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
54 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
55 |
progress.echo("Building rsync for " + platform_name + " ...") |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
56 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
57 |
val build_script = "./configure " + build_options + " && make" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
58 |
Isabelle_System.bash(build_script, cwd = source_dir.file, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
59 |
progress_stdout = progress.echo(_, verbose = true), |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
60 |
progress_stderr = progress.echo(_, verbose = true)).check |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
61 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
62 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
63 |
/* install */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
64 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
65 |
Isabelle_System.copy_file(source_dir + Path.explode("COPYING"), component_dir.LICENSE) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
66 |
Isabelle_System.copy_file(source_dir + Path.explode("rsync").platform_exe, platform_dir) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
67 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
68 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
69 |
/* settings */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
70 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
71 |
component_dir.write_settings(""" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
72 |
ISABELLE_RSYNC_HOME="$COMPONENT/$ISABELLE_PLATFORM64" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
73 |
ISABELLE_RSYNC="$ISABELLE_RSYNC_HOME/rsync" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
74 |
""") |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
75 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
76 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
77 |
/* README */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
78 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
79 |
File.write(component_dir.README, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
80 |
"This is rsync " + version + " from " + download_url + """ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
81 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
82 |
See also: |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
83 |
* https://github.com/WayneD/rsync |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
84 |
* https://rsync.samba.org |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
85 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
86 |
The distribution has been built like this: |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
87 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
88 |
cd src && """ + build_script + """ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
89 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
90 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
91 |
Makarius |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
92 |
""" + Date.Format.date(Date.now()) + "\n") |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
93 |
} |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
94 |
} |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
95 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
96 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
97 |
/* Isabelle tool wrapper */ |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
98 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
99 |
val isabelle_tool = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
100 |
Isabelle_Tool("component_rsync", "build rsync component from source distribution", |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
101 |
Scala_Project.here, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
102 |
{ args => |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
103 |
var target_dir = Path.current |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
104 |
var version = default_version |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
105 |
var download_url = default_download_url |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
106 |
var verbose = false |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
107 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
108 |
val getopts = Getopts(""" |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
109 |
Usage: isabelle component_rsync [OPTIONS] [BUILD_OPTIONS ...] |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
110 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
111 |
Options are: |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
112 |
-D DIR target directory (default ".") |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
113 |
-U URL download URL |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
114 |
(default: """" + default_download_url + """") |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
115 |
-V VERSION version (default: """ + default_version + """) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
116 |
-v verbose |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
117 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
118 |
Build rsync component from the specified source distribution. The default |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
119 |
BUILD_OPTIONS are: |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
120 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
121 |
""" + default_build_options + "\n", |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
122 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
123 |
"U:" -> (arg => download_url = arg), |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
124 |
"V:" -> (arg => version = arg), |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
125 |
"v" -> (_ => verbose = true)) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
126 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
127 |
val more_args = getopts(args) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
128 |
val build_options = |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
129 |
if (more_args.isEmpty) default_build_options else Bash.strings(more_args) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
130 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
131 |
val progress = new Console_Progress(verbose = verbose) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
132 |
|
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
133 |
build_rsync(version = version, download_url = download_url, progress = progress, |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
134 |
target_dir = target_dir, build_options = build_options) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
135 |
}) |
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff
changeset
|
136 |
} |