src/Pure/System/nodejs.scala
author wenzelm
Fri, 12 Sep 2025 17:07:21 +0200
changeset 83138 c66d77fb729e
parent 83124 921ca143fd94
child 83142 9316a0075326
permissions -rw-r--r--
clarified signature: closer to regular bash();
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 setup(
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    18
    base_dir: Path,
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    19
    platform_context: Isabelle_Platform.Context = Isabelle_Platform.Context(),
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    20
    version: String = default_version,
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    21
    packages: List[String] = Nil
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    22
  ): Directory = {
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    23
    val platform = platform_context.isabelle_platform
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    24
    val progress = platform_context.progress
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    25
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    26
    val platform_name =
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    27
      if (platform.is_windows) "win" else if (platform.is_macos) "darwin" else "linux"
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    28
83124
921ca143fd94 support Intel platform on Apple Silicon;
wenzelm
parents: 83123
diff changeset
    29
    val arch = if (platform_context.is_arm) "arm64" else "x64"
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    30
    val full_name = "node-v" + version + "-" + platform_name + "-" + arch
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    31
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    32
    val download_ext = if (platform.is_windows) "zip" else "tar.gz"
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    33
    val download_url = "https://nodejs.org/dist/v" + version + "/" + full_name + "." + download_ext
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    34
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    35
    Isabelle_System.with_tmp_file("node", ext = download_ext) { archive =>
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    36
      progress.echo("Getting Node.js ...")
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    37
      Isabelle_System.download_file(download_url, archive)
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    38
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    39
      progress.echo("Installing node ...")
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    40
      Isabelle_System.extract(archive, base_dir)
83123
dacf5621b8d7 more robust: explicit check of node_exe from download;
wenzelm
parents: 83121
diff changeset
    41
      val node_dir = directory(platform_context, base_dir + Path.basic(full_name))
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    42
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    43
      for (name <- packages) node_dir.install(name)
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    44
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    45
      node_dir
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    46
    }
83108
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
83121
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    49
  def directory(platform_context: Isabelle_Platform.Context, path: Path): Directory = {
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    50
    val node_dir = new Directory(platform_context, path)
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    51
    val node_exe = node_dir.bin_dir + Path.basic("node").exe_if(node_dir.platform.is_windows)
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    52
    if (node_exe.is_file) node_dir else error("Bad Node.js directory " + path)
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    53
  }
74a25a7c2481 support for existing Node.js directory;
wenzelm
parents: 83120
diff changeset
    54
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    55
  class Directory private[Nodejs](
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    56
    val platform_context: Isabelle_Platform.Context,
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    57
    val path: Path
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    58
  ) {
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    59
    def platform: Isabelle_Platform = platform_context.isabelle_platform
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    60
    def progress: Progress = platform_context.progress
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    61
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    62
    override def toString: String = path.file_name
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    63
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    64
    def bin_dir: Path = if (platform.is_windows) path else path + Path.basic("bin")
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    65
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    66
    def path_setup: String =
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    67
      "export PATH=" + Bash.string(platform_context.standard_path(bin_dir)) + """:"$PATH""""
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    68
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    69
    def install(name: String, production: Boolean = false): Unit = {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    70
      progress.echo("Installing " + name + " ...")
83138
c66d77fb729e clarified signature: closer to regular bash();
wenzelm
parents: 83124
diff changeset
    71
      platform_context.bash(
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    72
        Library.make_lines(
83138
c66d77fb729e clarified signature: closer to regular bash();
wenzelm
parents: 83124
diff changeset
    73
          "set -e",
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    74
          path_setup,
83116
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    75
          "npm install --global " + if_proper(production, "--production ") + Bash.string(name)
83138
c66d77fb729e clarified signature: closer to regular bash();
wenzelm
parents: 83124
diff changeset
    76
        ), cwd = path).check
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    77
    }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    78
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    79
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    80
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    81
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    82
  /** source snippets **/
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    83
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    84
  /* require modules */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    85
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    86
  def require_module(name: JS.Source, module: JS.Source): JS.Source =
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    87
    name + " = require(" + module + ")"
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    88
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    89
  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
    90
    require_module(name, JS.platform_path(path, dir = dir))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    91
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    92
  def require_builtin(name: String): JS.Source =
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    93
    require_module("const " + name, JS.string(name))
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    94
76507
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
  /* file-system operations */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    97
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    98
  def require_fs: JS.Source = require_builtin("fs")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    99
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   100
  val encoding_utf8: JSON.T = JSON.Object("encoding" -> "utf8")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   101
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   102
  def read_file(path: Path): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   103
    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
   104
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   105
  def write_file(path: Path, arg: JS.Source): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   106
    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
   107
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   108
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   109
  /* external process */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   110
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   111
  def execute(js: String): Process_Result =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   112
    Isabelle_System.bash("isabelle node -", input = js,
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   113
      description = "Node.js").check
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   114
}