src/Pure/System/nodejs.scala
author wenzelm
Mon, 08 Sep 2025 23:55:00 +0200
changeset 83116 e0c85cb6b924
parent 83115 ee6a594f0e7e
child 83120 402f51de0347
permissions -rw-r--r--
proper platform_context.execute for Windows/MinGW;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/nodejs.scala
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     3
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
     4
Support for the Node.js platform, in conjunction with Isabelle/VSCodium.
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     5
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
     6
See also: https://nodejs.org/docs/latest-v22.x/api/index.html
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     7
*/
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     8
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     9
package isabelle
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    10
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    11
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    12
object Nodejs {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    13
  /** independent installation **/
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    14
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    15
  val default_version = "22.17.0"
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    16
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    17
  def context(
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    18
    platform_context: Isabelle_Platform.Context = Isabelle_Platform.Context(),
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    19
    version: String = default_version
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    20
  ): Context = new Context(platform_context, version)
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    21
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    22
  def setup(
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    23
    base_dir: Path,
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    24
    platform_context: Isabelle_Platform.Context = Isabelle_Platform.Context(),
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    25
    version: String = default_version,
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    26
    packages: List[String] = Nil
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    27
  ): Directory = {
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    28
    context(platform_context = platform_context, version = version)
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    29
      .setup(base_dir, packages = packages)
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    30
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    31
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    32
  class Context private[Nodejs](val platform_context: Isabelle_Platform.Context, version: String) {
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    33
    def platform: Isabelle_Platform = platform_context.isabelle_platform
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    34
    def progress: Progress = platform_context.progress
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    35
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    36
    override def toString: String =
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    37
      "node-" + version + "-" + platform.ISABELLE_PLATFORM(windows = true, apple = true)
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    38
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    39
    def arch: String = if (platform.is_arm) "arm64" else "x64"
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    40
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    41
    def platform_name: String =
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    42
      if (platform.is_windows) "win" else if (platform.is_macos) "darwin" else "linux"
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    43
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    44
    def full_name: String = "node-v" + version + "-" + platform_name + "-" + arch
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    45
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    46
    def download_ext: String = if (platform.is_windows) "zip" else "tar.gz"
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    47
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    48
    def download_url: String =
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    49
      "https://nodejs.org/dist/v" + version + "/" + full_name + "." + download_ext
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    50
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    51
    def setup(base_dir: Path, packages: List[String] = Nil): Directory = {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    52
      Isabelle_System.with_tmp_file("node", ext = download_ext) { archive =>
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    53
        progress.echo("Getting Node.js ...")
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    54
        Isabelle_System.download_file(download_url, archive)
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    55
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    56
        progress.echo("Installing node ...")
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    57
        Isabelle_System.extract(archive, base_dir)
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    58
        val node_dir = new Directory(this, base_dir + Path.basic(full_name))
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    59
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    60
        for (name <- packages) node_dir.install(name)
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    61
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    62
        node_dir
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    63
      }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    64
    }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    65
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    66
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    67
  class Directory private[Nodejs](val context: Context, val path: Path) {
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    68
    override def toString: String = path.toString
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    69
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    70
    def platform_context: Isabelle_Platform.Context = context.platform_context
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    71
    def progress: Progress = context.progress
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    72
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    73
    def bin_dir: Path =
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    74
      if (platform_context.isabelle_platform.is_windows) path
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    75
      else path + Path.basic("bin")
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    76
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    77
    def path_setup: String =
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    78
      "export PATH=" + Bash.string(platform_context.standard_path(bin_dir)) + """:"$PATH""""
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    79
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    80
    def install(name: String, production: Boolean = false): Unit = {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    81
      progress.echo("Installing " + name + " ...")
83116
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    82
      platform_context.execute(path,
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    83
        Library.make_lines(
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    84
          path_setup,
83116
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    85
          "npm install --global " + if_proper(production, "--production ") + Bash.string(name)
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    86
        )).check
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    87
    }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    88
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    89
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    90
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    91
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    92
  /** source snippets **/
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    93
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    94
  /* require modules */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    95
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    96
  def require_module(name: JS.Source, module: JS.Source): JS.Source =
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    97
    name + " = require(" + module + ")"
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    98
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    99
  def require_path(name: JS.Source, path: Path, dir: Boolean = false): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   100
    require_module(name, JS.platform_path(path, dir = dir))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   101
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
   102
  def require_builtin(name: String): JS.Source =
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
   103
    require_module("const " + name, JS.string(name))
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
   104
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   105
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   106
  /* file-system operations */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   107
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   108
  def require_fs: JS.Source = require_builtin("fs")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   109
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   110
  val encoding_utf8: JSON.T = JSON.Object("encoding" -> "utf8")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   111
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   112
  def read_file(path: Path): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   113
    JS.function("fs.readFileSync", JS.platform_path(path), JS.value(encoding_utf8))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   114
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   115
  def write_file(path: Path, arg: JS.Source): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   116
    JS.function("fs.writeFileSync", JS.platform_path(path), arg, JS.value(encoding_utf8))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   117
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   118
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   119
  /* external process */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   120
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   121
  def execute(js: String): Process_Result =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   122
    Isabelle_System.bash("isabelle node -", input = js,
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   123
      description = "Node.js").check
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   124
}