diff --git a/tools/afp_check_roots.scala b/tools/afp_check_roots.scala --- a/tools/afp_check_roots.scala +++ b/tools/afp_check_roots.scala @@ -1,170 +1,160 @@ package afp import isabelle._ -object AFP_Check_Roots -{ +object AFP_Check_Roots { def print_good(string: String): Unit = println(Console.BOLD + Console.GREEN + string + Console.RESET) def print_bad(string: String): Unit = println(Console.BOLD + Console.RED + string + Console.RESET) class Check[T]( run: (Sessions.Structure, List[String]) => List[T], failure_msg: String, - failure_format: T => String) - { + failure_format: T => String + ) { def apply(tree: Sessions.Structure, selected: List[String]): Boolean = run(tree, selected) match { case Nil => true case offenders => print_bad(failure_msg) offenders.foreach(offender => println(" " + failure_format(offender))) false } } def afp_checks(afp_dir: Path, excludes: List[String]): List[Check[_]] = { val check_timeout = new Check[(String, List[String])]( run = { (tree, selected) => selected.flatMap { name => val info = tree(name) val entry = info.dir.base.implode val timeout = info.options.real("timeout") if (timeout == 0 || timeout % 300 != 0) Some((entry, name)) else None }.groupBy(_._1).view.mapValues(_.map(_._2)).toList }, failure_msg = "The following entries contain sessions without timeouts or with timeouts not divisible by 300:", failure_format = { case (entry, sessions) => s"""$entry ${sessions.mkString("(", ", ", ")")}""" } ) val check_paths = new Check[(String, Path)]( run = { (tree, selected) => selected.flatMap { name => val info = tree(name) val dir = info.dir if (dir.dir.expand.file != afp_dir.file) Some((name, dir)) else None } }, failure_msg = "The following sessions are in the wrong directory:", failure_format = { case (session, dir) => s"""$session ($dir)""" } ) val check_chapter = new Check[String]( run = { (tree, selected) => selected.flatMap { name => val info = tree(name) val entry = info.dir.base.implode if (info.chapter != "AFP") Some(entry) else None }.distinct }, failure_msg = "The following entries are not in the AFP chapter:", failure_format = identity ) val check_groups = new Check[(String, List[String])]( run = { (tree, selected) => selected.flatMap { name => val info = tree(name) if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") || !info.groups.contains("AFP")) Some((name, info.groups)) else None } }, failure_msg = "The following sessions have wrong groups:", failure_format = { case (session, groups) => s"""$session ${groups.mkString("{", ", ", "}")}""" } ) val check_presence = new Check[String]( run = { (tree, selected) => val fs_entries = File.read_dir(afp_dir).filterNot(excludes.contains) fs_entries.flatMap { name => if (!selected.contains(name) || tree(name).dir.base.implode != name) Some(name) else None } }, failure_msg = "The following entries (according to the file system) are not registered in ROOTS, or registered in the wrong ROOT:", failure_format = identity ) List( check_timeout, // check_paths, check_chapter, check_groups, check_presence) } - def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit = - { + def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit = { val full_tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir)) val selected = full_tree.build_selection(Sessions.Selection.empty) val checks = afp_checks(afp_dir, excludes) val bad = checks.exists(check => !check(full_tree, selected)) - if (bad) - { + if (bad) { print_bad("Errors found.") System.exit(1) } - else - { + else { print_good(s"${selected.length} sessions have been checked") print_good(s"${checks.length} checks have found no errors") } } - val isabelle_tool = - Isabelle_Tool( - "afp_check_roots", - "check ROOT files of AFP sessions", - Scala_Project.here, - args => { - var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc") + val isabelle_tool = Isabelle_Tool("afp_check_roots", "check ROOT files of AFP sessions", + Scala_Project.here, + { args => + var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc") - val getopts = Getopts( - """ + val getopts = Getopts(""" Usage: isabelle afp_check_roots [OPTIONS] Options are: -x NAME exclude directories with name (default """ + excludes.map(quote).mkString(", ") + """) Check ROOT files of AFP sessions. """, - "x:" -> (arg => excludes ::= arg) - ) - - getopts(args) + "x:" -> (arg => excludes ::= arg)) - val afp_dir = Path.explode("$AFP").expand + getopts(args) - afp_check_roots(afp_dir, excludes) - } - ) + val afp_dir = Path.explode("$AFP").expand + + afp_check_roots(afp_dir, excludes) + }) } diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala --- a/tools/afp_dependencies.scala +++ b/tools/afp_dependencies.scala @@ -1,92 +1,86 @@ /* Author: Fabian Huch, TU Muenchen Tool to extract dependencies of AFP entries. */ package afp import Metadata.Entry import isabelle._ object AFP_Dependencies { case class Dependency(entry: Entry.Name, distrib_deps: List[Entry.Name], afp_deps: List[Entry.Name]) object JSON { private def from_dep(dependency: Dependency): (String, isabelle.JSON.T) = dependency.entry -> isabelle.JSON.Object( "distrib_deps" -> dependency.distrib_deps, "afp_deps" -> dependency.afp_deps ) def from_dependency(dep: Dependency): isabelle.JSON.T = isabelle.JSON.Object(from_dep(dep)) def from_dependencies(deps: List[Dependency]): isabelle.JSON.T = deps.map(from_dep).toMap } def afp_dependencies(afp_dir: Path): List[Dependency] = { val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir)) val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil)) .build_graph.keys def get_entry(name: String): Option[String] = { val info = tree(name) val dir = info.dir if (selected.contains(dir.dir.expand)) None else Some(dir.base.implode) } selected.groupBy(get_entry).toList.collect { case (Some(e), sessions) => val dependencies = sessions.flatMap(tree.imports_graph.imm_preds) .map(d => (d, get_entry(d))) val distrib_deps = dependencies.collect { case (d, None) => d }.distinct val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct Dependency(e, distrib_deps, afp_deps) } } - val isabelle_tool = - Isabelle_Tool( - "afp_dependencies", - "extract dependencies between AFP entries", - Scala_Project.here, - args => { - var output_file: Option[Path] = None + val isabelle_tool = Isabelle_Tool("afp_dependencies", "extract dependencies between AFP entries", + Scala_Project.here, + { args => + var output_file: Option[Path] = None - val getopts = Getopts( - """ + val getopts = Getopts(""" Usage: isabelle afp_dependencies [OPTIONS] Options are: -o FILE output file name Extract dependencies between AFP entries. """, - "o:" -> (arg => output_file = Some(Path.explode(arg))) - ) - - getopts(args) - val afp_dir = Path.explode("$AFP").expand - - val progress = new Console_Progress() + "o:" -> (arg => output_file = Some(Path.explode(arg)))) - val res = afp_dependencies(afp_dir).map(JSON.from_dependency) - val json = isabelle.JSON.Format(res) + getopts(args) + val afp_dir = Path.explode("$AFP").expand - output_file match { - case Some(file) => File.write(file, json) - case None => progress.echo(json) - } + val progress = new Console_Progress() + + val res = afp_dependencies(afp_dir).map(JSON.from_dependency) + val json = isabelle.JSON.Format(res) + + output_file match { + case Some(file) => File.write(file, json) + case None => progress.echo(json) } - ) + }) }