src/Pure/Admin/component_cvc5.scala
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 81750 377887fbc968
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
     1
/*  Title:      Pure/Admin/component_cvc5.scala
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     3
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     4
Build Isabelle component for cvc5. See also:
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     5
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     6
  - https://cvc5.github.io/
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     7
  - https://github.com/cvc5/cvc5
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     8
*/
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
     9
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    10
package isabelle
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    11
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    12
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
    13
object Component_CVC5 {
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    14
  /* platform information */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    15
78300
ab95c9f2d55c tuned signature;
wenzelm
parents: 78158
diff changeset
    16
  sealed case class Download_Platform(platform_name: String, download_name: String) {
81707
f135e0693202 provide component cvc5-1.2.0, including arm64-linux;
wenzelm
parents: 81578
diff changeset
    17
    def is_arm: Boolean = platform_name.startsWith("arm64-")
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    18
    def is_windows: Boolean = platform_name.endsWith("-windows")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    19
  }
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    20
78300
ab95c9f2d55c tuned signature;
wenzelm
parents: 78158
diff changeset
    21
  val platforms: List[Download_Platform] =
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    22
    List(
81578
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    23
      Download_Platform("arm64-darwin", "cvc5-macOS-arm64-static.zip"),
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    24
      Download_Platform("arm64-linux", "cvc5-Linux-arm64-static.zip"),
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    25
      Download_Platform("x86_64-darwin", "cvc5-macOS-x86_64-static.zip"),
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    26
      Download_Platform("x86_64-linux", "cvc5-Linux-x86_64-static.zip"),
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    27
      Download_Platform("x86_64-windows", "cvc5-Win64-x86_64-static.zip"))
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    28
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    29
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    30
  /* build cvc5 */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    31
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    32
  val default_url = "https://github.com/cvc5/cvc5/releases/download"
81578
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    33
  val default_version = "1.2.0"
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    34
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    35
  def build_cvc5(
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    36
    base_url: String = default_url,
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    37
    version: String = default_version,
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    38
    target_dir: Path = Path.current,
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    39
    progress: Progress = new Progress
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    40
  ): Unit = {
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    41
    /* component name */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    42
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    43
    val component = "cvc5-" + version
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76477
diff changeset
    44
    val component_dir =
76547
9fe5d8c70352 tuned signature;
wenzelm
parents: 76518
diff changeset
    45
      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    46
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    47
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    48
    /* download executables */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    49
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    50
    for (platform <- platforms) {
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    51
      Isabelle_System.with_tmp_dir("download") { download_dir =>
81578
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
    52
        val download = base_url + "/cvc5-" + version + "/" + platform.download_name
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    53
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    54
        val archive_name =
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    55
          Url.get_base_name(platform.download_name) getOrElse
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    56
            error("Malformed download name " + quote(platform.download_name))
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    57
        val archive_path = download_dir + Path.basic(archive_name)
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    58
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    59
        val platform_dir = component_dir.path + Path.explode(platform.platform_name)
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    60
        Isabelle_System.make_directory(platform_dir)
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    61
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    62
        val exe_path = Path.explode("cvc5").exe_if(platform.is_windows)
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    63
        val exe_bin_path = Path.explode("cvc5-bin").exe_if(platform.is_windows)
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    64
81707
f135e0693202 provide component cvc5-1.2.0, including arm64-linux;
wenzelm
parents: 81578
diff changeset
    65
        val exe = platform_dir + exe_path
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    66
        val exe_bin = platform_dir + exe_bin_path
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    67
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    68
        Isabelle_System.download_file(download, archive_path, progress = progress)
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    69
        Isabelle_System.extract(archive_path, download_dir, strip = true)
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    70
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    71
        Isabelle_System.copy_file(download_dir + Path.basic("bin") + exe_path, exe_bin)
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    72
        File.set_executable(exe_bin)
81707
f135e0693202 provide component cvc5-1.2.0, including arm64-linux;
wenzelm
parents: 81578
diff changeset
    73
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    74
        File.write(exe, """#!/usr/bin/env bash
81707
f135e0693202 provide component cvc5-1.2.0, including arm64-linux;
wenzelm
parents: 81578
diff changeset
    75
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    76
"$CVC5_HOME/cvc5-bin" "$@"
81707
f135e0693202 provide component cvc5-1.2.0, including arm64-linux;
wenzelm
parents: 81578
diff changeset
    77
""")
81750
377887fbc968 rebuild cvc5 component (still inactive);
wenzelm
parents: 81707
diff changeset
    78
        File.set_executable(exe)
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    79
      }
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    80
    }
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    81
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    82
79750
f8fb4384180e provide cvc5-1.1.1 for testing --- still inactive;
wenzelm
parents: 78300
diff changeset
    83
  /* settings */
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    84
76548
0af64cc2eee9 tuned signature;
wenzelm
parents: 76547
diff changeset
    85
    component_dir.write_settings("""
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    86
CVC5_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    87
CVC5_VERSION=""" + Bash.string(version) + """
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    88
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    89
CVC5_SOLVER="$CVC5_HOME/cvc5"
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    90
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    91
if [ -e "$CVC5_HOME" ]
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    92
then
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    93
  CVC5_INSTALLED="yes"
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    94
fi
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    95
""")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    96
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    97
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    98
    /* README */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
    99
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76477
diff changeset
   100
    File.write(component_dir.README,
81578
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
   101
      """This distribution of cvc5 was assembled from official downloads from
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
   102
""" + base_url + """ --- the static.zip variants
78b746a99211 build component for cvc5-1.2.0;
wenzelm
parents: 79944
diff changeset
   103
for macOS, Linux, and Windows, with ARM64 support on macOS and Linux.
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   104
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   105
The downloaded files were renamed and made executable.
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   106
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   107
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   108
        Makarius
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   109
        """ + Date.Format.date(Date.now()) + "\n")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   110
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   111
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   112
    /* AUTHORS and COPYING */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   113
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   114
    // download "latest" versions as reasonable approximation
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   115
    def raw_download(name: String): Unit =
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   116
      Isabelle_System.download_file("https://raw.githubusercontent.com/cvc5/cvc5/main/" + name,
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76477
diff changeset
   117
        component_dir.path + Path.explode(name))
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   118
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   119
    raw_download("AUTHORS")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   120
    raw_download("COPYING")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   121
  }
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   122
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   123
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   124
  /* Isabelle tool wrapper */
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   125
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   126
  val isabelle_tool =
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
   127
    Isabelle_Tool("component_cvc5", "build component for cvc5", Scala_Project.here,
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   128
      { args =>
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   129
        var target_dir = Path.current
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   130
        var base_url = default_url
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   131
        var version = default_version
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   132
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   133
        val getopts = Getopts("""
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
   134
Usage: isabelle component_cvc5 [OPTIONS]
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   135
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   136
  Options are:
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   137
    -D DIR       target directory (default ".")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   138
    -U URL       download URL (default: """" + default_url + """")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   139
    -V VERSION   version (default: """" + default_version + """")
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   140
76477
6e68ec0fdc48 tuned message;
wenzelm
parents: 76183
diff changeset
   141
  Build component for cvc5 solver.
76017
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   142
""",
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   143
          "D:" -> (arg => target_dir = Path.explode(arg)),
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   144
          "U:" -> (arg => base_url = arg),
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   145
          "V:" -> (arg => version = arg))
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   146
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   147
        val more_args = getopts(args)
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   148
        if (more_args.nonEmpty) getopts.usage()
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   149
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   150
        val progress = new Console_Progress()
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   151
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   152
        build_cvc5(base_url = base_url, version = version, target_dir = target_dir,
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   153
          progress = progress)
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   154
      })
9ca22009c2d0 tool to build Isabelle component for cvc5;
wenzelm
parents:
diff changeset
   155
}