src/Pure/Admin/sync_repos.scala
author wenzelm
Tue, 07 Jun 2022 19:15:08 +0200
changeset 75536 7cdeed5dc96d
parent 75525 68162e4f60a7
permissions -rw-r--r--
more robust treatment of rsync on macOS (see also 96fb1f9a4042);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/sync_repos.scala
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     3
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     4
Synchronize Isabelle + AFP repositories.
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     5
*/
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     6
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     7
package isabelle
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     8
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
     9
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    10
object Sync_Repos {
75525
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    11
  def sync_repos(context: Rsync.Context, target: String,
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    12
    verbose: Boolean = false,
75487
167660a8f99e support thorough check of file content;
wenzelm
parents: 75486
diff changeset
    13
    thorough: Boolean = false,
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    14
    preserve_jars: Boolean = false,
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    15
    dry_run: Boolean = false,
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    16
    rev: String = "",
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    17
    afp_root: Option[Path] = None,
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    18
    afp_rev: String = ""
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    19
  ): Unit = {
75506
ee51db628e71 clarified signature;
wenzelm
parents: 75499
diff changeset
    20
    val hg = Mercurial.self_repository()
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    21
    val afp_hg = afp_root.map(Mercurial.repository(_))
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    22
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    23
    val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    24
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    25
    def sync(hg: Mercurial.Repository, dest: String, r: String,
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    26
      contents: List[File.Content] = Nil, filter: List[String] = Nil
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    27
    ): Unit = {
75525
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    28
      hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    29
        contents = contents, filter = filter ::: more_filter)
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    30
    }
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    31
75525
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    32
    context.progress.echo_if(verbose, "\n* Isabelle repository:")
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    33
    sync(hg, target, rev,
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    34
      contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    35
      filter = List("protect /AFP"))
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    36
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    37
    for (hg <- afp_hg) {
75525
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    38
      context.progress.echo_if(verbose, "\n* AFP repository:")
75524
ff8012edac89 clarified signature;
wenzelm
parents: 75523
diff changeset
    39
      sync(hg, Rsync.append(target, "AFP"), afp_rev)
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    40
    }
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    41
  }
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    42
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    43
  val isabelle_tool =
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    44
    Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    45
      Scala_Project.here, { args =>
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    46
        var afp_root: Option[Path] = None
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    47
        var preserve_jars = false
75536
7cdeed5dc96d more robust treatment of rsync on macOS (see also 96fb1f9a4042);
wenzelm
parents: 75525
diff changeset
    48
        var protect_args = false
75487
167660a8f99e support thorough check of file content;
wenzelm
parents: 75486
diff changeset
    49
        var thorough = false
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    50
        var afp_rev = ""
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    51
        var dry_run = false
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    52
        var rev = ""
75499
c635368021b6 support explicit SSH port;
wenzelm
parents: 75497
diff changeset
    53
        var port = SSH.default_port
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    54
        var verbose = false
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    55
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    56
        val getopts = Getopts("""
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    57
Usage: isabelle sync_repos [OPTIONS] TARGET
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    58
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    59
  Options are:
75497
0a5f7b5da16f clarified options;
wenzelm
parents: 75493
diff changeset
    60
    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    61
    -J           preserve *.jar files
75536
7cdeed5dc96d more robust treatment of rsync on macOS (see also 96fb1f9a4042);
wenzelm
parents: 75525
diff changeset
    62
    -S           robust (but less portable) treatment of spaces in directory names
75493
f775dfb55655 clarified option -T;
wenzelm
parents: 75492
diff changeset
    63
    -T           thorough treatment of file content and directory times
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    64
    -a REV       explicit AFP revision (default: state of working directory)
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    65
    -n           no changes: dry-run
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    66
    -r REV       explicit revision (default: state of working directory)
75499
c635368021b6 support explicit SSH port;
wenzelm
parents: 75497
diff changeset
    67
    -p PORT      explicit SSH port (default: """ + SSH.default_port + """)
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    68
    -v           verbose
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    69
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    70
  Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
75486
ba4ed9a50be3 more documentation;
wenzelm
parents: 75485
diff changeset
    71
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    72
  Example: quick testing
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    73
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    74
    isabelle sync_repos -A: -J testmachine:test/isabelle_afp
75486
ba4ed9a50be3 more documentation;
wenzelm
parents: 75485
diff changeset
    75
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    76
  Example: accurate testing
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    77
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
    78
    isabelle sync_repos -A: -T testmachine:test/isabelle_afp
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    79
""",
75497
0a5f7b5da16f clarified options;
wenzelm
parents: 75493
diff changeset
    80
          "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
75492
c03c2bf4ef8a preserve jars for quick testing;
wenzelm
parents: 75491
diff changeset
    81
          "J" -> (_ => preserve_jars = true),
75536
7cdeed5dc96d more robust treatment of rsync on macOS (see also 96fb1f9a4042);
wenzelm
parents: 75525
diff changeset
    82
          "S" -> (_ => protect_args = true),
75487
167660a8f99e support thorough check of file content;
wenzelm
parents: 75486
diff changeset
    83
          "T" -> (_ => thorough = true),
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    84
          "a:" -> (arg => afp_rev = arg),
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    85
          "n" -> (_ => dry_run = true),
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    86
          "r:" -> (arg => rev = arg),
75499
c635368021b6 support explicit SSH port;
wenzelm
parents: 75497
diff changeset
    87
          "p:" -> (arg => port = Value.Int.parse(arg)),
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    88
          "v" -> (_ => verbose = true))
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    89
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    90
        val more_args = getopts(args)
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    91
        val target =
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    92
          more_args match {
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    93
            case List(target) => target
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    94
            case _ => getopts.usage()
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    95
          }
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    96
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
    97
        val progress = new Console_Progress
75536
7cdeed5dc96d more robust treatment of rsync on macOS (see also 96fb1f9a4042);
wenzelm
parents: 75525
diff changeset
    98
        val context = Rsync.Context(progress, port = port, protect_args = protect_args)
75525
68162e4f60a7 clarified signature: more explicit type Rsync.Context;
wenzelm
parents: 75524
diff changeset
    99
        sync_repos(context, target, verbose = verbose, thorough = thorough,
75511
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
   100
          preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
b32fdb67f851 provide .hg_sync meta data;
wenzelm
parents: 75509
diff changeset
   101
          afp_rev = afp_rev)
75481
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
   102
      }
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
   103
    )
029cd4e1a2c7 support to synchronize Isabelle + AFP repositories;
wenzelm
parents:
diff changeset
   104
}