src/Pure/System/nodejs.scala
author wenzelm
Mon, 08 Sep 2025 22:43:15 +0200
changeset 83114 310f1c728ed2
parent 83108 75a5089dad12
child 83115 ee6a594f0e7e
permissions -rw-r--r--
more accurate treatment of 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
310f1c728ed2 more accurate treatment of Windows/MinGW;
wenzelm
parents: 83108
diff changeset
    80
    def install(name: String): Unit = {
83108
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    81
      progress.echo("Installing " + name + " ...")
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    82
      Isabelle_System.bash(path_setup + "\nnpm install -g " + Bash.string(name), cwd = path).check
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    83
    }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    84
  }
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    85
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    86
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
  /** source snippets **/
75a5089dad12 clarified signature and modules: more explicit Nodejs.setup;
wenzelm
parents: 76510
diff changeset
    89
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    90
  /* require modules */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    91
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    92
  def require_module(name: JS.Source, module: JS.Source): JS.Source =
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    93
    name + " = require(" + module + ")"
76507
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 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
    96
    require_module(name, JS.platform_path(path, dir = dir))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    97
76510
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    98
  def require_builtin(name: String): JS.Source =
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
    99
    require_module("const " + name, JS.string(name))
b0ad975cd25b clarified JS namespace;
wenzelm
parents: 76507
diff changeset
   100
76507
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
  /* file-system operations */
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 require_fs: JS.Source = require_builtin("fs")
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
  val encoding_utf8: JSON.T = JSON.Object("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
  def read_file(path: Path): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   109
    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
   110
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   111
  def write_file(path: Path, arg: JS.Source): JS.Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   112
    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
   113
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
  /* external process */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   116
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   117
  def execute(js: String): Process_Result =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   118
    Isabelle_System.bash("isabelle node -", input = js,
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   119
      description = "Node.js").check
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
   120
}