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,160 +1,123 @@ +/* Author: Lars Hupel and Fabian Huch, TU Muenchen + + + */ package afp -import isabelle._ +import isabelle.{Path, *} + +import java.io.File as JFile 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], + case class Check[T]( + name: String, failure_msg: String, - failure_format: T => String + run: (Sessions.Structure, List[String], AFP_Structure) => List[T], + failure_format: T => String = (t: T) => t.toString ) { - def apply(tree: Sessions.Structure, selected: List[String]): Boolean = - run(tree, selected) match { - case Nil => - true + override def toString: String = name + + def apply( + structure: Sessions.Structure, + sessions: List[String], + afp_structure: AFP_Structure + ): Boolean = + run(structure, sessions, afp_structure) 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 known_checks: List[Check[_]] = + List( + Check[String]("check_timeout", + "The following entries contain sessions without timeouts or with timeouts not divisible by 300:", + (structure, sessions, _) => + sessions.flatMap { session_name => + val info = structure(session_name) + val timeout = info.options.real("timeout") + if (timeout == 0 || timeout % 300 != 0) Some(session_name) else None + }), + Check[String]("check_chapter", "The following entries are not in the AFP chapter:", + (structure, sessions, _) => + sessions.flatMap { session_name => + val info = structure(session_name) + if (info.chapter != "AFP") Some(session_name) else None + }), + Check[(String, List[String])]("check_groups", "The following sessions have wrong groups:", + (structure, sessions, _) => + sessions.flatMap { session_name => + val info = structure(session_name) + if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") || + !info.groups.contains("AFP")) + Some((session_name, info.groups)) + else None + }, + t => t._1 + "{" + t._2.mkString(", ") + "}"), + Check[String]("check_presence", + "The following entries do not contain a corresponding session on top level:", + (structure, sessions, afp_structure) => { + val entries = afp_structure.entries_unchecked - 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 - ) + entries.flatMap { entry_name => + if (!sessions.contains(entry_name) || + structure(entry_name).dir.base.implode != entry_name) + Some(entry_name) + else None + } + }) + ).sortBy(_.name) - 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).filter(name => (afp_dir + Path.basic(name)).is_dir) + def the_check(name: String): Check[_] = + known_checks.find(check => check.name == name) getOrElse + error("Unkown check " + quote(name)) - fs_entries.filterNot(excludes.contains).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 - ) + def afp_check_roots(checks: List[Check[_]], afp_structure: AFP_Structure): Unit = { + val structure = afp_structure.sessions_structure + val sessions = structure.build_selection(Sessions.Selection.empty).sorted - List( - check_timeout, - // check_paths, - check_chapter, - check_groups, - check_presence) - } - - 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)) + val bad = checks.exists(check => !check(structure, sessions, afp_structure)) if (bad) { print_bad("Errors found.") System.exit(1) } else { - print_good(s"${selected.length} sessions have been checked") - print_good(s"${checks.length} checks have found no errors") + print_good(sessions.length.toString + " sessions have been checked") + print_good(checks.length.toString + " 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") + var checks: List[Check[_]] = known_checks val getopts = Getopts(""" Usage: isabelle afp_check_roots [OPTIONS] Options are: - -x NAME exclude directories with name - (default """ + excludes.map(quote).mkString(", ") + """) + -C NAMES checks (default: """ + known_checks.mkString("\"", ",", "\"") + """) Check ROOT files of AFP sessions. """, - "x:" -> (arg => excludes ::= arg)) + "C:" -> (arg => checks = Library.distinct(space_explode(',', arg)).map(the_check))) getopts(args) - val afp_dir = Path.explode("$AFP").expand + val afp_structure = AFP_Structure() - afp_check_roots(afp_dir, excludes) + afp_check_roots(checks, afp_structure) }) }