|
1 /* Title: Pure/Admin/build_spass.scala |
|
2 Author: Makarius |
|
3 |
|
4 Build Isabelle SPASS component from unofficial download. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Build_SPASS |
|
11 { |
|
12 /* build SPASS */ |
|
13 |
|
14 val default_download_url = "https://www.cs.vu.nl/~jbe248/spass-3.8ds-src.tar.gz" |
|
15 val standard_version = "3.8ds" |
|
16 |
|
17 def build_spass( |
|
18 download_url: String = default_download_url, |
|
19 verbose: Boolean = false, |
|
20 progress: Progress = new Progress, |
|
21 target_dir: Path = Path.current) |
|
22 { |
|
23 Isabelle_System.with_tmp_dir("build")(tmp_dir => |
|
24 { |
|
25 /* required commands */ |
|
26 |
|
27 List("bison", "flex").foreach(cmd => |
|
28 if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd)) |
|
29 |
|
30 |
|
31 /* component */ |
|
32 |
|
33 val Archive_Name = """^.*?([^/]+)$""".r |
|
34 val Component_Name = """^(.+)-src\.tar.gz$""".r |
|
35 val Version = """^[^-]+-([^-]+)$""".r |
|
36 |
|
37 val (archive_name, archive_base_name) = |
|
38 download_url match { |
|
39 case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", name)) |
|
40 case _ => error("Failed to determine source archive name from " + quote(download_url)) |
|
41 } |
|
42 |
|
43 val component_name = |
|
44 archive_name match { |
|
45 case Component_Name(name) => name |
|
46 case _ => error("Failed to determine component name from " + quote(archive_name)) |
|
47 } |
|
48 |
|
49 val version = |
|
50 component_name match { |
|
51 case Version(version) => version |
|
52 case _ => error("Failed to determine component version from " + quote(component_name)) |
|
53 } |
|
54 |
|
55 if (version != standard_version) { |
|
56 progress.echo_warning("Odd SPASS version " + version + " (expected " + standard_version + ")") |
|
57 } |
|
58 |
|
59 val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name)) |
|
60 progress.echo("Component " + component_dir) |
|
61 |
|
62 val platform_name = |
|
63 proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) |
|
64 .getOrElse(error("No 64bit platform")) |
|
65 |
|
66 val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name)) |
|
67 |
|
68 |
|
69 /* download source */ |
|
70 |
|
71 val archive_path = tmp_dir + Path.basic(archive_name) |
|
72 Isabelle_System.download(download_url, archive_path, progress = progress) |
|
73 |
|
74 Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check |
|
75 Isabelle_System.bash( |
|
76 "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src", |
|
77 cwd = component_dir.file).check |
|
78 |
|
79 |
|
80 /* build */ |
|
81 |
|
82 progress.echo("Building SPASS ...") |
|
83 |
|
84 val build_dir = tmp_dir + Path.basic(archive_base_name) |
|
85 Isabelle_System.bash("make", |
|
86 cwd = build_dir.file, |
|
87 progress_stdout = progress.echo_if(verbose, _), |
|
88 progress_stderr = progress.echo_if(verbose, _)).check |
|
89 |
|
90 |
|
91 /* install */ |
|
92 |
|
93 File.copy(build_dir + Path.basic("LICENCE"), component_dir + Path.basic("LICENSE")) |
|
94 |
|
95 val install_files = List("SPASS") |
|
96 for (name <- install_files ::: install_files.map(_ + ".exe")) { |
|
97 val path = build_dir + Path.basic(name) |
|
98 if (path.is_file) File.copy(path, platform_dir) |
|
99 } |
|
100 |
|
101 |
|
102 /* settings */ |
|
103 |
|
104 val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) |
|
105 File.write(etc_dir + Path.basic("settings"), |
|
106 """# -*- shell-script -*- :mode=shellscript: |
|
107 |
|
108 SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64" |
|
109 SPASS_VERSION=""" + quote(version) + """ |
|
110 """) |
|
111 |
|
112 /* README */ |
|
113 |
|
114 File.write(component_dir + Path.basic("README"), |
|
115 """This distribution of SPASS 3.8ds, described in Blanchette, Popescu, Wand, and |
|
116 Weidenbach's ITP 2012 paper "More SPASS with Isabelle", has been compiled from |
|
117 sources available at """ + download_url + """ |
|
118 via "make". |
|
119 |
|
120 The Windows/Cygwin compilation required commenting out the line |
|
121 |
|
122 #include "execinfo.h" |
|
123 |
|
124 in "misc.c" as well as most of the body of the "misc_DumpCore" function. |
|
125 |
|
126 The latest official SPASS sources can be downloaded from |
|
127 http://www.spass-prover.org/. Be aware, however, that the official SPASS |
|
128 releases are not compatible with Isabelle. |
|
129 |
|
130 |
|
131 Viel SPASS! |
|
132 |
|
133 |
|
134 Jasmin Blanchette |
|
135 16-May-2018 |
|
136 |
|
137 Makarius |
|
138 """ + Date.Format.date(Date.now()) + "\n") |
|
139 }) |
|
140 } |
|
141 |
|
142 /* Isabelle tool wrapper */ |
|
143 |
|
144 val isabelle_tool = |
|
145 Isabelle_Tool("build_spass", "build prover component from source distribution", |
|
146 args => |
|
147 { |
|
148 var target_dir = Path.current |
|
149 var download_url = default_download_url |
|
150 var verbose = false |
|
151 |
|
152 val getopts = Getopts(""" |
|
153 Usage: isabelle build_spass [OPTIONS] |
|
154 |
|
155 Options are: |
|
156 -D DIR target directory (default ".") |
|
157 -U URL download URL |
|
158 (default: """" + default_download_url + """") |
|
159 -v verbose |
|
160 |
|
161 Build prover component from the specified source distribution. |
|
162 """, |
|
163 "D:" -> (arg => target_dir = Path.explode(arg)), |
|
164 "U:" -> (arg => download_url = arg), |
|
165 "v" -> (_ => verbose = true)) |
|
166 |
|
167 val more_args = getopts(args) |
|
168 if (more_args.nonEmpty) getopts.usage() |
|
169 |
|
170 val progress = new Console_Progress() |
|
171 |
|
172 build_spass(download_url = download_url, verbose = verbose, progress = progress, |
|
173 target_dir = target_dir) |
|
174 }) |
|
175 } |