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,149 +1,149 @@ /* Author: Lars Hupel and Fabian Huch, TU Muenchen */ package afp 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) case class Check[T]( name: String, failure_msg: String, run: (Sessions.Structure, List[String], AFP_Structure) => List[T], failure_format: T => String = (t: T) => t.toString ) { 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 } } 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 entries.flatMap { entry_name => if (!sessions.contains(entry_name) || structure(entry_name).dir.base.implode != entry_name) Some(entry_name) else None } }), Check[(String, List[Path])]("check_unused_thys", "The following sessions contain unused theories:", (structure, sessions, afp_structure) => { - val thys_dir = afp_structure.thys_dir val selection = Sessions.Selection(sessions = sessions) val deps = structure.selection_deps(selection = selection) def rel_path(path: Path): Path = File.relative_path(afp_structure.thys_dir.absolute, path.absolute).get def is_thy_file(file: JFile): Boolean = file.isFile && file.getName.endsWith(".thy") - sessions.flatMap { session_name => - val theory_nodes = deps.base_info(session_name).base.proper_session_theories - val session_thy_files = theory_nodes.map(node => rel_path(node.path)) + afp_structure.entries.flatMap { entry => + val sessions = afp_structure.entry_sessions(entry).map(_.name) + val theory_nodes = sessions.flatMap(deps.base_info(_).base.proper_session_theories) + val thy_files = theory_nodes.map(node => rel_path(node.path)) - val dir = structure(session_name).dir - val physical_files = File.find_files(dir.file, is_thy_file, include_dirs = true).map( - file => rel_path(Path.explode(file.getAbsolutePath))) + val entry_dir = afp_structure.entry_thy_dir(entry) + val physical_files = File.find_files(entry_dir.file, is_thy_file, include_dirs = true) + val rel_files = physical_files.map(file => rel_path(Path.explode(file.getAbsolutePath))) - val unused = physical_files.toSet -- session_thy_files.toSet - if (unused.nonEmpty) Some(session_name -> unused.toList) + val unused = rel_files.toSet -- thy_files.toSet + if (unused.nonEmpty) Some(entry -> unused.toList) else None } }, t => t._1 + ": {" + t._2.mkString((", ")) + "}") ).sortBy(_.name) def the_check(name: String): Check[_] = known_checks.find(check => check.name == name) getOrElse error("Unkown check " + quote(name)) 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 val bad = checks.exists(check => !check(structure, sessions, afp_structure)) if (bad) { print_bad("Errors found.") System.exit(1) } else { 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 checks: List[Check[_]] = known_checks val getopts = Getopts(""" Usage: isabelle afp_check_roots [OPTIONS] Options are: -C NAMES checks (default: """ + known_checks.mkString("\"", ",", "\"") + """) Check ROOT files of AFP sessions. """, "C:" -> (arg => checks = Library.distinct(space_explode(',', arg)).map(the_check))) getopts(args) val afp_structure = AFP_Structure() afp_check_roots(checks, afp_structure) }) } diff --git a/tools/afp_structure.scala b/tools/afp_structure.scala --- a/tools/afp_structure.scala +++ b/tools/afp_structure.scala @@ -1,128 +1,130 @@ /* Author: Fabian Huch, TU Muenchen AFP Metadata file structure with save and load operations. */ package afp import isabelle._ class AFP_Structure private(val base_dir: Path) { /* files */ val metadata_dir = base_dir + Path.basic("metadata") val thys_dir = base_dir + Path.basic("thys") + def entry_thy_dir(name: Metadata.Entry.Name): Path = thys_dir + Path.basic(name) + val authors_file = metadata_dir + Path.basic("authors.toml") val releases_file = metadata_dir + Path.basic("releases.toml") val licenses_file = metadata_dir + Path.basic("licenses.toml") val topics_file = metadata_dir + Path.basic("topics.toml") val entries_dir = metadata_dir + Path.basic("entries") def entry_file(name: Metadata.Entry.Name): Path = entries_dir + Path.basic(name + ".toml") /* load */ private def load[A](file: Path, parser: afp.TOML.T => A): A = { val content = File.read(file) val toml = try { TOML.parse(content) } catch { case ERROR(msg) => error("Could not parse " + file.toString + ": " + msg) } parser(toml) } def load_authors: List[Metadata.Author] = load(authors_file, Metadata.TOML.to_authors) def load_releases: List[Metadata.Release] = load(releases_file, Metadata.TOML.to_releases) def load_licenses: List[Metadata.License] = load(licenses_file, Metadata.TOML.to_licenses) def load_topics: List[Metadata.Topic] = load(topics_file, Metadata.TOML.to_topics) def load_entry(name: Metadata.Entry.Name, authors: Map[Metadata.Author.ID, Metadata.Author], topics: Map[Metadata.Topic.ID, Metadata.Topic], licenses: Map[Metadata.License.ID, Metadata.License], releases: Map[Metadata.Entry.Name, List[Metadata.Release]] ): Metadata.Entry = { val entry_releases = releases.getOrElse(name, Nil) load(entry_file(name), toml => Metadata.TOML.to_entry(name, toml, authors, topics, licenses, entry_releases)) } def load(): List[Metadata.Entry] = { val authors = load_authors.map(author => author.id -> author).toMap val topics = Utils.grouped_sorted(load_topics.flatMap(_.all_topics), (t: Metadata.Topic) => t.id) val licenses = load_licenses.map(license => license.id -> license).toMap val releases = load_releases.groupBy(_.entry) entries.map(name => load_entry(name, authors, topics, licenses, releases)) } /* save */ private def save(file: Path, content: afp.TOML.T): Unit = { file.dir.file.mkdirs() File.write(file, TOML.Format(content)) } def save_authors(authors: List[Metadata.Author]): Unit = save(authors_file, Metadata.TOML.from_authors(authors)) def save_releases(releases: List[Metadata.Release]): Unit = save(releases_file, Metadata.TOML.from_releases(releases)) def save_topics(topics: List[Metadata.Topic]): Unit = save(topics_file, Metadata.TOML.from_topics(topics)) def save_entry(entry: Metadata.Entry): Unit = save(entry_file(entry.name), Metadata.TOML.from_entry(entry)) /* sessions */ def entries_unchecked: List[Metadata.Entry.Name] = { val Entry = """([a-zA-Z0-9+_-]+)\.toml""".r File.read_dir(entries_dir).map { case Entry(name) => name case f => error("Unrecognized file in metadata: " + f) } } def entries: List[Metadata.Entry.Name] = { val session_entries = Sessions.parse_roots(thys_dir + Path.basic("ROOTS")) val session_set = session_entries.toSet val metadata_set = entries_unchecked.toSet if (session_set != metadata_set) { val inter = session_set.intersect(metadata_set) val session_without_metadata = if (session_set.subsetOf(inter)) "" else "No metadata for session in ROOTS: " + commas_quote(session_set -- inter) val metadata_without_session = if (metadata_set.subsetOf(inter)) "" else "Metadata entries missing in ROOTS: " + commas_quote(metadata_set -- inter) error("Metadata does not match sessions:\n" + session_without_metadata + metadata_without_session) } else session_entries } def sessions_structure: Sessions.Structure = Sessions.load_structure(options = Options.init(), select_dirs = List(thys_dir)) def entry_sessions(name: Metadata.Entry.Name): List[Sessions.Session_Entry] = Sessions.parse_root(thys_dir + Path.make(List(name, "ROOT"))).collect { case e: Sessions.Session_Entry => e } def hg_id: String = Mercurial.repository(base_dir).id() } object AFP_Structure { def apply(base_dir: Path = Path.explode("$AFP_BASE")): AFP_Structure = new AFP_Structure(base_dir.absolute) }