diff --git a/metadata/README.md b/metadata/README.md --- a/metadata/README.md +++ b/metadata/README.md @@ -1,228 +1,233 @@ Metadata format =============== We're using the [TOML](https://toml.io/en/v1.0.0) format for metadata files. The data model is defined in Isabelle/Scala, so larger changes can also be done in a programmatic way. +You can also use the web-based user interface to edit the metadata, +which can be started locally with `isabelle afp_edit_metadata` +(though some fields can not be edited this way, such as the history) -- +on a save, the tool will overwrite the metadata in your repository clone. + `entries/.toml` --------------------- Storage for entry metadata. Format: ```toml title = "" date = --
topics = ["//...", "/..."] abstract = """ """ license = "" note = "" [authors] [contributors] [notify] [history] [extra] [related] ``` Optional: - ```toml statistics_ignore = ``` - in `[authors]` and `[contributors]`: ```toml [authors.] homepage = "" email = "" ``` - in `[notify]`: ```toml = "" ``` - in `[history]`: ```toml --
= "" ``` - in `[extra]`: ```toml extra- = ": " ``` - in `[related]`: ```toml dois = [ "", ... ] pubs = [ "", ... ] ``` [Example](/metadata/entries/Presburger-Automata.toml) Details: - **name**: The toml file name (`` in this terminology) must correspond to the folder name in `thys` directory. This short name is used as entry identifier during the whole process. - **date**: The date is the submission date of the entry. - **topics**: Currently, only three levels of topics and subtopics are allowed, but you may specify as many topics as you wish. If multiple topics are specified, the entry will appear under each of them. The topic must also appear in the `topics` file (see below). - **license**: Allowed values for the license are "bsd" and "lgpl". - **authors**: Authors and affiliations must appear in the `authors` file (see below). For each author, you may provide an affiliation as homepage and/or email. - **contributors**: Sometimes existing entries get significant contributions from other authors. These authors can be listed on a 'contributors' line. A separate change-history entry should indicate what these people have contributed. - **extra**: If you want to have some additional text fields below the 'Abstract' column, you can use the `extra` facility, where `` denotes an identifier (most cases 0, 1, ...) unique for each entry. The particular `` has no impact on output and is solely used for disambiguating multiple extra fields. Example: ```toml extra-0 = "Warning: Untested..." ``` - **related**: A Place for references related to this article, e.g., print publications. DOIs are preferred and stored by name only (e.g., `10.1000/182`). If there is none, use a formatted citation (html tags are allowed). `topics.toml` ------------- Each topic and its subtopics must go into there. Format: ```toml ["First level topic"] ["First level topic".classification] ["First level topic"."Second level topic"] ["First level topic"."Second level topic".classification] ["First level topic"."Second level topic"."Third level topic"] ["First level topic"."Second level topic"."Third level topic".classification] ["First level topic"."Another second level topic"] ["First level topic"."Another second level topic".classification] ``` Topics without space may omit quotes. Only three levels of indentation are supported currently. Optional: - in `[<...>.classification]`: - AMS: ```toml ams.id = "" ams.hierarchy = [ "", ] ``` - ACM: ```toml acm.id = "" acm.desc = "" ``` Details: - **classification**: A corresponding topic for each AMS and ACM subject classification can be put here. - AMS: Data comes from [MSC2020 database](https://mathscinet.ams.org/mathscinet/msc/msc2020.html). IDs are used without `-XX` or `xx`. In the hierarchy, descriptions are stored for each level (text in `{...}` is omitted), top level first. - ACM: Data comes from [2012 ACM CCS](https://dl.acm.org/ccs), and the fields can be directly copied from the xml output. `authors.toml` -------------- Name, alphanumeric short name, and affiliations for each author. Format: ```toml [] name = "" [.emails] [.homepages] ``` Optional: - in `[]`: ```toml orcid = "" ``` - in `[.emails]`: ```toml [.emails.] user = [ ] host = [ ] ``` - in `[.homepages]`: ```toml = "" ``` Example: ```toml [huch] name = "Fabian Huch" orcid = "0000-0002-9418-1580" [huch.emails] [huch.emails.huch_email] user = [ "huch", ] host = [ "in", "tum", "de", ] [huch.homepages] huch_homepage = "https://home.in.tum.de/~huch" ``` Details: - **shortname**: Author shortnames are derived from last name and characters from the first name until unique, e.g. `haslbeck` and `haslbeckm`. Homepage and email ids are usually of form `_email` ( or `_homepage`) and are incremented for multiples, e.g. `haslbeckm_email1`. - **orcid**: Orcid id, identifier only. - **parts**: User and host are represented as lists of parts split by dots. `releases.toml` --------------- Contains all releases. The youngest release is always ignored, so don't forget to add old releases when a new Isabelle version is released. Format: ```toml [name] --
= ``` diff --git a/tools/afp_release.scala b/tools/afp_release.scala --- a/tools/afp_release.scala +++ b/tools/afp_release.scala @@ -1,106 +1,103 @@ /* Author: Fabian Huch, TU Muenchen Tooling to manage AFP releases. */ package afp import isabelle.* import java.time.LocalDate object AFP_Release { def afp_import_releases( user: String, host: String, releases_dir: Path, - base_dir: Path, options: Options ): Unit = { val Release_Tar = """afp-(.+)-(\d{4}-\d{2}-\d{2})\.tar\.gz""".r - val afp = AFP_Structure(base_dir) + val afp = AFP_Structure() val isabelle_releases = split_lines(File.read(afp.metadata_dir + Path.basic("release-dates"))) val Isa_Release = """(.+) = (.+)""".r val release_dates = isabelle_releases.filterNot(_.isBlank).map { case Isa_Release(isabelle_version, date) => LocalDate.parse(date) -> isabelle_version case line => error("Could not parse: " + quote(line)) } using(SSH.open_session(options, host, user = user)) { ssh => val releases = ssh.read_dir(releases_dir).collect { case Release_Tar(entry, date_str) => val date = LocalDate.parse(date_str) release_dates.findLast { case (isa_date, _) => !isa_date.isAfter(date) } match { case Some(_, isabelle) => Metadata.Release(entry, date, isabelle) case None => error("No Isabelle version found for " + date_str) } } afp.save_releases(releases) } } - def afp_release(date: LocalDate, isabelle: Metadata.Isabelle.Version, base_dir: Path): Unit = { + def afp_release(date: LocalDate, isabelle: Metadata.Isabelle.Version): Unit = { def add_release(entry: Metadata.Entry): Metadata.Entry = entry.copy(releases = entry.releases :+ Metadata.Release(entry.name, date, isabelle)) - val afp = AFP_Structure(base_dir) + val afp = AFP_Structure() val releases = afp.load_entries().values.toList.map(add_release).flatMap(_.releases) afp.save_releases(releases) } val isabelle_tool = Isabelle_Tool("afp_release", "Create an AFP release", Scala_Project.here, { args => var isabelle = Isabelle_System.isabelle_identifier().getOrElse("") var date = LocalDate.now() var options = Options.init() var releases: String = "afpweb@isa-afp.org:/srv/afp/release" var import_releases = false val getopts = Getopts(""" Usage: isabelle afp_release [OPTIONS] Options are: -i ID Isabelle id (default: """ + quote(isabelle) + """) -d DATE release date (default: """ + quote(date.toString) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r REMOTE remote location of releases (default: """ + quote(releases) + """)" -I import releases from directory instead Register releases for old Isabelle version (when creating a new AFP release), or import all releases from release dir. """, "i:" -> (arg => isabelle = arg), "d:" -> (arg => date = LocalDate.parse(arg)), "o:" -> (arg => options = options + arg), "r:" -> (arg => releases = arg), "I" -> (_ => import_releases = true)) getopts(args) - val base_dir = Path.explode("$AFP_BASE") - if (import_releases) { val Remote = """([^@]+)@([^:]+):(.*)""".r releases match { case Remote(user, host, dir) => afp_import_releases(user = user, host = host, releases_dir = Path.explode(dir), - base_dir = base_dir, options = options) + options = options) case _ => error("Invalid remote: " + quote(releases)) } } else { if (isabelle.isEmpty) getopts.usage() - afp_release(date, isabelle, base_dir) + afp_release(date, isabelle) } }) } 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,485 +1,483 @@ /* Author: Fabian Huch, TU Muenchen Generation and compilation of SSG project for the AFP website. */ package afp import isabelle.* import afp.Metadata.{Affiliation, Author, ACM, AMS, Classification, DOI, Email, Entry, Formatted, Homepage, Reference, Release, Topic, Unaffiliated} object AFP_Site_Gen { /* cache */ class Cache(layout: Hugo.Layout, progress: Progress = new Progress()) { private val doi_cache = Path.basic("dois.json") private var dois: Map[String, String] = { val file = layout.cache_dir + doi_cache if (file.file.exists) { val content = File.read(file) val json = try { isabelle.JSON.parse(content) } catch { case ERROR(msg) => error("Could not parse " + file.toString + ": " + msg) } JSON.to_dois(json) } else { progress.echo_warning("No DOI cache found - resolving might take some time") Map.empty } } def resolve_doi(doi: DOI): String = { dois.get(doi.identifier) match { case Some(value) => value case None => val res = doi.formatted() dois += (doi.identifier -> res) layout.write_cache(doi_cache, JSON.from_dois(dois)) res } } } /* json */ object JSON { type T = isabelle.JSON.T object Object { type T = isabelle.JSON.Object.T def apply(entries: isabelle.JSON.Object.Entry*): T = isabelle.JSON.Object.apply(entries: _*) } def opt(k: String, v: String): Object.T = if (v.isEmpty) Object() else Object(k -> v) def opt(k: String, v: Option[T]): Object.T = v.map(v => Object(k -> v)).getOrElse(Object()) def opt[A <: Iterable[_]](k: String, vals: A): Object.T = if (vals.isEmpty) Object() else Object(k -> vals) def from_dois(dois: Map[String, String]): Object.T = dois def to_dois(dois: T): Map[String, String] = dois match { case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) && m.values.forall(_.isInstanceOf[String]) => m.asInstanceOf[Map[String, String]] case _ => error("Could not read dois") } def from_email(email: Email): Object.T = Object( "user" -> email.user.split('.').toList, "host" -> email.host.split('.').toList) def from_authors(authors: List[Author]): Object.T = authors.map(author => author.id -> (Object( "name" -> author.name, "emails" -> author.emails.map(from_email), "homepages" -> author.homepages.map(_.url.toString)) ++ opt("orcid", author.orcid.map(orcid => Object( "id" -> orcid.identifier, "url" -> orcid.url.toString))))).toMap def from_classification(classification: Classification): Object.T = Object( "desc" -> classification.desc, "url" -> classification.url.toString, "type" -> (classification match { case _: ACM => "ACM" case _: AMS => "AMS" })) def from_topics(topics: List[Topic]): Object.T = Object(topics.map(topic => topic.name -> ( opt("classification", topic.classification.map(from_classification)) ++ opt("topics", from_topics(topic.sub_topics)))): _*) def from_affiliations(affiliations: List[Affiliation]): Object.T = { Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues( { author_affiliations => val homepage = author_affiliations.collectFirst { case homepage: Homepage => homepage } val email = author_affiliations.collectFirst { case email: Email => email } Object() ++ opt("homepage", homepage.map(_.url.toString)) ++ opt("email", email.map(from_email)) }).toMap } def from_change_history(entry: (Metadata.Date, String)): Object.T = Object( "date" -> entry._1.toString, "value" -> entry._2) def from_release(release: Release): Object.T = Object( "date" -> release.date.toString, "isabelle" -> release.isabelle) def from_related(related: Reference, cache: Cache): T = related match { case d: DOI => val href = d.url.toString cache.resolve_doi(d).replace(href, "" + href + "") case Formatted(text) => text } def from_entry(entry: Entry, cache: Cache): Object.T = ( Object( "title" -> entry.title, "authors" -> entry.authors.map(_.author).distinct, "affiliations" -> from_affiliations(entry.authors ++ entry.contributors), "date" -> entry.date.toString, "topics" -> entry.topics.map(_.id), "abstract" -> entry.`abstract`, "license" -> entry.license.name) ++ opt("contributors", entry.contributors.map(_.author).distinct) ++ opt("releases", entry.releases.sortBy(_.isabelle).reverse.map(from_release)) ++ opt("note", entry.note) ++ opt("history", entry.change_history.toList.sortBy(_._1).reverse.map(from_change_history)) ++ opt("extra", entry.extra) ++ opt("related", entry.related.map(from_related(_, cache)))) def from_keywords(keywords: List[String]): T = keywords.sorted.map(keyword => Object("keyword" -> keyword)) } /* stats */ def afp_stats(deps: Sessions.Deps, structure: AFP_Structure, entries: List[Entry]): JSON.T = { def round(int: Int): Int = Math.round(int.toFloat / 100) * 100 def nodes(entry: Entry): List[Document.Node.Name] = structure.entry_sessions(entry.name).flatMap(session => deps(session.name).proper_session_theories) val theorem_commands = List("theorem", "lemma", "corollary", "proposition", "schematic_goal") var entry_lines = Map.empty[Entry, Int] var entry_lemmas = Map.empty[Entry, Int] for { entry <- entries node <- nodes(entry) lines = split_lines(File.read(node.path)).map(_.trim) } { entry_lines += entry -> (entry_lines.getOrElse(entry, 0) + lines.count(_.nonEmpty)) entry_lemmas += entry -> (entry_lemmas.getOrElse(entry, 0) + lines.count(line => theorem_commands.exists(line.startsWith))) } val first_year = entries.flatMap(_.releases).map(_.date.getYear).min def years(upto: Int): List[Int] = Range.inclusive(first_year, upto).toList val current_year = Date.now().rep.getYear val all_years = years(current_year) // per Isabelle release year val by_year = entries.groupBy(_.date.getYear) val size_by_year = by_year.view.mapValues(_.length).toMap val loc_by_year = by_year.view.mapValues(_.map(entry_lines).sum).toMap val authors_by_year = by_year.view.mapValues(_.flatMap(_.authors).map(_.author)).toMap val num_lemmas = entries.map(entry_lemmas).sum val num_lines = entries.map(entry_lines).sum // accumulated def total_articles(year: Int): Int = years(year).map(size_by_year.getOrElse(_, 0)).sum def total_loc(year: Int): Int = round(years(year).map(loc_by_year.getOrElse(_, 0)).sum) def total_authors(year: Int): Int = years(year).flatMap(authors_by_year.getOrElse(_, Nil)).distinct.length def fresh_authors(year: Int): Int = total_authors(year) - total_authors(year - 1) val sorted = entries.sortBy(_.date) def map_repetitions(elems: List[String], to: String): List[String] = elems.foldLeft(("", List.empty[String])) { case((last, acc), s) => (s, acc :+ (if (last == s) to else s)) }._2 JSON.Object( "years" -> all_years, "num_lemmas" -> num_lemmas, "num_loc" -> num_lines, "articles_year" -> all_years.map(total_articles), "loc_years" -> all_years.map(total_loc), "author_years" -> all_years.map(fresh_authors), "author_years_cumulative" -> all_years.map(total_authors), "loc_articles" -> sorted.map(entry_lines), "all_articles" -> sorted.map(_.name), "article_years_unique" -> map_repetitions(sorted.map(_.date.getYear.toString), "")) } /* site generation */ def afp_site_gen( layout: Hugo.Layout, status_file: Option[Path], afp: AFP_Structure, clean: Boolean = false, progress: Progress = new Progress() ): Unit = { /* clean old */ if (clean) { progress.echo("Cleaning up generated files...") layout.clean() } /* add topics */ progress.echo("Preparing topics...") val topics = afp.load_topics val root_topics = Metadata.Topics.root_topics(topics) layout.write_data(Path.basic("topics.json"), JSON.from_topics(root_topics)) /* add licenses */ progress.echo("Preparing licenses...") val licenses = afp.load_licenses /* add releases */ progress.echo("Preparing releases...") val releases = afp.load_releases /* prepare authors and entries */ progress.echo("Preparing authors...") val authors = afp.load_authors var seen_affiliations: List[Affiliation] = Nil val entries = afp.entries.flatMap { name => val entry = afp.load_entry(name, authors, topics, licenses, releases) seen_affiliations = seen_affiliations :++ entry.authors ++ entry.contributors Some(entry) } val seen_authors = Utils.group_sorted(seen_affiliations.distinct, (a: Affiliation) => a.author).map { case (id, affiliations) => val seen_emails = affiliations.collect { case e: Email => e } val seen_homepages = affiliations.collect { case h: Homepage => h } authors(id).copy(emails = seen_emails, homepages = seen_homepages) } layout.write_data(Path.basic("authors.json"), JSON.from_authors(seen_authors.toList)) /* extract keywords */ progress.echo("Extracting keywords...") var seen_keywords = Set.empty[String] val entry_keywords = entries.filterNot(_.statistics_ignore).map { entry => val scored_keywords = Rake.extract_keywords(entry.`abstract`) seen_keywords ++= scored_keywords.map(_._1) entry.name -> scored_keywords.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.getOrElse(name, Nil).filter(seen_keywords.contains).take(8) /* add entries and theory listings */ progress.echo("Preparing entries...") val sessions_structure = afp.sessions_structure val sessions_deps = Sessions.deps(sessions_structure) val browser_info = Browser_Info.context(sessions_structure) def theories_of(session_name: String): List[String] = sessions_deps(session_name).proper_session_theories.map(_.theory_base_name) def write_session_json(session_name: String, base: JSON.Object.T): Unit = { val session_json = base ++ JSON.Object( "title" -> session_name, "url" -> ("/sessions/" + session_name.toLowerCase), "theories" -> theories_of(session_name).map(thy_name => JSON.Object( "name" -> thy_name, "path" -> (browser_info.session_dir(session_name) + Path.basic(thy_name).html).implode ))) layout.write_content(Path.make(List("sessions", session_name + ".md")), session_json) } val cache = new Cache(layout, progress) val entry_sessions = entries.map(entry => entry -> afp.entry_sessions(entry.name)).toMap val session_entry = entry_sessions.flatMap((entry, sessions) => sessions.map(session => session.name -> entry)).toMap entries.foreach { entry => val deps = for { session <- entry_sessions(entry) dep_session <- sessions_structure.imports_graph.imm_preds(session.name) if sessions_structure(dep_session).is_afp dep <- session_entry.get(dep_session) if dep != entry } yield dep.name val sessions = afp.entry_sessions(entry.name).map { session => write_session_json(session.name, JSON.Object("entry" -> entry.name)) JSON.Object( "session" -> session.name, "theories" -> theories_of(session.name)) } val entry_json = JSON.from_entry(entry, cache) ++ JSON.Object( "dependencies" -> deps.distinct, "sessions" -> sessions, "url" -> ("/entries/" + entry.name + ".html"), "keywords" -> get_keywords(entry.name)) layout.write_content(Path.make(List("entries", entry.name + ".md")), entry_json) } for { (session_name, (info, _)) <- sessions_structure.imports_graph.iterator if !info.is_afp } write_session_json(session_name, JSON.Object("rss" -> false)) /* add statistics */ progress.echo("Preparing statistics...") val statistics_json = afp_stats(sessions_deps, afp, entries.filterNot(_.statistics_ignore)) layout.write_data(Path.basic("statistics.json"), statistics_json) /* 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 => } progress.echo("Finished sitegen preparation.") } /* build site */ def afp_build_site( out_dir: Path, layout: Hugo.Layout, do_watch: Boolean = false, clean: Boolean = false, progress: Progress = new Progress() ): Unit = { if (clean) { progress.echo("Cleaning output dir...") Hugo.clean(out_dir) } if (do_watch) { Hugo.watch(layout, out_dir, progress) } else { progress.echo("Building site...") Hugo.build(layout, out_dir) progress.echo("Build in " + (out_dir + Path.basic("index.html")).absolute.implode) } } /* tool wrapper */ val isabelle_tool = Isabelle_Tool("afp_site_gen", "generates afp website source", Scala_Project.here, { args => var base_dir = Path.explode("$AFP_BASE") var status_file: Option[Path] = None - var hugo_dir = base_dir + Path.make(List("web", "hugo")) - var out_dir: Path = base_dir + Path.make(List("web", "out")) + var hugo_dir = base_dir + Path.explode("out/hugo") + var out_dir: Path = base_dir + Path.explode("web") var build_only = false var devel_mode = false var fresh = false val getopts = Getopts(""" Usage: isabelle afp_site_gen [OPTIONS] Options are: - -B DIR afp base dir (default """" + base_dir.implode + """") -D FILE build status file for devel version -H DIR generated hugo project dir (default """" + hugo_dir.implode + """") -O DIR output dir for build (default """ + out_dir.implode + """) -b build only -d devel mode (overrides hugo dir, builds site in watch mode) -f fresh build: clean up existing hugo and build directories 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)), "D:" -> (arg => status_file = Some(Path.explode(arg))), "H:" -> (arg => hugo_dir = Path.explode(arg)), "O:" -> (arg => out_dir = Path.explode(arg)), "b" -> (_ => build_only = true), "d" -> (_ => devel_mode = true), "f" -> (_ => fresh = true)) getopts(args) status_file.foreach(path => if (!path.is_file || !path.file.exists()) error("Invalid status file: " + path)) if (devel_mode) hugo_dir = base_dir + Path.make(List("admin", "site")) - val afp = AFP_Structure(base_dir) + val afp = AFP_Structure() val layout = Hugo.Layout(hugo_dir) val progress = new Console_Progress() if (!build_only) { progress.echo("Preparing site generation in " + hugo_dir.implode) afp_site_gen(layout = layout, status_file = status_file, afp = afp, clean = fresh, progress = progress) } afp_build_site(out_dir = out_dir, layout = layout, do_watch = devel_mode, clean = fresh, 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,135 +1,135 @@ /* 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, options: Options) { +class AFP_Structure private(options: Options, val base_dir: Path) { /* files */ val metadata_dir = base_dir + Path.basic("metadata") val thys_dir = AFP.main_dir(base_dir) 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: isabelle.TOML.Table => 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: Metadata.Authors = Metadata.Authors(load(authors_file, Metadata.TOML.to_authors)) def load_releases: Metadata.Releases = Metadata.Releases(load(releases_file, Metadata.TOML.to_releases)) def load_licenses: Metadata.Licenses = Metadata.Licenses(load(licenses_file, Metadata.TOML.to_licenses)) def load_topics: Metadata.Topics = Metadata.Topics(load(topics_file, Metadata.TOML.to_topics)) def load_entry( name: Metadata.Entry.Name, authors: Metadata.Authors, topics: Metadata.Topics, licenses: Metadata.Licenses, releases: Metadata.Releases ): 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_entries( authors: Metadata.Authors = load_authors, topics: Metadata.Topics = load_topics, licenses: Metadata.Licenses = load_licenses, releases: Metadata.Releases = load_releases ): Metadata.Entries = Metadata.Entries(entries.map(name => load_entry(name, authors, topics, licenses, releases))) /* save */ private def save(file: Path, content: isabelle.TOML.Table): 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(root_topics: List[Metadata.Topic]): Unit = save(topics_file, Metadata.TOML.from_topics(root_topics)) def save_licenses(licenses: List[Metadata.License]): Unit = save(licenses_file, Metadata.TOML.from_licenses(licenses)) 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 + Sessions.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, select_dirs = List(thys_dir)) def entry_sessions(name: Metadata.Entry.Name): List[Sessions.Session_Entry] = Sessions.parse_root_entries(thys_dir + Path.basic(name) + Sessions.ROOT) def hg_id: String = Mercurial.repository(base_dir).id() } object AFP_Structure { - def apply(base_dir: Path = AFP.BASE, options: Options = Options.init0()): AFP_Structure = - new AFP_Structure(base_dir.absolute, options) + def apply(options: Options = Options.init0(), base_dir: Path = AFP.BASE): AFP_Structure = + new AFP_Structure(options, base_dir.absolute) } diff --git a/tools/afp_submit.scala b/tools/afp_submit.scala --- a/tools/afp_submit.scala +++ b/tools/afp_submit.scala @@ -1,1719 +1,1748 @@ /* Author: Fabian Huch, TU Muenchen AFP submission system backend. */ package afp import isabelle.* import isabelle.HTML.* import isabelle.Web_App.Params import isabelle.Web_App.More_HTML.* import afp.Metadata.{Affiliation, Author, Authors, DOI, Email, Entry, Entries, Formatted, Homepage, License, Licenses, Orcid, Reference, Release, Releases, Topic, Topics, Unaffiliated} import java.text.Normalizer import java.time.LocalDate object AFP_Submit { /* (optional) values with errors */ object Val_Opt { def ok[A](value: A): Val_Opt[A] = Val_Opt(Some(value), None) def user_err[A](msg: String): Val_Opt[A] = Val_Opt(None, Some(msg)) def error[A]: Val_Opt[A] = Val_Opt(None, None) } case class Val_Opt[A] private(opt: Option[A], err: Option[String]) { def is_empty: Boolean = opt.isEmpty } object Val { def ok[A](value: A): Val[A] = Val(value, None) def err[A](value: A, msg: String): Val[A] = Val(value, Some(msg)) } case class Val[A] private(v: A, err: Option[String]) { def with_err(err: String): Val[A] = Val.err(v, err) def perhaps_err(opt: Val_Opt[_]): Val[A] = opt.err.map(with_err).getOrElse(this) } /* data model and operations */ object Model { sealed trait T object Related extends Enumeration { val DOI, Plaintext = Value def from_string(s: String): Option[Value] = values.find(_.toString == s) def get(r: Reference): Value = r match { case afp.Metadata.DOI(_) => DOI case afp.Metadata.Formatted(_) => Plaintext } } object Create_Entry { def apply(state: State): Create_Entry = Create_Entry(license = state.licenses.values.head) } case class Create_Entry( name: Val[String] = Val.ok(""), title: Val[String] = Val.ok(""), affils: Val[List[Affiliation]] = Val.ok(Nil), notifies: Val[List[Email]] = Val.ok(Nil), author_input: Option[Author] = None, notify_input: Option[Author] = None, topics: Val[List[Topic]] = Val.ok(Nil), topic_input: Option[Topic] = None, license: License, `abstract`: Val[String] = Val.ok(""), related: List[Reference] = Nil, related_kind: Option[Related.Value] = None, related_input: Val[String] = Val.ok("") ) { def used_affils: Set[Affiliation] = (affils.v ++ notifies.v).toSet def used_authors: Set[Author.ID] = used_affils.map(_.author) def add_affil: Create_Entry = author_input match { case None => copy(affils = affils.with_err("Select author first")) case Some(author) => val default_affil = author.emails.headOption.orElse( author.homepages.headOption).getOrElse(Unaffiliated(author.id)) copy(author_input = None, affils = Val.ok(affils.v :+ default_affil)) } def remove_affil(affil: Affiliation): Create_Entry = copy(affils = Val.ok(affils.v.filterNot(_ == affil))) def add_notify: Option[Create_Entry] = notify_input match { case None => Some(copy(notifies = notifies.with_err("Select author first"))) case Some(author) => for (email <- author.emails.headOption) yield copy(notify_input = None, notifies = Val.ok(notifies.v :+ email)) } def remove_notify(notify: Email): Create_Entry = copy(notifies = Val.ok(notifies.v.filterNot(_ == notify))) def add_topic(state: State): Create_Entry = topic_input match { case None => copy(topics = topics.with_err("Select topic first")) case Some(topic) => val topic1 = Model.validate_topic(topic.id, topics.v, state) val topic_input1 = if (topic1.is_empty) topic_input else None copy(topic_input = topic_input1, topics = Val.ok(topics.v ++ topic1.opt).perhaps_err(topic1)) } def remove_topic(topic: Topic): Create_Entry = copy(topics = Val.ok(topics.v.filterNot(_ == topic))) def add_related: Create_Entry = related_kind match { case None => copy(related_input = related_input.with_err("Select reference kind first")) case Some(kind) => val reference = validate_related(kind, related_input.v, entry.related) copy(related = related ++ reference.opt, related_input = Val.ok(if (reference.is_empty) related_input.v else "").perhaps_err(reference)) } def remove_related(reference: Reference): Create_Entry = copy(related = related.filterNot(_ == reference)) def entry: Entry = Entry(name = name.v, title = title.v, authors = affils.v, date = LocalDate.now(), topics = topics.v, `abstract` = `abstract`.v.trim, notifies = notifies.v, license = license, note = "", related = related) } object Create { def init(state: State): Create = Create(entries = Val.ok(List(Create_Entry(state)))) } case class Create( entries: Val[List[Create_Entry]] = Val.ok(Nil), new_authors: Val[List[Author]] = Val.ok(Nil), new_author_input: String = "", new_author_orcid: String = "", new_affils: Val[List[Affiliation]] = Val.ok(Nil), new_affils_author: Option[Author] = None, new_affils_input: String = "", ) extends T { def add_entry(state: State): Create = copy(entries = Val.ok(entries.v :+ Create_Entry(state))) def update_entry(num: Int, entry: Create_Entry): Create = copy(entries = Val.ok(entries.v.updated(num, entry))) def remove_entry(num: Int): Create = copy(entries = Val.ok(Utils.remove_at(num, entries.v))) def updated_authors(state: State): Authors = (state.authors ++ new_authors.v.map(author => author.id -> author)).map { case (id, author) => val emails = author.emails ++ new_affils.v.collect { case e: Email if e.author == id => e } val homepages = author.homepages ++ new_affils.v.collect { case h: Homepage if h.author == id => h } id -> author.copy(emails = emails.distinct, homepages = homepages.distinct) } def add_new_author(state: State): Create = { val name = new_author_input.trim if (name.isEmpty) copy(new_authors = new_authors.with_err("Name must not be empty")) else { def as_ascii(str: String) = { var res: String = str List("ö" -> "oe", "ü" -> "ue", "ä" -> "ae", "ß" -> "ss").foreach { case (c, rep) => res = res.replace(c, rep) } Normalizer.normalize(res, Normalizer.Form.NFD).replaceAll("[^\\x00-\\x7F]", "") } def make_author_id(name: String): String = { val normalized = as_ascii(name) val Suffix = """^.*?([a-zA-Z]*)$""".r val suffix = normalized match { case Suffix(suffix) => suffix case _ => "" } val Prefix = """^([a-zA-Z]*).*$""".r val prefix = normalized.stripSuffix(suffix) match { case Prefix(prefix) => prefix case _ => "" } val authors = updated_authors(state) var ident = suffix.toLowerCase for { c <- prefix.toLowerCase if authors.contains(ident) } ident += c.toString Utils.make_unique(ident, authors.keySet) } val id = make_author_id(name) val author = validate_new_author(id, new_author_input, new_author_orcid, updated_authors(state)) copy( new_author_input = if (author.is_empty) new_author_input else "", new_author_orcid = if (author.is_empty) new_author_orcid else "", new_authors = Val.ok(new_authors.v ++ author.opt).perhaps_err(author)) } } def remove_new_author(author: Author): Option[Create] = if (used_authors.contains(author.id)) None else Some(copy(new_authors = Val.ok(new_authors.v.filterNot(_.id == author.id)))) def add_new_affil: Create = new_affils_author match { case Some(author) => val address = new_affils_input.trim if (address.isEmpty) copy(new_affils = new_affils.with_err("Must not be empty")) else { val id = if (address.contains("@")) Utils.make_unique(author.id + "_email", author.emails.map(_.id).toSet) else Utils.make_unique(author.id + "_homepage", author.homepages.map(_.id).toSet) val affil = validate_new_affil(id, address, author) copy( new_affils_input = if (affil.is_empty) new_affils_input else "", new_affils = Val.ok(new_affils.v ++ affil.opt).perhaps_err(affil)) } case None => copy(new_affils = new_affils.with_err("Select author first")) } def remove_new_affil(affil: Affiliation): Option[Create] = if (used_affils.contains(affil)) None else Some(copy(new_affils = Val.ok(new_affils.v.filterNot(_ == affil)))) def validate( state: State, message: String, existing: Boolean ): T = { var ok = true def validate[A](validator: A => Val[A], value: A): Val[A] = { val res = validator(value) if (res.err.nonEmpty) ok = false res } def val_title(title: String): Val[String] = if (title.isBlank) Val.err(title, "Title must not be blank") else if (title.trim != title) Val.err(title, "Title must not contain extra spaces") else Val.ok(title) def val_name(name: String): Val[String] = if (name.isBlank) Val.err(name, "Name must not be blank") else if (!"[a-zA-Z0-9_-]+".r.matches(name)) Val.err(name, "Invalid character in name") else if (existing && !state.entries.contains(name)) Val.err(name, "Entry does not exist") else if (!existing && state.entries.contains(name)) Val.err(name, "Entry already exists") else Val.ok(name) def val_entries(entries: List[Model.Create_Entry]): Val[List[Model.Create_Entry]] = if (entries.isEmpty) Val.err(entries, "Must contain at least one entry") else if (Library.duplicates(entries.map(_.name)).nonEmpty) Val.err(entries, "Entries must have different names") else Val.ok(entries) def val_new_authors(authors: List[Author]): Val[List[Author]] = if (!authors.forall(author => used_authors.contains(author.id))) Val.err(authors, "Unused authors") else Val.ok(authors) def val_new_affils(affils: List[Affiliation]): Val[List[Affiliation]] = if (!affils.forall(affil => used_affils.contains(affil))) Val.err(affils, "Unused affils") else Val.ok(affils) def val_entry_authors(authors: List[Affiliation]): Val[List[Affiliation]] = if (authors.isEmpty) Val.err(authors, "Must contain at least one author") else if (!Utils.is_distinct(authors)) Val.err(authors, "Duplicate affiliations") else Val.ok(authors) def val_notifies(notifies: List[Email]): Val[List[Email]] = if (notifies.isEmpty) Val.err(notifies, "Must contain at least one maintainer") else if (!Utils.is_distinct(notifies)) Val.err(notifies, "Duplicate emails") else Val.ok(notifies) def val_topics(topics: List[Topic]): Val[List[Topic]] = if (topics.isEmpty) Val.err(topics, "Must contain at least one topic") else Val.ok(topics) def val_abstract(txt: String): Val[String] = if (txt.isBlank) Val.err(txt, "Entry must contain an abstract") else if (List("\\cite", "\\emph", "\\texttt").exists(txt.contains(_))) Val.err(txt, "LaTeX not allowed, use MathJax for math symbols") else Val.ok(txt) val entries1 = for (entry <- entries.v) yield entry.copy( name = validate(val_name, entry.name.v), title = validate(val_title, entry.title.v), affils = validate(val_entry_authors, entry.affils.v), notifies = validate(val_notifies, entry.notifies.v), topics = validate(val_topics, entry.topics.v), `abstract` = validate(val_abstract, entry.`abstract`.v)) val validated = copy( entries = validate(val_entries, entries1), new_authors = validate(val_new_authors, new_authors.v), new_affils = validate(val_new_affils, new_affils.v)) if (ok) Upload(Metadata(updated_authors(state), entries.v.map(_.entry)), message) else validated } def used_affils: Set[Affiliation] = entries.v.toSet.flatMap(_.used_affils) def used_authors: Set[Author.ID] = new_affils.v.map(_.author).toSet ++ entries.v.flatMap(_.used_authors) } object Build extends Enumeration { val Pending, Running, Aborted, Failed, Success = Value } object Status extends Enumeration { val Submitted, Review, Added, Rejected = Value def from_string(s: String): Option[Value] = values.find(_.toString == s) } case class Overview(id: String, date: LocalDate, name: String, status: Status.Value) { def update_repo(repo: Mercurial.Repository): Boolean = if (status != Model.Status.Added) false else { val id_before = repo.id() repo.pull() repo.update() val id_after = repo.id() id_before != id_after } } case class Metadata(authors: Authors, entries: List[Entry]) { def new_authors(state: State): List[Author] = entries.flatMap(_.authors).map(_.author).filterNot(state.authors.contains).toSet.map(authors).toList def new_affils(state: State): List[Affiliation] = entries.flatMap(entry => entry.authors ++ entry.notifies).toSet.filter { case _: Unaffiliated => false case e: Email => !state.authors.get(e.author).exists(_.emails.contains(e)) case h: Homepage => !state.authors.get(h.author).exists(_.homepages.contains(h)) }.toList } case object Invalid extends T object Upload { def apply(submission: Submission): Upload = Upload(submission.meta, submission.message) } case class Upload(metadata: Metadata, message: String, error: String = "") extends T { def save(handler: Handler, state: State): (Submission, State) = { val (id, state1) = handler.save(state, metadata, message) (handler.get(id, state1).get, state1) } def submit(handler: Handler, archive: Bytes, file_name: String, state: State): (T, State) = { if (archive.is_empty || file_name.isEmpty) (copy(error = "Select a file"), state) else if (!file_name.endsWith(".zip") && !file_name.endsWith(".tar.gz")) (copy(error = "Only .zip and .tar.gz archives allowed"), state) else { val file_extension = if (file_name.endsWith(".zip")) ".zip" else ".tar.gz" val (id, state1) = handler.save(state, metadata, message, archive, file_extension) (Created(id), state1) } } } case class Created(id: String) extends T case class Submission( id: Handler.ID, meta: Metadata, build: Build.Value, status: Option[Status.Value], message: String = "", log: Option[String] = None, archive: Option[String] = None ) extends T { def submit(handler: Handler): Option[Submission] = if (status.nonEmpty) None else { handler.submit(id) Some(copy(status = Some(Status.Submitted))) } def abort_build(handler: Handler): Option[Submission] = if (build != Model.Build.Running) None else { handler.abort_build(id) Some(copy(build = Model.Build.Aborted)) } } case class Submission_List(submissions: List[Overview]) extends T /* validation */ def validate_topic(id: String, selected: List[Topic], state: State): Val_Opt[Topic] = state.topics.values.find(_.id == id) match { case Some(topic) => if (selected.contains(topic)) Val_Opt.user_err("Topic already selected") else Val_Opt.ok(topic) case _ => Val_Opt.error } def validate_new_author( id: String, name: String, orcid_str: String, authors: Authors ): Val_Opt[Author] = { val Id = """[a-zA-Z][a-zA-Z0-9]*""".r id match { case Id() if !authors.contains(id) => if (name.isEmpty || name.trim != name) Val_Opt.user_err("Name must not be empty") else if (orcid_str.isEmpty) Val_Opt.ok(Author(id, name)) else Exn.capture(Orcid(orcid_str)) match { case Exn.Res(orcid) => if (authors.values.exists(_.orcid.exists(_ == orcid))) Val_Opt.user_err("Author with that orcid already exists") else Val_Opt.ok(Author(id, name, orcid = Some(orcid))) case _ => Val_Opt.user_err("Invalid orcid") } case _ => Val_Opt.error } } def validate_new_affil(id: String, address: String, author: Author): Val_Opt[Affiliation] = { if (address.isBlank) Val_Opt.user_err("Address must not be empty") else if (address.contains("@")) { val Id = (author.id + """_email\d*""").r id match { case Id() if !author.emails.map(_.id).contains(id) => val Address = """([^@\s]+)@([^@\s]+)""".r address match { case Address(user, host) => Val_Opt.ok(Email(author.id, id, user, host)) case _ => Val_Opt.user_err("Invalid email address") } case _ => Val_Opt.error } } else { val Id = (author.id + """_homepage\d*""").r id match { case Id() if !author.homepages.map(_.id).contains(id) => if (Url.is_wellformed(address)) Val_Opt.ok(Homepage(author.id, id, Url(address))) else Val_Opt.user_err("Invalid url") case _ => Val_Opt.error } } } def validate_related( kind: Model.Related.Value, related: String, references: List[Reference] ): Val_Opt[Reference] = if (related.isBlank) Val_Opt.user_err("Reference must not be empty") else { kind match { case Model.Related.DOI => Exn.capture(DOI(related)) match { case Exn.Res(doi) => if (references.contains(doi)) Val_Opt.user_err("Already present") else Val_Opt.ok(doi) case _ => Val_Opt.user_err("Invalid DOI format") } case Model.Related.Plaintext => val formatted = Formatted(related) if (references.contains(formatted)) Val_Opt.user_err("Already present") else Val_Opt.ok(formatted) } } } /* Physical submission handling */ trait Handler { def save( state: State, metadata: Model.Metadata, message: String = "", archive: Bytes = Bytes.empty, file_extension: String = "" ): (Handler.ID, State) def list(state: State): Model.Submission_List def get(id: Handler.ID, state: State): Option[Model.Submission] def submit(id: Handler.ID): Unit def set_status(id: Handler.ID, status: Model.Status.Value): Unit def abort_build(id: Handler.ID): Unit def get_patch(id: Handler.ID): Option[Path] def get_archive(id: Handler.ID): Option[Path] } object Handler { type ID = String object ID { private val format = Date.Format.make( List( Date.Formatter.pattern("uuuu-MM-dd_HH-mm-ss_SSS"), Date.Formatter.pattern("uuuu-MM-dd_HH-mm-ss_SSS_VV")), _ + "_" + Date.timezone().getId) def apply(submission_time: Date): ID = format(submission_time) def unapply(id: ID): Option[Date] = format.unapply(id) def check(id: ID): Option[ID] = unapply(id).map(apply) } /* Handler for local edits */ class Edit(afp: AFP_Structure) extends Handler { def save( state: State, metadata: Model.Metadata, message: String, archive: Bytes, ext: String ): (ID, State) = { val entry = metadata.entries match { case e :: Nil => e case _ => isabelle.error("Must be a single entry") } val old = state.entries(entry.name) val updated = old.copy(title = entry.title, authors = entry.authors, topics = entry.topics, `abstract` = entry.`abstract`, notifies = entry.notifies, license = entry.license, related = entry.related) afp.save_entry(updated) afp.save_authors(metadata.authors.values.toList) (entry.name, State.load(afp)) } def list(state: State): Model.Submission_List = Model.Submission_List(state.entries.values.toList.sortBy(_.date).reverse.map { entry => Model.Overview(entry.name, entry.date, entry.name, Model.Status.Added) }) def get(id: ID, state: State): Option[Model.Submission] = state.entries.get(id).map { entry => val meta = Model.Metadata(state.authors, List(entry)) Model.Submission(id, meta, Model.Build.Success, Some(Model.Status.Added)) } def submit(id: ID): Unit = () def set_status(id: ID, status: Model.Status.Value): Unit = () def abort_build(id: ID): Unit = () def get_patch(id: ID): Option[Path] = None def get_archive(id: ID): Option[Path] = None } /* Adapter to existing submission system */ class Adapter(submission_dir: Path, afp: AFP_Structure) extends Handler { private val up: Path = submission_dir + Path.basic("up") private def up(id: ID): Path = up + Path.basic(id) private def down(id: ID): Path = submission_dir + Path.basic("down") + Path.basic(id) private def signal(id: ID, s: String): Unit = File.write(up(id) + Path.basic(s), s.toUpperCase) private def is_signal(id: ID, s: String): Boolean = (up(id) + Path.basic(s)).file.exists() private def read_build(id: ID): Model.Build.Value = { val build = down(id) + Path.basic("result") if (!build.file.exists) Model.Build.Pending else File.read(build).trim match { case "" => Model.Build.Running case "NOT_FINISHED" => Model.Build.Running case "FAILED" => if (is_signal(id, "kill")) Model.Build.Aborted else Model.Build.Failed case "SUCCESS" => Model.Build.Success case s => isabelle.error("Unkown build status: " + quote(s)) } } private def status_file(id: ID): Path = up(id) + Path.basic("AFP_STATUS") private def read_status(id: ID): Option[Model.Status.Value] = { val status = status_file(id) if (!status.file.exists()) None else File.read(status).trim match { case "SUBMITTED" => Some(Model.Status.Submitted) case "PROCESSING" => Some(Model.Status.Review) case "REJECTED" => Some(Model.Status.Rejected) case "ADDED" => Some(Model.Status.Added) case s => isabelle.error("Unknown status: " + quote(s)) } } private def info_file(id: ID): Path = up(id) + Path.basic("info.json") private def patch_file(id: ID): Path = up(id) + Path.basic("patch") private val archive_name: String = "archive" def make_partial_patch(base_dir: Path, src: Path, dst: Path): String = { val patch = Isabelle_System.make_patch(base_dir, src, dst, "--unidirectional-new-file") split_lines(patch).filterNot(_.startsWith("Only in")).mkString("\n") } def save( state: State, metadata: Model.Metadata, message: String, archive: Bytes, file_extension: String ): (ID, State) = { val id = ID(Date.now()) val dir = up(id) dir.file.mkdirs() - val structure = AFP_Structure(dir) + val structure = AFP_Structure(base_dir = dir) structure.save_authors(metadata.authors.values.toList.sortBy(_.id)) metadata.entries.foreach(structure.save_entry) val archive_file = dir + Path.basic(archive_name + file_extension) Bytes.write(archive_file, archive) val metadata_rel = File.relative_path(afp.base_dir, afp.metadata_dir).getOrElse(afp.metadata_dir) val metadata_patch = make_partial_patch(afp.base_dir, metadata_rel, structure.metadata_dir) File.write(patch_file(id), metadata_patch) val info = JSON.Format(JSON.Object( "comment" -> message, "entries" -> metadata.entries.map(_.name), "notify" -> metadata.entries.flatMap(_.notifies).map(_.address).distinct)) File.write(info_file(id), info) signal(id, "done") (id, state) } def list(state: State): Model.Submission_List = Model.Submission_List( File.read_dir(up).flatMap(ID.unapply).reverse.flatMap { date => val id = ID(date) val day = date.rep.toLocalDate read_status(id).map( - Model.Overview(id, day, AFP_Structure(up(id)).entries_unchecked.head, _)) + Model.Overview(id, day, AFP_Structure(base_dir = up(id)).entries_unchecked.head, _)) }) def get(id: ID, state: State): Option[Model.Submission] = ID.check(id).filter(up(_).file.exists).map { id => - val structure = AFP_Structure(up(id)) + val structure = AFP_Structure(base_dir = up(id)) val authors = structure.load_authors val entries = structure.entries_unchecked.map( structure.load_entry(_, authors, state.topics, state.licenses, state.releases)) val log_file = down(id) + Path.basic("isabelle.log") val log = if (log_file.file.exists) Some(File.read(log_file)) else None val archive = get_archive(id).map(_.file_name) JSON.parse(File.read(info_file(id))) match { case JSON.Object(m) if m.contains("comment") => val comment = m("comment").toString val meta = Model.Metadata(authors, entries) Model.Submission(id, meta, read_build(id), read_status(id), comment, log, archive) case _ => isabelle.error("Could not read info") } } private def check(id: ID): Option[ID] = ID.check(id).filter(up(_).file.exists) def submit(id: ID): Unit = check(id).foreach(signal(_, "mail")) def set_status(id: ID, status: Model.Status.Value): Unit = check(id).foreach { id => val content = status match { case Model.Status.Submitted => "SUBMITTED" case Model.Status.Review => "PROCESSING" case Model.Status.Added => "ADDED" case Model.Status.Rejected => "REJECTED" } File.write(status_file(id), content) } def abort_build(id: ID): Unit = check(id).foreach(signal(_, "kill")) def get_patch(id: ID): Option[Path] = check(id).map(patch_file) def get_archive(id: ID): Option[Path] = check(id).flatMap { id => val dir = up(id) File.read_dir(dir).find(_.startsWith(archive_name + ".")).map(dir + Path.basic(_)) } } } /* paths */ object Page { val SUBMIT = Path.explode("submit") val SUBMISSION = Path.explode("submission") val SUBMISSIONS = Path.explode("submissions") } object API { val SUBMISSION = Path.explode("api/submission") val SUBMISSION_UPLOAD = Path.explode("api/submission/upload") val SUBMISSION_CREATE = Path.explode("api/submission/create") val SUBMISSION_STATUS = Path.explode("api/submission/status") val RESUBMIT = Path.explode("api/resubmit") val BUILD_ABORT = Path.explode("api/build/abort") val SUBMIT = Path.explode("api/submit") val SUBMISSION_AUTHORS_ADD = Path.explode("api/submission/authors/add") val SUBMISSION_AUTHORS_REMOVE = Path.explode("api/submission/authors/remove") val SUBMISSION_AFFILIATIONS_ADD = Path.explode("api/submission/affiliations/add") val SUBMISSION_AFFILIATIONS_REMOVE = Path.explode("api/submission/affiliations/remove") val SUBMISSION_ENTRIES_ADD = Path.explode("api/submission/entries/add") val SUBMISSION_ENTRIES_REMOVE = Path.explode("api/submission/entries/remove") val SUBMISSION_ENTRY_TOPICS_ADD = Path.explode("api/submission/entry/topics/add") val SUBMISSION_ENTRY_TOPICS_REMOVE = Path.explode("api/submission/entry/topics/remove") val SUBMISSION_ENTRY_AUTHORS_ADD = Path.explode("api/submission/entry/authors/add") val SUBMISSION_ENTRY_AUTHORS_REMOVE = Path.explode("api/submission/entry/authors/remove") val SUBMISSION_ENTRY_NOTIFIES_ADD = Path.explode("api/submission/entry/notifies/add") val SUBMISSION_ENTRY_NOTIFIES_REMOVE = Path.explode("api/submission/entry/notifies/remove") val SUBMISSION_ENTRY_RELATED_ADD = Path.explode("api/submission/entry/related/add") val SUBMISSION_ENTRY_RELATED_REMOVE = Path.explode("api/submission/entry/related/remove") val SUBMISSION_DOWNLOAD = Path.explode("api/download/patch") val SUBMISSION_DOWNLOAD_ZIP = Path.explode("api/download/archive.zip") val SUBMISSION_DOWNLOAD_TGZ = Path.explode("api/download/archive.tar.gz") val CSS = Path.explode("api/main.css") } /* view: html rendering and parameter parsing */ class View(paths: Web_App.Paths, mode: Mode.Value) { /* keys */ private val ABSTRACT = Params.key("abstract") private val ADDRESS = Params.key("address") private val AFFILIATION = Params.key("affiliation") private val ARCHIVE = Params.key("archive") private val AUTHOR = Params.key("author") private val DATE = Params.key("date") private val ENTRY = Params.key("entry") private val ID = Params.key("id") private val INPUT = Params.key("input") private val KIND = Params.key("kind") private val LICENSE = Params.key("license") private val MESSAGE = Params.key("message") private val NAME = Params.key("name") private val NOTIFY = Params.key("notify") private val ORCID = Params.key("orcid") private val RELATED = Params.key("related") private val STATUS = Params.key("status") private val TITLE = Params.key("title") private val TOPIC = Params.key("topic") private val ACTION = Params.key("action") /* utils */ def keyed(id: String, value: String): String = "[" + id + "] " + value def author_string(author: Author): String = { val orcid = author.orcid.map(orcid => " (ORCID id: " + orcid.identifier + ")").getOrElse("") keyed(author.id, author.name) + orcid } def author_option(author: Author): XML.Elem = option(author.id, author_string(author)) def affil_id(affil: Affiliation): String = affil match { case Unaffiliated(_) => "" case Email(_, id, _) => id case Homepage(_, id, _) => id } def affil_address(affil: Affiliation): String = affil match { case Unaffiliated(_) => "" case Email(_, _, address) => address case Homepage(_, _, url) => url.toString } def affil_string(affil: Affiliation): String = affil match { case Unaffiliated(_) => "No email or homepage" case Email(_, id, address) => keyed(id, address) case Homepage(_, id, url) => keyed(id, url.toString) } def related_string(related: Reference): String = related match { case Metadata.DOI(identifier) => identifier case Metadata.Formatted(rep) => rep } def fold[A](it: List[Params.Key], a: A)(f: (Params.Key, A) => Option[A]): Option[A] = it.foldLeft(Option(a)) { case (None, _) => None case (Some(a), key) => f(key, a) } def download_link(href: String, body: XML.Body): XML.Elem = class_("download")(link(href, body)) + ("target" -> "_blank") def frontend_link(path: Path, params: Properties.T, body: XML.Body): XML.Elem = link(paths.frontend_url(path, params).toString, body) + ("target" -> "_parent") def fieldlabel(for_elem: Params.Key, txt: String): XML.Elem = label(for_elem, " " + txt + ": ") def explanation(for_elem: Params.Key, txt: String): XML.Elem = par(List(emph(List(label(for_elem, txt))))) def action_button(call: String, label: String, action: Params.Key): XML.Elem = name(ACTION.print)(value(action.print)(api_button(call, label))) def render_if(cond: Boolean, body: XML.Body): XML.Body = if (cond) body else Nil def render_if(cond: Boolean, elem: XML.Elem): XML.Body = if (cond) List(elem) else Nil def render_error(for_elem: Params.Key, validated: Val[_]): XML.Body = validated.err.map(error => break ::: List(css("color: red")(label(for_elem, error)))).getOrElse(Nil) def render_metadata(metadata: Model.Metadata, state: State): XML.Body = { def render_topic(key: Params.Key, topic: Topic): XML.Elem = item(hidden(key + ID, topic.id) :: text(topic.id)) def render_affil(key: Params.Key, affil: Affiliation): XML.Elem = item( hidden(key + ID, affil.author) :: hidden(key + AFFILIATION, affil_id(affil)) :: text(author_string(metadata.authors(affil.author)) + ", " + affil_string(affil))) def render_related(key: Params.Key, related: Reference): XML.Elem = item( hidden(key + KIND, Model.Related.get(related).toString) :: hidden(key + INPUT, related_string(related)) :: input_raw(related_string(related)) :: Nil) def render_entry(key: Params.Key, entry: Entry): XML.Elem = fieldset(List( legend("Entry"), par(fieldlabel(key + TITLE, "Title") :: hidden(key + TITLE, entry.title) :: text(entry.title)), par(fieldlabel(key + NAME, "Short Name") :: hidden(key + NAME, entry.name) :: text(entry.name)), par(fieldlabel(key + DATE, "Date") :: hidden(key + DATE, entry.date.toString) :: text(entry.date.toString)), par(List(fieldlabel(Params.Key.empty, "Topics"), list(Params.indexed(key + TOPIC, entry.topics, render_topic)))), par(fieldlabel(key + LICENSE, "License") :: hidden(key + LICENSE, entry.license.id) :: text(entry.license.name)), par(List(fieldlabel(key + ABSTRACT, "Abstract"), hidden(key + ABSTRACT, entry.`abstract`), class_("mathjax_process")(span(List(input_raw(entry.`abstract`)))))), par(List(fieldlabel(Params.Key.empty, "Authors"), list(Params.indexed(key + AUTHOR, entry.authors, render_affil)))), par(List(fieldlabel(Params.Key.empty, "Contact"), list(Params.indexed(key + NOTIFY, entry.notifies, render_affil)))), par(List(fieldlabel(Params.Key.empty, "Related Publications"), list(Params.indexed(key + RELATED, entry.related, render_related)))))) def render_new_author(key: Params.Key, author: Author): XML.Elem = par(List( hidden(key + ID, author.id), hidden(key + NAME, author.name), hidden(key + ORCID, author.orcid.map(_.identifier).getOrElse("")))) def render_new_affil(key: Params.Key, affil: Affiliation): XML.Elem = par(List( hidden(key + AUTHOR, affil.author), hidden(key + ID, affil_id(affil)), hidden(key + AFFILIATION, affil_address(affil)))) Params.indexed(ENTRY, metadata.entries, render_entry) ::: Params.indexed(AUTHOR, metadata.new_authors(state), render_new_author) ::: Params.indexed(AFFILIATION, metadata.new_affils(state), render_new_affil) } /* rendering */ def render_create(model: Model.Create, state: State): XML.Body = { val updated_authors = model.updated_authors(state) val authors_list = updated_authors.values.toList.sortBy(_.id) val (entry_authors, other_authors) = updated_authors.values.toList.sortBy(_.id).partition(author => model.used_authors.contains(author.id)) val email_authors = authors_list.filter(_.emails.nonEmpty) def render_topic(key: Params.Key, topic: Topic): XML.Elem = par( hidden(key + ID, topic.id) :: text(topic.id) ::: action_button(paths.api_route(API.SUBMISSION_ENTRY_TOPICS_REMOVE), "x", key) :: Nil) def render_affil(key: Params.Key, affil: Affiliation): XML.Elem = { val author = updated_authors(affil.author) val affils = author.emails ::: author.homepages ::: Unaffiliated(author.id) :: Nil par( hidden(key + ID, affil.author) :: text(author_string(updated_authors(affil.author))) ::: selection(key + AFFILIATION, Some(affil_id(affil)), affils.map(affil => option(affil_id(affil), affil_string(affil)))) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_AUTHORS_REMOVE), "x", key) :: Nil) } def render_notify(key: Params.Key, email: Email): XML.Elem = { val author = updated_authors(email.author) par( hidden(key + ID, email.author) :: text(author_string(updated_authors(email.author))) ::: selection( key + AFFILIATION, Some(affil_id(email)), author.emails.map(affil => option(affil_id(affil), affil_string(affil)))) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_NOTIFIES_REMOVE), "x", key) :: Nil) } def render_related(key: Params.Key, related: Reference): XML.Elem = par( hidden(key + KIND, Model.Related.get(related).toString) :: hidden(key + INPUT, related_string(related)) :: text(related_string(related)) ::: action_button(paths.api_route(API.SUBMISSION_ENTRY_RELATED_REMOVE), "x", key) :: Nil) def render_entry(key: Params.Key, entry: Model.Create_Entry): XML.Elem = fieldset(legend("Entry") :: par( fieldlabel(key + TITLE, "Title of article") :: textfield(key + TITLE, "Example Submission", entry.title.v) :: render_error(key + TITLE, entry.title)) :: par( fieldlabel(key + NAME, "Short name") :: textfield(key + NAME, "Example_Submission", entry.name.v) :: explanation(key + NAME, "Name of the folder where your ROOT and theory files reside.") :: render_error(key + NAME, entry.name)) :: fieldset(legend("Topics") :: Params.indexed(key + TOPIC, entry.topics.v, render_topic) ::: selection(key + TOPIC, entry.topic_input.map(_.id), state.topics.values.toList.map(topic => option(topic.id, topic.id))) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_TOPICS_ADD), "add", key) :: render_error(Params.Key.empty, entry.topics)) :: par(List( fieldlabel(key + LICENSE, "License"), radio(key + LICENSE, Params.Key.explode(entry.license.id), state.licenses.values.toList.map(license => Params.Key.explode(license.id) -> license.name)), explanation(key + LICENSE, "Note: For LGPL submissions, please include the header \"License: LGPL\" in each file"))) :: par( fieldlabel(key + ABSTRACT, "Abstract") :: placeholder("HTML and MathJax, no LaTeX")( textarea(key + ABSTRACT, entry.`abstract`.v) + ("rows" -> "8") + ("cols" -> "70")) :: explanation(key + ABSTRACT, "Note: You can use HTML or MathJax (not LaTeX!) to format your abstract.") :: render_error(key + ABSTRACT, entry.`abstract`)) :: fieldset(legend("Authors") :: Params.indexed(key + AUTHOR, entry.affils.v, render_affil) ::: selection(key + AUTHOR, entry.author_input.map(_.id), authors_list.map(author => option(author.id, author_string(author)))) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_AUTHORS_ADD), "add", key) :: explanation(key + AUTHOR, "Add an author from the list. Register new authors first below.") :: render_error(key + AUTHOR, entry.affils)) :: fieldset(legend("Contact") :: Params.indexed(key + NOTIFY, entry.notifies.v, render_notify) ::: selection(key + NOTIFY, entry.notify_input.map(_.id), optgroup("Suggested", email_authors.filter(author => entry.used_authors.contains(author.id)).map(author_option)) :: email_authors.filter(author => !entry.used_authors.contains(author.id)).map(author_option)) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_NOTIFIES_ADD), "add", key) :: explanation(key + NOTIFY, "These addresses serve two purposes: " + "1. They are used to send you updates about the state of your submission. " + "2. They are the maintainers of the entry once it is accepted. " + "Typically this will be one or more of the authors.") :: render_error(Params.Key.empty, entry.notifies)) :: fieldset(legend("Related Publications") :: Params.indexed(key + RELATED, entry.related, render_related) ::: selection(key + RELATED + KIND, entry.related_kind.map(_.toString), Model.Related.values.toList.map(v => option(v.toString, v.toString))) :: textfield(key + RELATED + INPUT, "10.1109/5.771073", entry.related_input.v) :: action_button(paths.api_route(API.SUBMISSION_ENTRY_RELATED_ADD), "add", key) :: explanation(key + RELATED + INPUT, "Publications related to the entry, as DOIs (10.1109/5.771073) or plaintext (HTML)." + "Typically a publication by the authors describing the entry," + " background literature (articles, books) or web resources. ") :: render_error(key + RELATED + INPUT, entry.related_input)) :: render_if(mode == Mode.SUBMISSION, action_button(paths.api_route(API.SUBMISSION_ENTRIES_REMOVE), "remove entry", key))) def render_new_author(key: Params.Key, author: Author): XML.Elem = par( hidden(key + ID, author.id) :: hidden(key + NAME, author.name) :: hidden(key + ORCID, author.orcid.map(_.identifier).getOrElse("")) :: text(author_string(author)) ::: render_if(!model.used_authors.contains(author.id), action_button(paths.api_route(API.SUBMISSION_AUTHORS_REMOVE), "x", key))) def render_new_affil(key: Params.Key, affil: Affiliation): XML.Elem = par( hidden(key + AUTHOR, affil.author) :: hidden(key + ID, affil_id(affil)) :: hidden(key + AFFILIATION, affil_address(affil)) :: text(author_string(updated_authors(affil.author)) + ": " + affil_string(affil)) ::: render_if(!model.used_affils.contains(affil), action_button(paths.api_route(API.SUBMISSION_AFFILIATIONS_REMOVE), "x", key))) val (upload, preview) = mode match { case Mode.EDIT => ("Save", "preview and save >") case Mode.SUBMISSION => ("Upload", "preview and upload >") } List(submit_form(paths.api_route(API.SUBMISSION), Params.indexed(ENTRY, model.entries.v, render_entry) ::: render_error(Params.Key.empty, model.entries) ::: render_if(mode == Mode.SUBMISSION, par(List( explanation(Params.Key.empty, "You can submit multiple entries at once. " + "Put the corresponding folders in the archive " + "and use the button below to add more input fields for metadata. "), api_button(paths.api_route(API.SUBMISSION_ENTRIES_ADD), "additional entry")))) ::: break ::: fieldset(legend("New Authors") :: explanation(Params.Key.empty, "If you are new to the AFP, add yourself here.") :: Params.indexed(AUTHOR, model.new_authors.v, render_new_author) ::: fieldlabel(AUTHOR + NAME, "Name") :: textfield(AUTHOR + NAME, "Gerwin Klein", model.new_author_input) :: fieldlabel(AUTHOR + ORCID, "ORCID id (optional)") :: textfield(AUTHOR + ORCID, "0000-0002-1825-0097", model.new_author_orcid) :: api_button(paths.api_route(API.SUBMISSION_AUTHORS_ADD), "add") :: render_error(Params.Key.empty, model.new_authors)) :: fieldset(legend("New email or homepage") :: explanation(Params.Key.empty, "Add new email or homepages here. " + "If you would like to update an existing, " + "submit with the old one and write to the editors.") :: Params.indexed(AFFILIATION, model.new_affils.v, render_new_affil) ::: fieldlabel(AFFILIATION, "Author") :: selection(AFFILIATION, model.new_affils_author.map(_.id), optgroup("Entry authors", entry_authors.map(author_option)) :: other_authors.map(author_option)) :: fieldlabel(AFFILIATION + ADDRESS, "Email or Homepage") :: textfield(AFFILIATION + ADDRESS, "https://proofcraft.org", model.new_affils_input) :: api_button(paths.api_route(API.SUBMISSION_AFFILIATIONS_ADD), "add") :: render_error(Params.Key.empty, model.new_affils)) :: break ::: fieldset(List(legend(upload), api_button(paths.api_route(API.SUBMISSION_UPLOAD), preview))) :: Nil)) } def render_submission(submission: Model.Submission, state: State): XML.Body = { def status_text(status: Option[Model.Status.Value]): String = status.map { case Model.Status.Submitted => "AFP editors notified." case Model.Status.Review => "Review in progress." case Model.Status.Added => "Added to the AFP." case Model.Status.Rejected => "Submission rejected." } getOrElse "Draft saved. Check the logs for errors and warnings, " + "and submit to editors once successfully built." def render_archive(archive: Option[String]): XML.Body = { val archive_url = archive match { case Some(archive) if archive.endsWith(".zip") => Some(API.SUBMISSION_DOWNLOAD_ZIP) case Some(archive) if archive.endsWith(".tar.gz") => Some(API.SUBMISSION_DOWNLOAD_TGZ) case _ => None } archive_url match { case Some(url) => List(download_link(paths.api_route(url, List(ID.print -> submission.id)), text("archive"))) case None => Nil } } val resubmit = mode match { case Mode.EDIT => "Update" case Mode.SUBMISSION => "Resubmit" } def render_log(log: Option[String]): XML.Body = log match { case None => text("Waiting for build...") case Some(log) => text("Isabelle log:") ::: source(log) :: Nil } List(submit_form(paths.api_route(Page.SUBMISSION, List(ID.print -> submission.id)), render_if(mode == Mode.SUBMISSION, render_archive(submission.archive) ::: download_link(paths.api_route(API.SUBMISSION_DOWNLOAD, List(ID.print -> submission.id)), text("metadata patch")) :: text(" (apply with: 'patch -p0 < FILE')")) ::: render_if(mode == Mode.SUBMISSION, par( hidden(MESSAGE, submission.message) :: text("Comment: " + submission.message))) ::: section("Metadata") :: render_metadata(submission.meta, state) ::: section("Status") :: span(text(status_text(submission.status))) :: render_if(submission.build != Model.Build.Running, action_button(paths.api_route(API.RESUBMIT), resubmit, Params.Key.explode(submission.id))) ::: render_if(submission.build == Model.Build.Running, action_button(paths.api_route(API.BUILD_ABORT), "Abort build", Params.Key.explode(submission.id))) ::: render_if(submission.build == Model.Build.Success && submission.status.isEmpty, action_button(paths.api_route(API.SUBMIT), "Send submission to AFP editors", Params.Key.explode(submission.id))) ::: render_if(mode == Mode.SUBMISSION, fieldset(legend("Build") :: bold(text(submission.build.toString)) :: par(render_log(submission.log)) :: Nil)))) } def render_upload(upload: Model.Upload, state: State): XML.Body = { val submit = mode match { case Mode.EDIT => "save" case Mode.SUBMISSION => "submit" } List(submit_form(paths.api_route(API.SUBMISSION), List( fieldset(legend("Overview") :: render_metadata(upload.metadata, state)), fieldset(legend("Submit") :: api_button(paths.api_route(API.SUBMISSION), "< edit metadata") :: render_if(mode == Mode.SUBMISSION, List( par(List( fieldlabel(MESSAGE, "Message for the editors (optional)"), textfield(MESSAGE, "", upload.message), explanation( MESSAGE, "Note: Anything special or noteworthy about your submission can be covered here. " + "It will not become part of your entry. " + "You're also welcome to leave suggestions for our AFP submission service here. ") )), par(List( fieldlabel(ARCHIVE, "Archive file (.tar.gz or .zip)"), browse(ARCHIVE, List(".zip", ".tar.gz")), explanation(ARCHIVE, "Note: Your zip or tar file must contain exactly one folder for each entry with your theories, ROOT, etc. " + "The folder name must be the short/folder name used in the submission form. " + "Hidden files and folders (e.g., __MACOSX) are not allowed."))))) ::: api_button(paths.api_route(API.SUBMISSION_CREATE), submit) :: render_error(ARCHIVE, Val.err((), upload.error)))))) } def render_submission_list(submission_list: Model.Submission_List): XML.Body = { def render_overview(key: Params.Key, overview: Model.Overview): XML.Elem = item( hidden(key + ID, overview.id) :: hidden(key + DATE, overview.date.toString) :: hidden(key + NAME, overview.name) :: span(text(overview.date.toString)) :: span(List(frontend_link(Page.SUBMISSION, List(ID.print -> overview.id), text(overview.name)))) :: render_if(mode == Mode.SUBMISSION, class_("right")(span(List( selection(key + STATUS, Some(overview.status.toString), Model.Status.values.toList.map(v => option(v.toString, v.toString))), action_button(paths.api_route(API.SUBMISSION_STATUS), "update", key)))))) def list1(ls: List[XML.Elem]): XML.Elem = if (ls.isEmpty) par(Nil) else list(ls) val ls = Params.indexed(ENTRY, submission_list.submissions, (k, s) => (k, s)) val finished = ls.filter(t => Set(Model.Status.Added, Model.Status.Rejected).contains(t._2.status)) List(submit_form(paths.api_route(API.SUBMISSION_STATUS), render_if(mode == Mode.SUBMISSION, text("Open") ::: list1(ls.filter(_._2.status == Model.Status.Submitted).map(render_overview)) :: text("In Progress") ::: list1(ls.filter(_._2.status == Model.Status.Review).map(render_overview)) :: text("Finished")) ::: list1(finished.map(render_overview)) :: Nil)) } def render_created(created: Model.Created): XML.Body = { val status = mode match { case Mode.SUBMISSION => "View your submission status: " case Mode.EDIT => "View the entry at: " } List(div( span(text("Entry successfully saved. " + status)) :: break ::: frontend_link(Page.SUBMISSION, List(ID.print -> created.id), text(paths.frontend_url(Page.SUBMISSION, List(ID.print -> created.id)).toString)) :: break ::: render_if(mode == Mode.SUBMISSION, span(text("(keep that url!)."))))) } def render_invalid: XML.Body = text("Invalid request") def render_head: XML.Body = List( XML.Elem(Markup("script", List( "type" -> "text/javascript", "id" -> "MathJax-script", "async" -> "async", "src" -> "https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js")), text("\n")), script( "MathJax={tex:{inlineMath:[['$','$'],['\\\\(','\\\\)']]},processEscapes:true,svg:{fontCache:'global'}}"), style_file(paths.api_route(API.CSS))) /* param parsing */ def parse_create(params: Params.Data, state: State): Option[Model.Create] = { def parse_topic(key: Params.Key, topics: List[Topic]): Option[Topic] = Model.validate_topic(params(key + ID), topics, state).opt def parse_email(key: Params.Key, authors: Authors): Option[Email] = authors.get(params(key + ID)).flatMap(_.emails.find(_.id == params(key + AFFILIATION))) def parse_affil(key: Params.Key, authors: Authors): Option[Affiliation] = authors.get(params(key + ID)).flatMap { author => val id = params(key + AFFILIATION) if (id.isEmpty) Some(Unaffiliated(author.id)) else (author.emails ++ author.homepages).collectFirst { case e: Email if e.id == id => e case h: Homepage if h.id == id => h } } def parse_related(key: Params.Key, references: List[Reference]): Option[Reference] = Model.Related.from_string(params(key + KIND)).flatMap( Model.validate_related(_, params(key + INPUT), references).opt) def parse_new_author(key: Params.Key, authors: Authors): Option[Author] = Model.validate_new_author( params(key + ID), params(key + NAME), params(key + ORCID), authors).opt def parse_new_affil(key: Params.Key, authors: Authors): Option[Affiliation] = authors.get(params(key + AUTHOR)).flatMap(author => Model.validate_new_affil(params(key + ID), params(key + AFFILIATION), author).opt) def parse_entry(key: Params.Key, authors: Authors): Option[Model.Create_Entry] = for { topics <- fold(params.list(key + TOPIC), List.empty[Topic]) { case (key, topics) => parse_topic(key, topics).map(topics :+ _) } affils <- fold(params.list(key + AUTHOR), List.empty[Affiliation]) { case (key, affils) => parse_affil(key, authors).map(affils :+ _) } notifies <- fold(params.list(key + NOTIFY), List.empty[Email]) { case (key, emails) => parse_email(key, authors).map(emails :+ _) } related <- fold(params.list(key + RELATED), List.empty[Reference]) { case (key, references) => parse_related(key, references).map(references :+ _) } license <- state.licenses.get(params(key + LICENSE)) } yield Model.Create_Entry( name = Val.ok(params(key + NAME)), title = Val.ok(params(key + TITLE)), topics = Val.ok(topics), topic_input = state.topics.get(params(key + TOPIC)), license = license, `abstract` = Val.ok(params(key + ABSTRACT)), author_input = authors.get(params(key + AUTHOR)), notify_input = authors.get(params(key + NOTIFY)), affils = Val.ok(affils), notifies = Val.ok(notifies), related = related, - related_kind = Model.Related.from_string(params(RELATED + KIND)), - related_input = Val.ok(params(RELATED + INPUT))) + related_kind = Model.Related.from_string(params(key + RELATED + KIND)), + related_input = Val.ok(params(key + RELATED + INPUT))) for { (new_author_ids, all_authors) <- fold(params.list(AUTHOR), (List.empty[Author.ID], state.authors)) { case (key, (new_authors, authors)) => parse_new_author(key, authors).map(author => (new_authors :+ author.id, authors.updated(author.id, author))) } (new_affils, all_authors) <- fold(params.list(AFFILIATION), (List.empty[Affiliation], all_authors)) { case (key, (new_affils, authors)) => parse_new_affil(key, authors).map { affil => val author = authors(affil.author) (new_affils :+ affil, affil match { case _: Unaffiliated => authors case e: Email => authors.updated(author.id, author.copy(emails = author.emails :+ e)) case h: Homepage => authors.updated(author.id, author.copy(homepages = author.homepages :+ h)) }) } } new_authors = new_author_ids.map(all_authors) entries <- fold(params.list(ENTRY), List.empty[Model.Create_Entry]) { case (key, entries) => parse_entry(key, all_authors).map(entries :+ _) } } yield Model.Create( entries = Val.ok(entries), new_authors = Val.ok(new_authors), new_author_input = params(AUTHOR + NAME), new_author_orcid = params(AUTHOR + ORCID), new_affils = Val.ok(new_affils), new_affils_author = all_authors.get(params(AFFILIATION)), new_affils_input = params(AFFILIATION + ADDRESS)) } def parse_submission_list(params: Params.Data): Option[Model.Submission_List] = { def parse_overview(key: Params.Key): Option[Model.Overview] = for { date <- Exn.capture(LocalDate.parse(params(key + DATE))) match { case Exn.Res(date) => Some(date) case Exn.Exn(_) => None } status <- Model.Status.from_string(params(key + STATUS)) } yield Model.Overview(params(key + ID), date, params(key + NAME), status) val submissions = fold(params.list(ENTRY), List.empty[Model.Overview]) { case (key, overviews) => parse_overview(key).map(overviews :+ _) } submissions.map(Model.Submission_List.apply) } def parse_num_entry(action: Params.Key): Option[Int] = action.get(ENTRY).flatMap(_.num) def parse_num_affil(num_entry: Int, action: Params.Key): Option[Int] = action.get(ENTRY + num_entry + AUTHOR).flatMap(_.num) def parse_num_notify(num_entry: Int, action: Params.Key): Option[Int] = action.get(ENTRY + num_entry + NOTIFY).flatMap(_.num) def parse_num_topic(num_entry: Int, action: Params.Key): Option[Int] = action.get(ENTRY + num_entry + TOPIC).flatMap(_.num) def parse_num_related(num_entry: Int, action: Params.Key): Option[Int] = action.get(ENTRY + num_entry + RELATED).flatMap(_.num) def parse_num_new_author(action: Params.Key): Option[Int] = action.get(AUTHOR).flatMap(_.num) def parse_num_new_affil(action: Params.Key): Option[Int] = action.get(AFFILIATION).flatMap(_.num) def parse_id(props: Properties.T): Option[String] = Properties.get(props, ID.print) def action(params: Params.Data): Params.Key = Params.Key.explode(params(ACTION)) def message(params: Params.Data): String = params(MESSAGE) def archive_file(params: Params.Data): Bytes = params.file(ARCHIVE).getOrElse(Bytes.empty) def archive_filename(params: Params.Data): String = params(ARCHIVE) } /* server */ object State { def load(afp: AFP_Structure): State = { val authors = afp.load_authors val topics = afp.load_topics val licenses = afp.load_licenses val releases = afp.load_releases val entries = afp.load_entries(authors, topics, licenses, releases) State(authors, topics, licenses, releases, entries) } } case class State( authors: Authors, topics: Topics, licenses: Licenses, releases: Releases, entries: Entries) object Mode extends Enumeration { val EDIT, SUBMISSION = Value } class Server( paths: Web_App.Paths, afp: AFP_Structure, mode: Mode.Value, handler: Handler, devel: Boolean, verbose: Boolean, progress: Progress, port: Int ) extends Web_App.Server[Model.T](paths, port, verbose, progress) { private var _state: State = State.load(afp) val repo = Mercurial.the_repository(afp.base_dir) val view = new View(paths, mode) def render(model: Model.T): XML.Body = model match { case create: Model.Create => view.render_create(create, _state) case upload: Model.Upload => view.render_upload(upload, _state) case submission: Model.Submission => view.render_submission(submission, _state) case submissions: Model.Submission_List => view.render_submission_list(submissions) case created: Model.Created => view.render_created(created) case Model.Invalid => view.render_invalid } /* control */ def add_entry(params: Params.Data): Option[Model.T] = for (model <- view.parse_create(params, _state)) yield model.add_entry(_state) def remove_entry(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) } yield model.remove_entry(num_entry) def add_author(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) entry <- model.entries.v.unapply(num_entry) } yield model.update_entry(num_entry, entry.add_affil) def remove_author(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) num_affil <- view.parse_num_affil(num_entry, view.action(params)) entry <- model.entries.v.unapply(num_entry) affil <- entry.affils.v.unapply(num_affil) } yield model.update_entry(num_entry, entry.remove_affil(affil)) def add_notify(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) entry <- model.entries.v.unapply(num_entry) entry1 <- entry.add_notify } yield model.update_entry(num_entry, entry1) def remove_notify(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) num_notify <- view.parse_num_notify(num_entry, view.action(params)) entry <- model.entries.v.unapply(num_entry) notify <- entry.notifies.v.unapply(num_notify) } yield model.update_entry(num_entry, entry.remove_notify(notify)) def add_topic(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) entry <- model.entries.v.unapply(num_entry) } yield model.update_entry(num_entry, entry.add_topic(_state)) def remove_topic(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) num_topic <- view.parse_num_topic(num_entry, view.action(params)) entry <- model.entries.v.unapply(num_entry) topic <- entry.topics.v.unapply(num_topic) } yield model.update_entry(num_entry, entry.remove_topic(topic)) def add_related(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) entry <- model.entries.v.unapply(num_entry) } yield model.update_entry(num_entry, entry.add_related) def remove_related(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_entry <- view.parse_num_entry(view.action(params)) num_related <- view.parse_num_related(num_entry, view.action(params)) entry <- model.entries.v.unapply(num_entry) related <- entry.related.unapply(num_related) } yield model.update_entry(num_entry, entry.remove_related(related)) def add_new_author(params: Params.Data): Option[Model.T] = for (model <- view.parse_create(params, _state)) yield model.add_new_author(_state) def remove_new_author(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_author <- view.parse_num_new_author(view.action(params)) author <- model.new_authors.v.unapply(num_author) model1 <- model.remove_new_author(author) } yield model1 def add_new_affil(params: Params.Data): Option[Model.T] = for (model <- view.parse_create(params, _state)) yield model.add_new_affil def remove_new_affil(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) num_affil <- view.parse_num_new_affil(view.action(params)) affil <- model.new_affils.v.unapply(num_affil) model1 <- model.remove_new_affil(affil) } yield model1 def upload(params: Params.Data): Option[Model.T] = for (model <- view.parse_create(params, _state)) yield model.validate(_state, view.message(params), mode == Mode.EDIT) def create(params: Params.Data): Option[Model.T] = for { model <- view.parse_create(params, _state) upload <- model.validate(_state, view.message(params), mode == Mode.EDIT) match { case upload: Model.Upload => Some(upload) case _ => None } } yield synchronized { val (model1, state) = mode match { case Mode.EDIT => upload.save(handler, _state) case Mode.SUBMISSION => upload.submit(handler, view.archive_file(params), view.archive_filename(params), _state) } _state = state model1 } def empty_submission: Option[Model.T] = Some(Model.Create.init(_state)) def get_submission(props: Properties.T): Option[Model.Submission] = for { id <- view.parse_id(props) submission <- handler.get(id, _state) } yield submission def resubmit(params: Params.Data): Option[Model.T] = for (submission <- handler.get(view.action(params).print, _state)) yield Model.Upload(submission) def submit(params: Params.Data): Option[Model.T] = for { submission <- handler.get(view.action(params).print, _state) submission1 <- submission.submit(handler) } yield submission1 def abort_build(params: Params.Data): Option[Model.T] = for { submission <- handler.get(view.action(params).print, _state) submission1 <- submission.abort_build(handler) } yield submission1 def submission(params: Params.Data): Option[Model.T] = view.parse_create(params, _state) def set_status(params: Params.Data): Option[Model.T] = for { model <- view.parse_submission_list(params) num_entry <- view.parse_num_entry(view.action(params)) entry <- model.submissions.unapply(num_entry) } yield synchronized { if (!devel) { val updated = entry.update_repo(repo) if (updated) { progress.echo_if(verbose, "Updating server data...") _state = State.load(afp) progress.echo("Updated repo to " + repo.id()) } } model } def submission_list: Option[Model.T] = Some(handler.list(_state)) def download(props: Properties.T): Option[Path] = for { id <- view.parse_id(props) patch <- handler.get_patch(id) } yield patch def download_archive(props: Properties.T): Option[Path] = for { id <- view.parse_id(props) archive <- handler.get_archive(id) } yield archive def style_sheet: Option[Path] = Some(afp.base_dir + Path.make(List("tools", "main.css"))) val error_model = Model.Invalid val endpoints = List( Get(Page.SUBMIT, "empty submission form", _ => empty_submission), Get(Page.SUBMISSION, "get submission", get_submission), Get(Page.SUBMISSIONS, "list submissions", _ => submission_list), Get_File(API.SUBMISSION_DOWNLOAD, "download patch", download), Get_File(API.SUBMISSION_DOWNLOAD_ZIP, "download archive", download_archive), Get_File(API.SUBMISSION_DOWNLOAD_TGZ, "download archive", download_archive), Get_File(API.CSS, "download css", _ => style_sheet), Post(API.RESUBMIT, "get form for resubmit", resubmit), Post(API.SUBMIT, "submit to editors", submit), Post(API.BUILD_ABORT, "abort the build", abort_build), Post(API.SUBMISSION, "get submission form", submission), Post(API.SUBMISSION_AUTHORS_ADD, "add author", add_new_author), Post(API.SUBMISSION_AUTHORS_REMOVE, "remove author", remove_new_author), Post(API.SUBMISSION_AFFILIATIONS_ADD, "add affil", add_new_affil), Post(API.SUBMISSION_AFFILIATIONS_REMOVE, "remove affil", remove_new_affil), Post(API.SUBMISSION_ENTRIES_ADD, "add entry", add_entry), Post(API.SUBMISSION_ENTRIES_REMOVE, "remove entry", remove_entry), Post(API.SUBMISSION_ENTRY_AUTHORS_ADD, "add entry author", add_author), Post(API.SUBMISSION_ENTRY_AUTHORS_REMOVE, "remove entry author", remove_author), Post(API.SUBMISSION_ENTRY_NOTIFIES_ADD, "add notify", add_notify), Post(API.SUBMISSION_ENTRY_NOTIFIES_REMOVE, "remove notify", remove_notify), Post(API.SUBMISSION_ENTRY_TOPICS_ADD, "add topic", add_topic), Post(API.SUBMISSION_ENTRY_TOPICS_REMOVE, "remove topic", remove_topic), Post(API.SUBMISSION_ENTRY_RELATED_ADD, "add related", add_related), Post(API.SUBMISSION_ENTRY_RELATED_REMOVE, "remove related", remove_related), Post(API.SUBMISSION_UPLOAD, "upload archive", upload), Post(API.SUBMISSION_CREATE, "create submission", create), Post(API.SUBMISSION_STATUS, "set submission status", set_status)) val head = view.render_head } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("afp_submit", "start afp submission server", Scala_Project.here, { args => var backend_path = Path.current var frontend = "http://localhost" var devel = false var verbose = false var port = 8080 - var dir: Option[Path] = None val getopts = Getopts(""" -Usage: isabelle afp_submit [OPTIONS] +Usage: isabelle afp_submit [OPTIONS] DIR Options are: -a PATH backend path (if endpoint is not server root) -b URL application frontend url. Default: """ + frontend + """ -d devel mode (serves frontend and skips automatic AFP repository updates) -p PORT server port. Default: """ + port + """ -v verbose - -D DIR submission directory - Start afp submission server. Server is in "edit" mode - unless directory to store submissions in is specified. + Start afp submission server for specified submission directory. """, "a:" -> (arg => backend_path = Path.explode(arg)), "b:" -> (arg => frontend = arg), "d" -> (_ => devel = true), "p:" -> (arg => port = Value.Int.parse(arg)), - "v" -> (_ => verbose = true), - "D:" -> (arg => dir = Some(Path.explode(arg)))) + "v" -> (_ => verbose = true)) - getopts(args) + val dir = + getopts(args) match { + case dir :: Nil => Path.explode(dir) + case _ => getopts.usage() + } val afp = AFP_Structure() val progress = new Console_Progress(verbose = verbose) - val (handler, mode) = dir match { - case Some(dir) => (Handler.Adapter(dir, afp), Mode.SUBMISSION) - case None => (Handler.Edit(afp), Mode.EDIT) - } + val handler = Handler.Adapter(dir, afp) val paths = Web_App.Paths(Url(frontend + ":" + port), backend_path, serve_frontend = devel, landing = Page.SUBMISSIONS) - val server = new Server(paths = paths, afp = afp, mode = mode, + val server = new Server(paths = paths, afp = afp, mode = Mode.SUBMISSION, handler = handler, devel = devel, verbose = verbose, progress = progress, port = port) server.run() }) + + val isabelle_tool1 = Isabelle_Tool("afp_edit_metadata", "edit AFP metadata", + Scala_Project.here, + { args => + var verbose = false + var port = 8080 + + val getopts = Getopts(""" +Usage: isabelle afp_submit [OPTIONS] + + Options are: + -p PORT server port. Default: """ + port + """ + -v verbose + + Start afp server to edit metadata. +""", + "p:" -> (arg => port = Value.Int.parse(arg)), + "v" -> (_ => verbose = true)) + + val afp = AFP_Structure() + + val progress = new Console_Progress(verbose = verbose) + + val handler = Handler.Edit(afp) + + val paths = Web_App.Paths(Url("http://localhost:" + port), Path.current, + serve_frontend = true, landing = Page.SUBMISSIONS) + val server = new Server(paths = paths, afp = afp, mode = Mode.EDIT, + handler = handler, devel = true, verbose = verbose, progress = progress, port = port) + + server.run() + }) } diff --git a/tools/afp_tool.scala b/tools/afp_tool.scala --- a/tools/afp_tool.scala +++ b/tools/afp_tool.scala @@ -1,13 +1,14 @@ package afp import isabelle._ class Tools extends Isabelle_Scala_Tools( AFP_Site_Gen.isabelle_tool, AFP_Check_Roots.isabelle_tool, AFP_Check_Metadata.isabelle_tool, AFP_Dependencies.isabelle_tool, AFP_Release.isabelle_tool, - AFP_Submit.isabelle_tool) + AFP_Submit.isabelle_tool, + AFP_Submit.isabelle_tool1)