1/*  Title:      Pure/Admin/components.scala
2    Author:     Makarius
3
4Isabelle system components.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object Components
14{
15  /* archive name */
16
17  object Archive
18  {
19    val suffix: String = ".tar.gz"
20
21    def apply(name: String): String =
22      if (name == "") error("Bad component name: " + quote(name))
23      else name + suffix
24
25    def unapply(archive: String): Option[String] =
26    {
27      for {
28        name0 <- Library.try_unsuffix(suffix, archive)
29        name <- proper_string(name0)
30      } yield name
31    }
32
33    def get_name(archive: String): String =
34      unapply(archive) getOrElse
35        error("Bad component archive name (expecting .tar.gz): " + quote(archive))
36  }
37
38
39  /* component collections */
40
41  val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE")
42
43  def admin(dir: Path): Path = dir + Path.explode("Admin/components")
44
45  def contrib(dir: Path = Path.current, name: String = ""): Path =
46    dir + Path.explode("contrib") + Path.explode(name)
47
48  def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
49  {
50    val name = Archive.get_name(archive.file_name)
51    progress.echo("Unpacking " + name)
52    Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
53    name
54  }
55
56  def resolve(base_dir: Path, names: List[String],
57    target_dir: Option[Path] = None,
58    copy_dir: Option[Path] = None,
59    progress: Progress = No_Progress)
60  {
61    Isabelle_System.mkdirs(base_dir)
62    for (name <- names) {
63      val archive_name = Archive(name)
64      val archive = base_dir + Path.explode(archive_name)
65      if (!archive.is_file) {
66        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
67        progress.echo("Getting " + remote)
68        Bytes.write(archive, Url.read_bytes(Url(remote)))
69      }
70      for (dir <- copy_dir) {
71        Isabelle_System.mkdirs(dir)
72        File.copy(archive, dir)
73      }
74      unpack(target_dir getOrElse base_dir, archive, progress = progress)
75    }
76  }
77
78  def purge(dir: Path, platform: Platform.Family.Value)
79  {
80    def purge_platforms(platforms: String*): Set[String] =
81      platforms.flatMap(name => List("x86-" + name, "x86_64_32-" + name, "x86_64-" + name)).toSet +
82      "ppc-darwin"
83    val purge_set =
84      platform match {
85        case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
86        case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
87        case Platform.Family.windows => purge_platforms("linux", "darwin")
88      }
89
90    File.find_files(dir.file,
91      (file: JFile) => file.isDirectory && purge_set(file.getName),
92      include_dirs = true).foreach(Isabelle_System.rm_tree)
93  }
94
95
96  /* component directory content */
97
98  def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings")
99  def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components")
100
101  def check_dir(dir: Path): Boolean =
102    settings(dir).is_file || components(dir).is_file
103
104  def read_components(dir: Path): List[String] =
105    split_lines(File.read(components(dir))).filter(_.nonEmpty)
106
107  def write_components(dir: Path, lines: List[String]): Unit =
108    File.write(components(dir), terminate_lines(lines))
109
110
111  /* component repository content */
112
113  val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
114
115  sealed case class SHA1_Digest(sha1: String, file_name: String)
116  {
117    override def toString: String = sha1 + "  " + file_name
118  }
119
120  def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
121    (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
122      Word.explode(line) match {
123        case Nil => None
124        case List(sha1, name) => Some(SHA1_Digest(sha1, name))
125        case _ => error("Bad components.sha1 entry: " + quote(line))
126      })
127
128  def write_components_sha1(entries: List[SHA1_Digest]) =
129    File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
130
131
132
133  /** build and publish components **/
134
135  def build_components(
136    options: Options,
137    components: List[Path],
138    progress: Progress = No_Progress,
139    publish: Boolean = false,
140    force: Boolean = false,
141    update_components_sha1: Boolean = false)
142  {
143    val archives: List[Path] =
144      for (path <- components) yield {
145        path.file_name match {
146          case Archive(_) => path
147          case name =>
148            if (!path.is_dir) error("Bad component directory: " + path)
149            else if (!check_dir(path)) {
150              error("Malformed component directory: " + path +
151                "\n  (requires " + settings() + " or " + Components.components() + ")")
152            }
153            else {
154              val component_path = path.expand
155              val archive_dir = component_path.dir
156              val archive_name = Archive(name)
157
158              val archive = archive_dir + Path.explode(archive_name)
159              if (archive.is_file && !force) {
160                error("Component archive already exists: " + archive)
161              }
162
163              progress.echo("Packaging " + archive_name)
164              Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
165                dir = archive_dir).check
166
167              archive
168            }
169        }
170      }
171
172    if ((publish && archives.nonEmpty) || update_components_sha1) {
173      options.string("isabelle_components_server") match {
174        case SSH.Target(user, host) =>
175          using(SSH.open_session(options, host = host, user = user))(ssh =>
176          {
177            val components_dir = Path.explode(options.string("isabelle_components_dir"))
178            val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
179
180            for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
181              error("Bad remote directory: " + dir)
182            }
183
184            if (publish) {
185              for (archive <- archives) {
186                val archive_name = archive.file_name
187                val name = Archive.get_name(archive_name)
188                val remote_component = components_dir + archive.base
189                val remote_contrib = contrib_dir + Path.explode(name)
190
191                // component archive
192                if (ssh.is_file(remote_component) && !force) {
193                  error("Remote component archive already exists: " + remote_component)
194                }
195                progress.echo("Uploading " + archive_name)
196                ssh.write_file(remote_component, archive)
197
198                // contrib directory
199                val is_standard_component =
200                  Isabelle_System.with_tmp_dir("component")(tmp_dir =>
201                  {
202                    Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
203                    check_dir(tmp_dir + Path.explode(name))
204                  })
205                if (is_standard_component) {
206                  if (ssh.is_dir(remote_contrib)) {
207                    if (force) ssh.rm_tree(remote_contrib)
208                    else error("Remote component directory already exists: " + remote_contrib)
209                  }
210                  progress.echo("Unpacking remote " + archive_name)
211                  ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
212                    ssh.bash_path(remote_component)).check
213                }
214                else {
215                  progress.echo_warning("No unpacking of non-standard component: " + archive_name)
216                }
217              }
218            }
219
220            // remote SHA1 digests
221            if (update_components_sha1) {
222              val lines =
223                for {
224                  entry <- ssh.read_dir(components_dir)
225                  if entry.is_file && entry.name.endsWith(Archive.suffix)
226                }
227                yield {
228                  progress.echo("Digesting remote " + entry.name)
229                  Library.trim_line(
230                    ssh.execute("cd " + ssh.bash_path(components_dir) +
231                      "; sha1sum " + Bash.string(entry.name)).check.out)
232                }
233              write_components_sha1(read_components_sha1(lines))
234            }
235          })
236        case s => error("Bad isabelle_components_server: " + quote(s))
237      }
238    }
239
240    // local SHA1 digests
241    {
242      val new_entries =
243        for (archive <- archives)
244        yield {
245          val file_name = archive.file_name
246          progress.echo("Digesting local " + file_name)
247          val sha1 = SHA1.digest(archive).rep
248          SHA1_Digest(sha1, file_name)
249        }
250      val new_names = new_entries.map(_.file_name).toSet
251
252      write_components_sha1(
253        new_entries :::
254        read_components_sha1().filterNot(entry => new_names.contains(entry.file_name)))
255    }
256  }
257
258
259  /* Isabelle tool wrapper */
260
261  private val relevant_options =
262    List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
263
264  val isabelle_tool =
265    Isabelle_Tool("build_components", "build and publish Isabelle components", args =>
266    {
267      var publish = false
268      var update_components_sha1 = false
269      var force = false
270      var options = Options.init()
271
272      def show_options: String =
273        cat_lines(relevant_options.map(name => options.options(name).print))
274
275      val getopts = Getopts("""
276Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
277
278  Options are:
279    -P           publish on SSH server (see options below)
280    -f           force: overwrite existing component archives and directories
281    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
282    -u           update all SHA1 keys in Isabelle repository Admin/components
283
284  Build and publish Isabelle components as .tar.gz archives on SSH server,
285  depending on system options:
286
287""" + Library.prefix_lines("  ", show_options) + "\n",
288        "P" -> (_ => publish = true),
289        "f" -> (_ => force = true),
290        "o:" -> (arg => options = options + arg),
291        "u" -> (_ => update_components_sha1 = true))
292
293      val more_args = getopts(args)
294      if (more_args.isEmpty && !update_components_sha1) getopts.usage()
295
296      val progress = new Console_Progress
297
298      build_components(options, more_args.map(Path.explode), progress = progress,
299        publish = publish, force = force, update_components_sha1 = update_components_sha1)
300    })
301}
302