diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala --- a/tools/afp_dependencies.scala +++ b/tools/afp_dependencies.scala @@ -1,91 +1,95 @@ +/* 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.map { 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 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() 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) } } ) } diff --git a/tools/afp_site_gen.scala b/tools/afp_site_gen.scala --- a/tools/afp_site_gen.scala +++ b/tools/afp_site_gen.scala @@ -1,296 +1,300 @@ +/* Author: Fabian Huch, TU Muenchen + +Generation and compilation of SSG project for the AFP website. + */ package afp import isabelle._ object AFP_Site_Gen { /* json */ object JSON { type T = isabelle.JSON.T object Object { type T = isabelle.JSON.Object.T } def from_authors(authors: List[Metadata.Author]): T = { authors.map(author => author.id -> isabelle.JSON.Object( "name" -> author.name, "emails" -> author.emails.map(_.address), "homepages" -> author.homepages.map(_.url))).toMap } def from_topics(topics: List[Metadata.Topic]): T = Metadata.TOML.from_topics(topics) def from_affiliations(affiliations: List[Metadata.Affiliation]): Object.T = { Utils.group_sorted(affiliations, (a: Metadata.Affiliation) => a.author).view.mapValues(author_affiliations => { val homepage = author_affiliations.collectFirst { case Metadata.Homepage(_, _, url) => url } val email = author_affiliations.collectFirst { case Metadata.Email(_, _, address) => address } isabelle.JSON.Object( homepage.map(s => List("homepage" -> s)).getOrElse(Nil) ::: email.map(s => List("email" -> s)).getOrElse(Nil): _*) }).toMap } def from_change_history(history: Metadata.Change_History): Object.T = { if (history.isEmpty) { Map.empty } else { Map("Change history" -> history.map { case (date, str) => "[" + date.toString + "] " + str }.mkString("\n")) } } def from_entry(entry: Metadata.Entry): JSON.Object.T = isabelle.JSON.Object( "title" -> entry.title :: "authors" -> entry.authors.map(_.author).distinct :: "affiliations" -> from_affiliations(entry.authors ++ entry.contributors) :: (if (entry.contributors.nonEmpty) "contributors" -> entry.contributors.map(_.author).distinct :: Nil else Nil) ::: "date" -> entry.date.toString :: "topics" -> entry.topics.map(_.id) :: "abstract" -> entry.`abstract` :: "license" -> entry.license.name :: (if (entry.releases.nonEmpty) "releases" -> entry.releases.map(r => r.isabelle -> r.date.toString).toMap :: Nil else Nil) ::: (if (entry.note.nonEmpty) "note" -> entry.note :: Nil else Nil) ::: (if (entry.change_history.nonEmpty || entry.extra.nonEmpty) "extra" -> (from_change_history(entry.change_history) ++ entry.extra) :: Nil else Nil): _*) def from_keywords(keywords: List[String]): T = keywords.zipWithIndex.map { case (keyword, i) => isabelle.JSON.Object("id" -> i, "keyword" -> keyword) } } /* keyword extraction */ private val replacements = List( "<[^>]*>".r -> "", "[^\\w\\s()'.,;:-]".r -> " ", "\\s+".r -> " ") def extract_keywords(text: String): List[String] = { val stripped_text = replacements.foldLeft(text) { case (res, (regex, replacement)) => regex.replaceAllIn(res, replacement) } val arg = quote(stripped_text.replaceAll("\"", "\\\"")) val keyword_cmd = "from keywords import *; print_keywords(" + arg + ")" Python.run(keyword_cmd).check.out_lines } /* site generation */ def afp_site_gen( out_dir: Option[Path], layout: Hugo.Layout, status_file: Option[Path], afp_structure: AFP_Structure, progress: Progress = new Progress()): Unit = { /* add authors */ progress.echo("Preparing authors...") val authors = afp_structure.load_authors val authors_by_id = Utils.grouped_sorted(authors, (a: Metadata.Author) => a.id) layout.write_data(Path.basic("authors.json"), JSON.from_authors(authors)) /* add topics */ progress.echo("Preparing topics...") val topics = afp_structure.load_topics def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] = topic :: topic.sub_topics.flatMap(sub_topics) val topics_by_id = Utils.grouped_sorted(topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id) layout.write_data(Path.basic("topics.json"), JSON.from_topics(topics)) /* add licenses */ progress.echo("Preparing licenses...") val licenses_by_id = Utils.grouped_sorted(afp_structure.load_licenses, (l: Metadata.License) => l.id) /* add releases */ progress.echo("Preparing releases...") val releases_by_entry = afp_structure.load_releases.groupBy(_.entry) /* extract keywords */ progress.echo("Extracting keywords...") var seen_keywords = Set.empty[String] val entry_keywords = afp_structure.entries.map(name => { val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, licenses_by_id, releases_by_entry) val Keyword = """\('([^']*)', ([^)]*)\)""".r val scored_keywords = extract_keywords(entry.`abstract`).map { case Keyword(keyword, score) => keyword -> score.toDouble case s => error("Could not parse: " + s) } seen_keywords ++= scored_keywords.map(_._1) name -> scored_keywords.filter(_._2 > 1.0).map(_._1) }).toMap seen_keywords = seen_keywords.filter(k => !k.endsWith("s") || !seen_keywords.contains(k.stripSuffix("s"))) layout.write_static(Path.make(List("data", "keywords.json")), JSON.from_keywords(seen_keywords.toList)) def get_keywords(name: Metadata.Entry.Name): List[String] = entry_keywords(name).filter(seen_keywords.contains).take(8) /* add entries and theory listings */ progress.echo("Preparing entries...") val sessions_structure = afp_structure.sessions_structure val sessions_deps = Sessions.deps(sessions_structure) for (name <- afp_structure.entries) { val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, licenses_by_id, releases_by_entry) val deps = for { session <- afp_structure.entry_sessions(name) dep <- sessions_structure.imports_graph.imm_preds(session.name) if session.name != dep && sessions_structure(dep).groups.contains("AFP") } yield dep val topo_theories = for { session <- afp_structure.entry_sessions(name) base = sessions_deps(session.name) node <- base.session_theories } yield node.theory_base_name val entry_json = JSON.from_entry(entry) ++ isabelle.JSON.Object( "dependencies" -> deps.distinct, "theories" -> topo_theories, "url" -> ("/entries/" + name + ".html"), "keywords" -> get_keywords(name)) val theories_json = isabelle.JSON.Object( "title" -> entry.title, "url" -> ("/entries/" + name.toLowerCase + "/theories"), "theories" -> topo_theories) layout.write_content(Path.make(List("entries", name + ".md")), entry_json) layout.write_content(Path.make(List("theories", name + ".md")), theories_json) } /* add statistics */ progress.echo("Preparing statistics...") val statistics_cmd = "from statistics import *; add_statistics(" + commas_quote( List( Path.explode("$AFP_BASE").absolute.implode, Path.explode("$AFP").absolute.implode, layout.data_dir.implode)) + ")" Python.run(statistics_cmd).check (layout.data_dir + Path.basic("statistics.html")).file.delete() /* project */ progress.echo("Preparing project files") layout.copy_project() /* status */ status_file match { case Some(status_file) => progress.echo("Preparing devel version...") val status_json = isabelle.JSON.parse(File.read(status_file)) layout.write_data(Path.basic("status.json"), status_json) case None => } /* hugo */ out_dir match { case Some(out_dir) => progress.echo("Building site...") Hugo.build(layout, out_dir).check progress.echo("Finished building site") case None => progress.echo("Finished sitegen preparation.") } } val isabelle_tool = Isabelle_Tool("afp_site_gen", "generates afp website source", Scala_Project.here, args => { var base_dir = Path.explode("$AFP_BASE") var hugo_dir = base_dir + Path.make(List("web", "hugo")) var status_file: Option[Path] = None var out_dir: Option[Path] = None val getopts = Getopts(""" Usage: isabelle afp_site_gen [OPTIONS] Options are: -B DIR afp base dir (default """" + base_dir.implode + """") -H DIR generated hugo project dir (default """" + hugo_dir.implode + """") -D FILE build status file for devel version -O DIR output dir for optional build (default none) Generates the AFP website source. HTML files of entries are dynamically loaded. Providing a status file will build the development version of the archive. Site will be built from generated source if output dir is specified. """, "B:" -> (arg => base_dir = Path.explode(arg)), "H:" -> (arg => hugo_dir = Path.explode(arg)), "D:" -> (arg => status_file = Some(Path.explode(arg))), "O:" -> (arg => out_dir = Some(Path.explode(arg)))) getopts(args) val afp_structure = AFP_Structure(base_dir) val layout = Hugo.Layout(hugo_dir) val progress = new Console_Progress() progress.echo("Preparing site generation in " + hugo_dir.implode) afp_site_gen(out_dir = out_dir, layout = layout, status_file = status_file, afp_structure = afp_structure, progress = progress) }) } \ No newline at end of file diff --git a/tools/afp_structure.scala b/tools/afp_structure.scala --- a/tools/afp_structure.scala +++ b/tools/afp_structure.scala @@ -1,114 +1,118 @@ +/* Author: Fabian Huch, TU Muenchen + +AFP Metadata file structure with save and load operations. + */ package afp import isabelle._ class AFP_Structure private(base_dir: Path) { /* files */ private val metadata_dir = base_dir + Path.basic("metadata") private val thys_dir = base_dir + Path.basic("thys") private val authors_file = metadata_dir + Path.basic("authors.toml") private val releases_file = metadata_dir + Path.basic("releases.toml") private val licenses_file = metadata_dir + Path.basic("licenses.toml") private val topics_file = metadata_dir + Path.basic("topics.toml") private val entries_dir = metadata_dir + Path.basic("entries") private 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 = TOML.parse(content) 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, error("No releases for entry " + name)) load(entry_file(name), toml => Metadata.TOML.to_entry(toml ++ TOML.T("name" -> name), authors, topics, licenses, entry_releases)) } /* save */ private def save(file: Path, content: afp.TOML.T): Unit = { file.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: List[Metadata.Entry.Name] = { val Entry = """([a-zA-Z0-9+_-]+)\.toml""".r val file_entries = File.read_dir(entries_dir).map { case Entry(name) => name case f => error("Unrecognized metadata entry: " + f) } val session_entries = Sessions.parse_roots(thys_dir + Path.basic("ROOTS")) val session_set = session_entries.toSet val metadata_set = file_entries.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 roots: " + commas_quote(session_set -- inter) val metadata_without_session = if (metadata_set.subsetOf(inter)) "" else "Not session roots for metadata entries: " + 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 } } object AFP_Structure { def apply(base_dir: Path = Path.explode("$AFP_BASE")): AFP_Structure = new AFP_Structure(base_dir.absolute) } diff --git a/tools/hugo.scala b/tools/hugo.scala --- a/tools/hugo.scala +++ b/tools/hugo.scala @@ -1,79 +1,83 @@ +/* Author: Fabian Huch, TU Muenchen + +AFP Hugo wrapper and project layout. + */ package afp import isabelle._ object Hugo { val hugo_home = Isabelle_System.getenv("ISABELLE_HUGO") val hugo_static = Path.explode("$AFP_BASE") + Path.make(List("admin", "site")) class Layout private(private[Hugo] val src_dir: Path) { private def write(file: Path, content: String): Unit = { val path = src_dir + file if (!path.dir.file.exists()) path.dir.file.mkdirs() File.write(path, content) } val data_dir = src_dir + Path.basic("data") def write_data(file: Path, content: JSON.T): Unit = write(Path.basic("data") + file, isabelle.JSON.Format(content)) val content_dir = src_dir + Path.basic("content") def write_content(file: Path, content: JSON.T): Unit = write(Path.basic("content") + file, isabelle.JSON.Format(content)) val static_dir = src_dir + Path.basic("static") def write_static(file: Path, content: JSON.T): Unit = write(Path.basic("static") + file, isabelle.JSON.Format(content)) def copy_project(): Unit = { if (hugo_static.canonical != src_dir) { for { file <- List( List("content", "_index.md"), List("content", "about.md"), List("content", "submission.md"), List("content", "download.md"), List("content", "help.md"), List("content", "search.md"), List("content", "statistics.md"), List("content", "submission.md"), List("themes"), List("config.json")) } Isabelle_System.copy_dir(hugo_static + Path.make(file), src_dir + Path.make(file)) } } } object Layout { def apply(src_dir: Path = Path.explode("$AFP_BASE") + Path.make(List("web", "hugo"))): Layout = new Layout(src_dir.canonical) } private lazy val exec = Path.explode(proper_string(hugo_home).getOrElse(error("No hugo component found"))) + Path.basic("hugo") def build(layout: Layout, out_dir: Path = Path.explode("$AFP_BASE") + Path.basic("web")): Process_Result = { Isabelle_System.bash( exec.implode + " -s " + quote(layout.src_dir.implode) + " -d " + quote(out_dir.canonical.implode)) } def watch(layout: Layout, out_dir: Path = Path.explode("$AFP_BASE") + Path.basic("web"), progress: Progress = new Progress()): Process_Result = { Isabelle_System.bash( exec.implode + " server -s " + quote(layout.src_dir.implode) + " -d " + quote(out_dir.canonical.implode), progress_stdout = progress.echo, progress_stderr = progress.echo_warning) } } \ No newline at end of file diff --git a/tools/metadata.scala b/tools/metadata.scala --- a/tools/metadata.scala +++ b/tools/metadata.scala @@ -1,271 +1,275 @@ +/* Author: Fabian Huch, TU Muenchen + +AFP metadata model and TOML serialization. + */ package afp import isabelle._ import afp.TOML._ import java.time.LocalDate object Metadata { sealed abstract class Affiliation(val author: Author.ID) case class Unaffiliated(override val author: Author.ID) extends Affiliation(author) case class Email(override val author: Author.ID, id: Email.ID, address: String) extends Affiliation(author) object Email { type ID = String } case class Homepage(override val author: Author.ID, id: Homepage.ID, url: String) extends Affiliation(author) object Homepage { type ID = String } case class Author( id: Author.ID, name: String, emails: List[Email], homepages: List[Homepage] ) object Author { type ID = String } case class Topic(id: Topic.ID, name: String, sub_topics: List[Topic]) object Topic { type ID = String } type Date = LocalDate object Isabelle { type Version = String } case class Release(entry: Entry.Name, date: Date, isabelle: Isabelle.Version) case class License(id: License.ID, name: String) object License { type ID = String } type Change_History = Map[Date, String] type Extra = Map[String, String] case class Entry( name: Entry.Name, title: String, authors: List[Affiliation], date: Date, topics: List[Topic], `abstract`: String, notifies: List[Email], contributors: List[Affiliation], license: License, note: String, change_history: Change_History, extra: Extra, releases: List[Release]) object Entry { type Name = String } /* toml */ object TOML { private def by_id[A](elems: Map[String, A], id: String): A = elems.getOrElse(id, error("Elem " + quote(id) + " not found in " + commas_quote(elems.map(_.toString)))) /* author */ def from_authors(authors: List[Author]): T = { def from_author(author: Author): T = T( "name" -> author.name, "emails" -> T(author.emails.map(email => email.id -> email.address)), "homepages" -> T(author.homepages.map(homepage => homepage.id -> homepage.url))) T(authors.map(author => author.id -> from_author(author))) } def to_authors(authors: T): List[Author] = { def to_author(author_id: Author.ID, author: T): Author = { val emails = split_as[String](get_as[T](author, "emails")) map { case (id, address) => Email(author = author_id, id = id, address = address) } val homepages = split_as[String](get_as[T](author, "homepages")) map { case (id, url) => Homepage(author = author_id, id = id, url = url) } Author( id = author_id, name = get_as[String](author, "name"), emails = emails, homepages = homepages ) } split_as[T](authors).map { case (id, author) => to_author(id, author) } } /* topics */ def from_topics(root_topics: List[Topic]): T = T(root_topics.map(t => t.name -> from_topics(t.sub_topics))) def to_topics(root_topics: T): List[Topic] = { def to_topics_rec(topics: T, root: Topic.ID): List[Topic] = split_as[T](topics).map { case (name, sub_topics) => val id = (if (root.nonEmpty) root + "/" else "") + name Topic(id, name, to_topics_rec(sub_topics, id)) } to_topics_rec(root_topics, "") } /* releases */ def from_releases(releases: List[Release]): T = T(Utils.group_sorted(releases, (r: Release) => r.entry).view.mapValues { entry_releases => T(entry_releases.map(r => r.isabelle -> r.date)) }.toList) def to_releases(map: T): List[Release] = split_as[T](map).flatMap { case (entry, releases) => split_as[Date](releases).map { case (version, date) => Release(entry = entry, date = date, isabelle = version) } } /* affiliation */ def from_affiliations(affiliations: List[Affiliation]): T = T(Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues(vs => T(vs.collect { case Email(_, id, _) => "email" -> id case Homepage(_, id, _) => "homepage" -> id })).toList) def to_affiliations(affiliations: T, authors: Map[Author.ID, Author]): List[Affiliation] = { def to_affiliation(affiliation: (String, String), author: Author): Affiliation = { affiliation match { case ("email", id: String) => author.emails.find(_.id == id) getOrElse error("Email not found: " + quote(id)) case ("homepage", id: String) => author.homepages.find(_.id == id) getOrElse error("Homepage not found: " + quote(id)) case e => error("Unknown affiliation type: " + e) } } split_as[T](affiliations).flatMap { case (id, author_affiliations) => val author = by_id(authors, id) if (author_affiliations.isEmpty) List(Unaffiliated(author.id)) else split_as[String](author_affiliations).map(to_affiliation(_, author)) } } def from_emails(emails: List[Email]): T = T(emails.map(email => email.author -> email.id)) def to_emails(emails: T, authors: Map[Author.ID, Author]): List[Email] = emails.toList.map { case (author, id: String) => by_id(authors, author).emails.find(_.id == id) getOrElse error("Email not found: " + quote(id)) case e => error("Unknown email: " + quote(e.toString)) } /* license */ def from_licenses(licenses: List[License]): T = T(licenses.map(license => license.id -> T("name" -> license.name))) def to_licenses(licenses: T): List[License] = { split_as[T](licenses) map { case (id, license) => License(id, get_as[String](license, "name")) } } def to_license(license: String, licenses: Map[License.ID, License]): License = licenses.getOrElse(license, error("No such license: " + quote(license))) /* history */ def from_change_history(change_history: Change_History): T = change_history.map { case (date, str) => date.toString -> str } def to_change_history(change_history: T): Change_History = change_history.map { case (date, entry: String) => LocalDate.parse(date) -> entry case e => error("Unknown history entry: " + quote(e.toString)) } /* entry */ def from_entry(entry: Entry): T = T( "title" -> entry.title, "authors" -> from_affiliations(entry.authors), "contributors" -> from_affiliations(entry.contributors), "date" -> entry.date, "topics" -> entry.topics.map(_.id), "abstract" -> entry.`abstract`, "notify" -> from_emails(entry.notifies), "license" -> entry.license.id, "note" -> entry.note, "history" -> from_change_history(entry.change_history), "extra" -> entry.extra) def to_entry(entry: T, authors: Map[Author.ID, Author], topics: Map[Topic.ID, Topic], licenses: Map[License.ID, License], releases: List[Release]): Entry = Entry( name = get_as[String](entry, "name"), title = get_as[String](entry, "title"), authors = to_affiliations(get_as[T](entry, "authors"), authors), date = get_as[Date](entry, "date"), topics = get_as[List[String]](entry, "topics").map(by_id(topics, _)), `abstract` = get_as[String](entry, "abstract"), notifies = to_emails(get_as[T](entry, "notify"), authors), contributors = to_affiliations(get_as[T](entry, "contributors"), authors), license = to_license(get_as[String](entry, "license"), licenses), note = get_as[String](entry, "note"), change_history = to_change_history(get_as[T](entry, "history")), extra = get_as[Extra](entry, "extra"), releases = releases) } } diff --git a/tools/python.scala b/tools/python.scala --- a/tools/python.scala +++ b/tools/python.scala @@ -1,28 +1,32 @@ +/* Author: Fabian Huch, TU Muenchen + +Wrapper for Python interaction, to be used with the AFP Python component. + */ package afp import isabelle._ object Python { val python_home = Isabelle_System.getenv("ISABELLE_PYTHON") val python_path = (Path.explode("$AFP_BASE") + Path.make(List("admin", "sitegen-lib"))).absolute def run(script: String): Process_Result = { val exec = Path.explode(proper_string(python_home).getOrElse("No python component found")) + Path.make(List("bin", "python3")) val script_file = Isabelle_System.tmp_file("isabelle_python", "py") File.write(script_file, script) val res = Isabelle_System.bash(exec.implode + " " + script_file.getAbsolutePath, env = Isabelle_System.settings(List("PYTHONPATH" -> python_path.implode))) script_file.delete() res } } diff --git a/tools/toml.scala b/tools/toml.scala --- a/tools/toml.scala +++ b/tools/toml.scala @@ -1,406 +1,410 @@ +/* Author: Fabian Huch, TU Muenchen + +Support for TOML: https://toml.io/en/v1.0.0 + */ package afp import isabelle._ import scala.collection.immutable.ListMap import scala.reflect.{ClassTag, classTag} import scala.util.Try import scala.util.matching.Regex import scala.util.parsing.combinator.Parsers import scala.util.parsing.combinator.lexical.Scanners import scala.util.parsing.input.CharArrayReader.EofCh import java.time.{LocalDate, LocalDateTime, LocalTime, OffsetDateTime} object TOML { type Key = String type V = Any type T = Map[Key, V] object T { def apply(entries: (Key, V)*): T = ListMap(entries: _*) def apply(entries: List[(Key, V)]): T = ListMap(entries: _*) def unapply(t: Map[_, V]): Option[T] = { if (t.keys.forall(_.isInstanceOf[Key])) Some(t.asInstanceOf[T]) else None } } /* typed access */ def split_as[A: ClassTag](map: T): List[(Key, A)] = map.keys.toList.map(k => k -> get_as[A](map, k)) def get_as[A: ClassTag](map: T, name: String): A = map.get(name) match { case Some(value: A) => value case Some(value) => error("Value " + quote(value.toString) + " not of type " + classTag[A].runtimeClass.getName) case None => error("Field " + name + " not in " + map) } /* lexer */ object Kind extends Enumeration { val KEYWORD, IDENT, STRING, COMMENT, ERROR = Value } sealed case class Token(kind: Kind.Value, text: String) { def is_ident: Boolean = kind == Kind.IDENT def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name def is_string: Boolean = kind == Kind.STRING def is_error: Boolean = kind == Kind.ERROR } object Lexer extends Scanners with Scan.Parsers { override type Elem = Char type Token = TOML.Token def errorToken(msg: String): Token = Token(Kind.ERROR, msg) val white_space: String = " \t\n\r" override val whiteSpace: Regex = ("[" + white_space + "]+").r override def whitespace: Parser[Any] = many(character(white_space.contains(_))) override def comment: Parser[String] = '#' ~>! rep(elem("", c => c != EofCh && c != '\n')) ~ elem("", c => c == EofCh || c == '\n') ^^ { case s ~ t => s.mkString + t } def keyword: Parser[Token] = ("[[" | "]]" | one(character("{}[],=.".contains(_)))) ^^ (s => Token(Kind.KEYWORD, s)) def ident: Parser[Token] = many1(character(c => Symbol.is_ascii_digit(c) || Symbol.is_ascii_letter(c) || c == '_' || c == '-')) ^^ (s => Token(Kind.IDENT, s)) def basic_string: Parser[Token] = '\"' ~> rep(string_body) <~ '\"' ^^ (cs => Token(Kind.STRING, cs.mkString)) def multiline_basic_string: Parser[Token] = "\"\"\"" ~>! rep(multiline_string_body | ("\"" | "\"\"") ~ multiline_string_body) <~ "\"\"\"" ^^ (cs => Token(Kind.STRING, cs.mkString.stripPrefix("\n"))) def multiline_string_body: Parser[Char] = elem("", c => c == '\t' || c == '\n' || c == '\r' || (c > '\u001f' && c != '\"' && c != '\\' && c != EofCh)) | '\\' ~> string_escape def string_body: Parser[Char] = elem("", c => c > '\u001f' && c != '\"' && c != '\\' && c != EofCh) | '\\' ~> string_escape def string_escape: Parser[Char] = elem("", "\"\\/".contains(_)) | elem("", "bfnrt".contains(_)) ^^ { case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } | 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^ (s => Integer.parseInt(s, 16).toChar) def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string") def token: Parser[Token] = keyword | ident | (multiline_basic_string | basic_string | string_failure) | failure("Illegal character") } /* parser */ trait Parser extends Parsers { type Elem = Token def keys: Parser[List[Key]] = rep1sep(key, $$$(".")) def string: Parser[String] = elem("string", _.is_string) ^^ (_.text) def integer: Parser[Int] = token("integer", _.is_ident, _.toInt) def float: Parser[Double] = token("float", _.is_ident, _.toDouble) def boolean: Parser[Boolean] = token("boolean", _.is_ident, _.toBoolean) def offset_date_time: Parser[OffsetDateTime] = token("offset date-time", _.is_ident, OffsetDateTime.parse) def local_date_time: Parser[LocalDateTime] = token("local date-time", _.is_ident, LocalDateTime.parse) def local_date: Parser[LocalDate] = token("local date", _.is_ident, LocalDate.parse) def local_time: Parser[LocalTime] = token("local time", _.is_ident, LocalTime.parse) def array: Parser[V] = $$$("[") ~>! rep(toml_value <~ $$$(",")) <~ $$$("]") def table: Parser[T] = $$$("[") ~>! (keys <~ $$$("]")) ~! content ^^ { case base ~ T(map) => to_map(List(base -> map)) } def inline_table: Parser[V] = $$$("{") ~>! (content ^? to_map) <~ $$$("}") def array_of_tables: Parser[T] = $$$("[[") ~>! (keys <~ $$$("]]")) >> { ks => repsep(content ^^ to_map, $$$("[[") ~! (keys ^? { case ks1 if ks1 == ks => }) ~ $$$("]]")) ^^ { list => List(ks -> list) } ^? to_map } def toml: Parser[T] = (content ~ rep(table | array_of_tables)) ^? { case T(map) ~ maps => map :: maps } ^? { case Merge(map) => map } /* auxiliary parsers */ private def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name)) private def token[A](name: String, p: Token => Boolean, parser: String => A): Parser[A] = elem(name, p) ^^ (tok => Try { parser(tok.text) }) ^? { case util.Success(v) => v } private def key: Parser[Key] = elem("key", e => e.is_ident || e.is_string) ^^ (_.text) private def toml_value: Parser[V] = string | integer | float | offset_date_time | local_date_time | local_date | local_time | array | inline_table private def content: Parser[List[(List[Key], V)]] = rep((keys <~ $$$("=")) ~! toml_value ^^ { case ks ~ v => ks -> v }) /* extractors */ private object T { def unapply(table: List[(List[Key], V)]): Option[T] = { val by_first_key = table.foldLeft(ListMap.empty[Key, List[(List[Key], V)]]) { case (map, (k :: ks, v)) => map.updatedWith(k) { case Some(value) => Some(value :+ (ks, v)) case None => Some(List((ks, v))) } case _ => return None } val res = by_first_key.map { case (k, (Nil, v) :: Nil) => k -> v case (k, T(map)) => k -> map case _ => return None } Some(res) } } private def to_map: PartialFunction[List[(List[Key], V)], T] = { case T(map) => map } object Merge { private def merge(map1: T, map2: T): Option[T] = { val res2 = map2.map { case (k2, v2) => map1.get(k2) match { case Some(v1) => (v1, v2) match { case (TOML.T(t1), TOML.T(t2)) => k2 -> merge(t1, t2).getOrElse(return None) case x => return None } case None => k2 -> v2 } } Some(map1.filter { case (k, _) => !map2.contains(k) } ++ res2) } def unapply(maps: List[T]): Option[T] = Some(maps.fold(Map.empty)(merge(_, _).getOrElse(return None))) } /* parse */ def parse(input: CharSequence): T = { val scanner = new Lexer.Scanner(Scan.char_reader(input)) phrase(toml)(scanner) match { case Success(toml, _) => toml case NoSuccess(_, next) => error("Malformed TOML input at " + next.pos) } } } object Parser extends Parser /* standard format */ def parse(s: String): T = Parser.parse(s) /* format to a subset of TOML */ object Format { def apply(toml: T): String = { val result = new StringBuilder /* keys */ def key(k: Key): Unit = { val Bare_Key = """[A-Za-z0-9_-]+""".r k match { case Bare_Key() => result ++= k case _ => result += '"' result ++= k result += '"' } } def keys(ks: List[Key]): Unit = Library.separate(None, ks.reverse.map(Some(_))).foreach { case None => result += '.' case Some(k) => key(k) } /* string */ def basic_string(s: String): Unit = { result += '"' result ++= s.iterator.map { case '\b' => "\\b" case '\t' => "\\t" case '\n' => "\\n" case '\f' => "\\f" case '\r' => "\\r" case '"' => "\\\"" case '\\' => "\\\\" case c => if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c }.mkString result += '"' } def multiline_basic_string(s: String): Unit = { result ++= "\"\"\"\n" result ++= s.iterator.map { case '\b' => "\\b" case '\t' => "\t" case '\n' => "\n" case '\f' => "\\f" case '\r' => "\r" case '"' => "\\\"" case '\\' => "\\\\" case c => if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c }.mkString.replace("\"\"\"", "\"\"\\\"") result ++= "\"\"\"" } /* integer, boolean, offset date-time, local date-time, local date, local time */ object To_String { def unapply(v: V): Option[String] = v match { case _: Int | _: Double | _: Boolean | _: OffsetDateTime | _: LocalDateTime | _: LocalDate | _: LocalTime => Some(v.toString) case _ => None } } /* inline: string, float, To_String, value array */ def inline(v: V, indent: Int = 0): Unit = { def indentation(i: Int): Unit = for (_ <- Range(0, i)) result ++= " " indentation(indent) v match { case s: String => if (s.contains("\n") && s.length > 20) multiline_basic_string(s) else basic_string(s) case To_String(s) => result ++= s case list: List[V] => if (list.isEmpty) { result ++= "[]" } else { result ++= "[\n" list.foreach { elem => inline(elem, indent + 1) result ++= ",\n" } indentation(indent) result += ']' } case _ => error("Not inline TOML value: " + v.toString) } } /* array */ def inline_values(path: List[Key], v: V): Unit = { v match { case T(map) => map.foreach { case (k, v1) => inline_values(k :: path, v1) } case _ => keys(path) result ++= " = " inline(v) result += '\n' } } def is_inline(elem: V): Boolean = elem match { case To_String(_) | _: Double | _: String => true case list: List[V] => list.forall(is_inline) case _ => false } def array(path: List[Key], list: List[V]): Unit = { if (list.forall(is_inline)) inline_values(path.take(1), list) else { list.collect { case T(map) => result ++= "\n[[" keys(path) result ++= "]]\n" table(path, map, is_table_entry = true) case _ => error("Array can only contain either all tables or all non-tables") } } } /* table */ def table(path: List[Key], map: T, is_table_entry: Boolean = false): Unit = { val (values, nodes) = map.toList.partition(kv => is_inline(kv._2)) if (!is_table_entry && path.nonEmpty) { result ++= "\n[" keys(path) result ++= "]\n" } values.foreach { case (k, v) => inline_values(List(k), v) } nodes.foreach { case (k, T(map1)) => table(k :: path, map1) case (k, list: List[V]) => array(k :: path, list) case (_, v) => error("Invalid TOML: " + v.toString) } } table(Nil, toml) result.toString } } } diff --git a/tools/utils.scala b/tools/utils.scala --- a/tools/utils.scala +++ b/tools/utils.scala @@ -1,27 +1,31 @@ +/* Author: Fabian Huch, TU Muenchen + +Utilities. + */ package afp import isabelle._ import scala.collection.immutable.ListMap object Utils { def group_sorted[A, K](l: List[A], f: A => K): ListMap[K, List[A]] = l.foldRight(ListMap.empty[K, List[A]]) { case (a, m) => m.updatedWith(f(a)) { case Some(as) => Some(a :: as) case None => Some(List(a)) } } def grouped_sorted[A, K](l: List[A], f: A => K): ListMap[K, A] = group_sorted(l, f).map { case (k, v :: Nil) => k -> v case (k, vs) => error("Not distinct for " + quote(k.toString) + ": " + commas_quote(vs.map(_.toString))) } def the_entry[K, V](m: Map[K, V], k: K): V = m.getOrElse(k, error("Expected key " + quote(k.toString))) } \ No newline at end of file