src/Pure/Admin/build_easychair.scala
author wenzelm
Sun, 06 Nov 2022 22:20:51 +0100
changeset 76479 8ac1d83301b5
parent 76398 fc35958d2e73
child 76518 b30b8e23383c
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76396
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_easychair.scala
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     3
76479
8ac1d83301b5 tuned comments;
wenzelm
parents: 76398
diff changeset
     4
Build Isabelle component for Easychair LaTeX style.
76396
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     5
76398
fc35958d2e73 tuned comments;
wenzelm
parents: 76396
diff changeset
     6
See also https://easychair.org/publications/for_authors
76396
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     7
*/
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     8
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
     9
package isabelle
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    10
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    11
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    12
object Build_Easychair {
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    13
  /* build easychair component */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    14
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    15
  val default_url = "https://easychair.org/publications/easychair.zip"
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    16
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    17
  def build_easychair(
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    18
    download_url: String = default_url,
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    19
    target_dir: Path = Path.current,
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    20
    progress: Progress = new Progress
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    21
  ): Unit = {
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    22
    Isabelle_System.require_command("unzip", test = "-h")
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    23
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    24
    Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    25
      Isabelle_System.with_tmp_dir("download") { download_dir =>
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    26
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    27
        /* download */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    28
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    29
        Isabelle_System.download_file(download_url, download_file, progress = progress)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    30
        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    31
          cwd = download_dir.file).check
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    32
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    33
        val easychair_dir =
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    34
          File.read_dir(download_dir) match {
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    35
            case List(name) => download_dir + Path.explode(name)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    36
            case bad =>
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    37
              error("Expected exactly one directory entry in " + download_file +
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    38
                bad.mkString("\n", "\n  ", ""))
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    39
          }
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    40
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    41
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    42
        /* component */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    43
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    44
        val version =
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    45
          Library.try_unprefix("EasyChair", easychair_dir.file_name)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    46
            .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name))
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    47
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    48
        val component = "easychair-" + version
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    49
        val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    50
        progress.echo("Component " + component_dir)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    51
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    52
        component_dir.file.delete
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    53
        Isabelle_System.copy_dir(easychair_dir, component_dir)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    54
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    55
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    56
        /* settings */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    57
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    58
        val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    59
        File.write(etc_dir + Path.basic("settings"),
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    60
          """# -*- shell-script -*- :mode=shellscript:
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    61
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    62
ISABELLE_EASYCHAIR_HOME="$COMPONENT"
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    63
""")
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    64
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    65
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    66
        /* README */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    67
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    68
        File.write(component_dir + Path.basic("README"),
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    69
          """This is the Easychair style for authors from
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    70
""" + download_url + """
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    71
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    72
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    73
    Makarius
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    74
    """ + Date.Format.date(Date.now()) + "\n")
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    75
      }
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    76
    }
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    77
  }
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    78
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    79
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    80
  /* Isabelle tool wrapper */
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    81
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    82
  val isabelle_tool =
76479
8ac1d83301b5 tuned comments;
wenzelm
parents: 76398
diff changeset
    83
    Isabelle_Tool("build_easychair", "build component for Easychair LaTeX style",
76396
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    84
      Scala_Project.here,
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    85
      { args =>
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    86
        var target_dir = Path.current
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    87
        var download_url = default_url
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    88
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    89
        val getopts = Getopts("""
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    90
Usage: isabelle build_easychair [OPTIONS]
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    91
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    92
  Options are:
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    93
    -D DIR       target directory (default ".")
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    94
    -U URL       download URL (default: """" + default_url + """")
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    95
76479
8ac1d83301b5 tuned comments;
wenzelm
parents: 76398
diff changeset
    96
  Build component for Easychair LaTeX style.
76396
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    97
""",
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    98
          "D:" -> (arg => target_dir = Path.explode(arg)),
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
    99
          "U:" -> (arg => download_url = arg))
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   100
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   101
        val more_args = getopts(args)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   102
        if (more_args.nonEmpty) getopts.usage()
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   103
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   104
        val progress = new Console_Progress()
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   105
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   106
        build_easychair(download_url = download_url, target_dir = target_dir, progress = progress)
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   107
      })
389d77e6be9f support for Easychair style with demo document;
wenzelm
parents:
diff changeset
   108
}