src/Pure/System/cygwin.scala
author wenzelm
Mon, 28 Jun 2021 13:45:46 +0200
changeset 73890 8f6b2eb15240
parent 73340 0ffcad1f6130
child 73892 2847a3deedf9
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62058
1cfd5d604937 updated headers;
wenzelm
parents: 61293
diff changeset
     1
/*  Title:      Pure/System/cygwin.scala
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     3
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     4
Cygwin as POSIX emulation on Windows.
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     5
*/
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     6
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     7
package isabelle
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     8
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
     9
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile}
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    11
import java.nio.file.Files
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    12
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    13
import scala.annotation.tailrec
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    14
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    15
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    16
object Cygwin
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    17
{
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    18
  /* init (e.g. after extraction via 7zip) */
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    19
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
    20
  def init(isabelle_root: String, cygwin_root: String): Unit =
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    21
  {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 69402
diff changeset
    22
    require(Platform.is_windows, "Windows platform expected")
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    23
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
    24
    def exec(cmdline: String*): Unit =
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    25
    {
61293
876e7eae22be clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents: 61291
diff changeset
    26
      val cwd = new JFile(isabelle_root)
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62291
diff changeset
    27
      val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
73890
8f6b2eb15240 clarified modules;
wenzelm
parents: 73340
diff changeset
    28
      val proc = Isabelle_Env.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
8f6b2eb15240 clarified modules;
wenzelm
parents: 73340
diff changeset
    29
      val (output, rc) = Isabelle_Env.process_output(proc)
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    30
      if (rc != 0) error(output)
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    31
    }
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    32
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    33
    val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    34
    val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    35
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    36
    if (uninitialized) {
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    37
      val symlinks =
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    38
      {
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    39
        val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    40
        Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    41
      }
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    42
      @tailrec def recover_symlinks(list: List[String]): Unit =
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    43
      {
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    44
        list match {
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    45
          case Nil | List("") =>
69402
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    46
          case target :: content :: rest =>
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    47
            link(content, new JFile(isabelle_root, target))
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    48
            recover_symlinks(rest)
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    49
          case _ => error("Unbalanced symlinks list")
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    50
        }
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    51
      }
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    52
      recover_symlinks(symlinks)
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    53
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62291
diff changeset
    54
      exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62291
diff changeset
    55
      exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    56
    }
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    57
  }
69402
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    58
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
    59
  def link(content: String, target: JFile): Unit =
69402
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    60
  {
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    61
    val target_path = target.toPath
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    62
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    63
    using(Files.newBufferedWriter(target_path, UTF8.charset))(
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    64
      _.write("!<symlink>" + content + "\u0000"))
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    65
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    66
    Files.setAttribute(target_path, "dos:system", true)
61f4c406d727 more direct File.link operation: avoid external process;
wenzelm
parents: 69393
diff changeset
    67
  }
61282
3e578ddef85d clarified Isabelle_System.init;
wenzelm
parents:
diff changeset
    68
}