src/Pure/Admin/component_verit.scala
author wenzelm
Tue, 07 Mar 2023 23:24:40 +0100
changeset 77570 98b4a9902582
parent 77566 2a99fcb283ee
child 80004 31ebb6be32b0
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77570
98b4a9902582 tuned headers;
wenzelm
parents: 77566
diff changeset
     1
/*  Title:      Pure/Admin/component_verit.scala
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     3
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     4
Build Isabelle veriT component from official download.
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     5
*/
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     6
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     7
package isabelle
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     8
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
     9
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
    10
object Component_VeriT {
74819
ed3adabf0dbe updated to verit-2021.06.2-rmx;
wenzelm
parents: 74417
diff changeset
    11
  val default_download_url = "https://verit.loria.fr/rmx/2021.06.2/verit-2021.06.2-rmx.tar.gz"
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    12
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    13
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    14
  /* build veriT */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    15
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    16
  def build_verit(
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    17
    download_url: String = default_download_url,
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    18
    progress: Progress = new Progress,
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    19
    target_dir: Path = Path.current,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74819
diff changeset
    20
    mingw: MinGW = MinGW.none
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74819
diff changeset
    21
  ): Unit = {
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    22
    mingw.check
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    23
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    24
    Isabelle_System.with_tmp_dir("build") { tmp_dir =>
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    25
      /* component */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    26
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    27
      val Archive_Name = """^.*?([^/]+)$""".r
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    28
      val Version = """^[^-]+-(.+)\.tar.gz$""".r
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    29
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    30
      val archive_name =
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    31
        download_url match {
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    32
          case Archive_Name(name) => name
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    33
          case _ => error("Failed to determine source archive name from " + quote(download_url))
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    34
        }
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    35
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    36
      val version =
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    37
        archive_name match {
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    38
          case Version(version) => version
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    39
          case _ => error("Failed to determine component version from " + quote(archive_name))
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    40
        }
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    41
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    42
      val component_name = "verit-" + version
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    43
      val component_dir =
76547
9fe5d8c70352 tuned signature;
wenzelm
parents: 76541
diff changeset
    44
        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    45
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    46
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    47
      /* platform */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    48
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    49
      val platform_name =
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    50
        proper_string(Isabelle_System.getenv("ISABELLE_WINDOWS_PLATFORM64")) orElse
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    51
        proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    52
        error("No 64bit platform")
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    53
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    54
      val platform_dir =
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    55
        Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    56
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    57
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    58
      /* download source */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    59
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    60
      val archive_path = tmp_dir + Path.basic(archive_name)
73566
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73340
diff changeset
    61
      Isabelle_System.download_file(download_url, archive_path, progress = progress)
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    62
76540
83de6e9ae983 clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents: 76529
diff changeset
    63
      Isabelle_System.extract(archive_path, tmp_dir)
76529
ded37aade88e clarified signature;
wenzelm
parents: 76518
diff changeset
    64
      val source_dir = File.get_dir(tmp_dir, title = download_url)
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    65
76541
3706b88035d2 more direct target directory;
wenzelm
parents: 76540
diff changeset
    66
      Isabelle_System.extract(archive_path, component_dir.src, strip = true)
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    67
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    68
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    69
      /* build */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    70
72440
d0ba71b3297e tuned messages;
wenzelm
parents: 72439
diff changeset
    71
      progress.echo("Building veriT for " + platform_name + " ...")
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    72
72475
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    73
      val configure_options =
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    74
        if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    75
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    76
      progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
    77
        cwd = source_dir.file, echo = progress.verbose).check
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    78
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    79
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    80
      /* install */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    81
76529
ded37aade88e clarified signature;
wenzelm
parents: 76518
diff changeset
    82
      Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
72475
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    83
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    84
      val exe_path = Path.basic("veriT").platform_exe
76529
ded37aade88e clarified signature;
wenzelm
parents: 76518
diff changeset
    85
      Isabelle_System.copy_file(source_dir + exe_path, platform_dir)
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
    86
      Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
72475
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
    87
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    88
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    89
      /* settings */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    90
76548
0af64cc2eee9 tuned signature;
wenzelm
parents: 76547
diff changeset
    91
      component_dir.write_settings("""
72478
b452242dce36 proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents: 72476
diff changeset
    92
ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    93
""")
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    94
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    95
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    96
      /* README */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    97
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    98
      File.write(component_dir.README,
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
    99
"""This is veriT """ + version + """ from
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   100
""" + download_url + """
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   101
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   102
It has been built from sources like this:
72475
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
   103
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
   104
  cd src
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
   105
  ./configure
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
   106
  make
37e344d8fac8 proper libraries_closure for libgmp;
wenzelm
parents: 72472
diff changeset
   107
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   108
72443
ff5e700ed490 more robust: ignore existing gmp installation, but let veriT incorporate extern/gmp;
wenzelm
parents: 72442
diff changeset
   109
        Makarius
ff5e700ed490 more robust: ignore existing gmp installation, but let veriT incorporate extern/gmp;
wenzelm
parents: 72442
diff changeset
   110
        """ + Date.Format.date(Date.now()) + "\n")
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   111
    }
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   112
}
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   113
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   114
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   115
  /* Isabelle tool wrapper */
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   116
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   117
  val isabelle_tool =
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
   118
    Isabelle_Tool("component_verit", "build prover component from official download",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   119
      Scala_Project.here,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   120
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   121
        var target_dir = Path.current
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   122
        var mingw = MinGW.none
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   123
        var download_url = default_download_url
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   124
        var verbose = false
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   125
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   126
        val getopts = Getopts("""
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
   127
Usage: isabelle component_verit [OPTIONS]
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   128
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   129
  Options are:
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   130
    -D DIR       target directory (default ".")
72476
845001bdf41a proper setup for Windows/MinGW;
wenzelm
parents: 72475
diff changeset
   131
    -M DIR       msys/mingw root specification for Windows
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   132
    -U URL       download URL
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   133
                 (default: """" + default_download_url + """")
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   134
    -v           verbose
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   135
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   136
  Build prover component from official download.
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   137
""",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   138
          "D:" -> (arg => target_dir = Path.explode(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   139
          "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   140
          "U:" -> (arg => download_url = arg),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   141
          "v" -> (_ => verbose = true))
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   142
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   143
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   144
        if (more_args.nonEmpty) getopts.usage()
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   145
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
   146
        val progress = new Console_Progress(verbose = verbose)
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   147
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
   148
        build_verit(download_url = download_url, progress = progress,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   149
          target_dir = target_dir, mingw = mingw)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   150
      })
72439
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents:
diff changeset
   151
}