src/Pure/System/nodejs.scala
author wenzelm
Tue, 09 Sep 2025 17:39:04 +0200
changeset 83120 402f51de0347
parent 83116 e0c85cb6b924
child 83121 74a25a7c2481
permissions -rw-r--r--
clarified signature: just one class Directory is sufficient;
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
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    29
    val arch = if (platform.is_arm) "arm64" else "x64"
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)
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    41
      val node_dir = new Directory(platform_context, base_dir + Path.basic(full_name))
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
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    49
  class Directory private[Nodejs](
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    50
    val platform_context: Isabelle_Platform.Context,
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    51
    val path: Path
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    52
  ) {
83114
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    53
    def platform: Isabelle_Platform = platform_context.isabelle_platform
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    54
    def progress: Progress = platform_context.progress
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    55
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    56
    override def toString: String = path.file_name
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    57
83120
402f51de0347 clarified signature: just one class Directory is sufficient;
wenzelm
parents: 83116
diff changeset
    58
    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
    59
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    60
    def path_setup: String =
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    61
      "export PATH=" + Bash.string(platform_context.standard_path(bin_dir)) + """:"$PATH""""
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    62
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    63
    def install(name: String, production: Boolean = false): Unit = {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    64
      progress.echo("Installing " + name + " ...")
83116
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    65
      platform_context.execute(path,
83115
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    66
        Library.make_lines(
ee6a594f0e7e clarified signature: more options;
wenzelm
parents: 83114
diff changeset
    67
          path_setup,
83116
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    68
          "npm install --global " + if_proper(production, "--production ") + Bash.string(name)
e0c85cb6b924 proper platform_context.execute for Windows/MinGW;
wenzelm
parents: 83115
diff changeset
    69
        )).check
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    70
    }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    71
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    72
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    73
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    74
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    75
  /** source snippets **/
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    76
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    77
  /* require modules */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    78
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    79
  def require_module(name: JS.Source, module: JS.Source): JS.Source =
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    80
    name + " = require(" + module + ")"
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    81
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    82
  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
    83
    require_module(name, JS.platform_path(path, dir = dir))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    84
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    85
  def require_builtin(name: String): JS.Source =
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    86
    require_module("const " + name, JS.string(name))
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    87
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
  /* file-system operations */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    90
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    91
  def require_fs: JS.Source = require_builtin("fs")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    92
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    93
  val encoding_utf8: JSON.T = JSON.Object("encoding" -> "utf8")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    94
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    95
  def read_file(path: Path): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    96
    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
    97
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    98
  def write_file(path: Path, arg: JS.Source): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    99
    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
   100
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
  /* external process */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   103
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   104
  def execute(js: String): Process_Result =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   105
    Isabelle_System.bash("isabelle node -", input = js,
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   106
      description = "Node.js").check
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   107
}