diff --git a/tools/afp_build.scala b/tools/afp_build.scala
--- a/tools/afp_build.scala
+++ b/tools/afp_build.scala
@@ -1,347 +1,345 @@
/* Author: Lars Hupel and Fabian Huch, TU Muenchen
Unified AFP CI integration.
*/
package afp
import isabelle.*
import isabelle.CI_Build.{hg_id, print_section, Build_Config, Failed, Job, Profile, Result, Status}
-import afp.Metadata.{Email, Entry}
+import afp.Metadata.{Email, Entry, Entries}
import java.time.{Instant, ZoneId}
import java.time.format.DateTimeFormatter
import java.util.{Map => JMap, Properties => JProperties}
object AFP_Build {
/* mailing */
object Mailer {
def failed_subject(name: Entry.Name): String = s"Build of AFP entry $name failed"
def failed_text(session_name: String, entry: Entry.Name, isabelle_id: String,
afp_id: String, result: Process_Result): String = s"""
The build for the session
$session_name,
belonging to the AFP entry
$entry
failed.
You are receiving this mail because you are the maintainer of that AFP
entry.
The following information might help you with resolving the problem.
Build log: ${Isabelle_System.getenv("BUILD_URL")}
Isabelle ID: $isabelle_id
AFP ID: $afp_id
Timeout? ${result.timeout}
Exit code: ${result.rc}
Last 50 lines from stdout (if available):
${result.out_lines.takeRight(50).mkString("\n")}
Last 50 lines from stderr (if available):
${result.err_lines.takeRight(50).mkString("\n")}
"""
}
/* metadata tooling */
class Metadata_Tools private(
val structure: AFP_Structure,
val server: Mail.Server,
- val entries: Map[Entry.Name, Entry]
+ val entries: Entries
) {
def maintainers(name: Entry.Name): List[Email] = {
entries.get(name) match {
case None => Nil
case Some(entry) => entry.notifies
}
}
val sessions: Map[Entry.Name, List[String]] =
entries.values.map(entry =>
entry.name -> structure.entry_sessions(entry.name).map(_.name)).toMap
def session_entry(session_name: String): Option[Entry.Name] = {
val entry = sessions.find { case (_, sessions) => sessions.contains(session_name) }
entry.map { case (name, _) => name }
}
def by_entry(sessions: List[String]): Map[Option[Entry.Name], List[String]] =
sessions.groupBy(session_entry)
def notify(name: Entry.Name, subject: String, text: String): Boolean = {
val recipients = entries.get(name).map(_.notifies).getOrElse(Nil)
if (recipients.nonEmpty) {
val from = Some(Mail.address("ci@isabelle.systems"))
val to = recipients.map(mail => Mail.address(mail.address))
val mail = Mail(subject, to, text, from, "Jenkins Admin")
server.send(mail)
}
recipients.nonEmpty
}
}
object Metadata_Tools {
- def load(afp: AFP_Structure, options: Options): Metadata_Tools = {
- val entries = afp.load().map(entry => entry.name -> entry).toMap
- new Metadata_Tools(afp, CI_Build.mail_server(options), entries)
- }
+ def load(afp: AFP_Structure, options: Options): Metadata_Tools =
+ new Metadata_Tools(afp, CI_Build.mail_server(options), afp.load())
}
/* utilities */
def status_as_json(isabelle_id: String, afp_id: String, start_time: String,
status: Map[Option[String], Status]): String = {
val entries_strings = status.collect {
case (Some(entry), status) =>
s"""{"entry": "$entry", "status": "${status.str}"}"""
}
val entries_string = entries_strings.mkString("[", ",\n", "]")
s"""
{"build_data":
{"isabelle_id": "$isabelle_id",
"afp_id": "$afp_id",
"time": "$start_time",
"url": "${Isabelle_System.getenv("BUILD_URL")}",
"job": "${Isabelle_System.getenv("JOB_NAME")}"
},
"entries":
$entries_string
}
"""
}
def status_as_html(status: Map[Option[String], Status]): String = {
val entries_strings = status.collect {
case (None, Failed) =>
s"Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
/* ci build jobs */
val afp =
Job("afp", "builds the AFP, without slow sessions", Profile.from_host,
{
val afp = AFP_Structure()
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def pre_hook(options: Options): Result = {
println(s"AFP id ${ afp.hg_id }")
if (status_file.exists())
status_file.delete()
Result.ok
}
def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
print_section("COMPLETED")
Result.ok
}
Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection = Sessions.Selection(
session_groups = List("AFP"),
exclude_session_groups = List("slow")))
})
val all =
Job("all", "builds Isabelle + AFP (without slow)", Profile.from_host,
{
val afp = AFP_Structure()
val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
val isabelle_id = hg_id(isabelle_home)
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def pre_hook(options: Options): Result = {
println(s"AFP id ${ afp.hg_id }")
if (status_file.exists())
status_file.delete()
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
val server = CI_Build.mail_server(options)
if (!server.defined) {
println(s"Mail configuration not found.")
Result.error
}
else {
server.check()
Result.ok
}
}
def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
val metadata = Metadata_Tools.load(afp, options)
val status = metadata.by_entry(results.sessions.toList).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
}.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, status_as_html(status))
print_section("SITEGEN")
println("Writing status file ...")
val formatted_time =
start_time.instant.atZone(ZoneId.systemDefault)
.format(DateTimeFormatter.RFC_1123_DATE_TIME)
File.write(status_file, status_as_json(isabelle_id, afp.hg_id, formatted_time, status))
println("Running sitegen ...")
val script = afp.base_dir + Path.explode("admin/sitegen-devel")
val sitegen_cmd =
Bash.strings(List(script.file.toString, status_file.toString, deps_file.toString))
val sitegen_res =
Isabelle_System.bash(sitegen_cmd, progress_stdout = println, progress_stderr = println)
if (!sitegen_res.ok) {
println("sitegen failed")
}
if (!results.ok) {
print_section("NOTIFICATIONS")
for (session_name <- results.sessions) {
val result = results(session_name)
if (!result.ok && !results.cancelled(session_name) && metadata.server.defined) {
metadata.session_entry(session_name).foreach { entry =>
val subject = Mailer.failed_subject(entry)
val text = Mailer.failed_text(session_name, entry, isabelle_id, afp.hg_id, result)
val notified = metadata.notify(entry, subject, text)
if (!notified) println(s"Entry $entry: WARNING no maintainers specified")
}
}
}
}
print_section("COMPLETED")
Result(sitegen_res.rc)
}
Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection = Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow")))
})
val mac =
Job("mac", "builds the AFP (without some sessions) on Mac Os",
Profile.from_host.copy(threads = 8, jobs = 1),
{
val afp = AFP_Structure()
def pre_hook(options: Options): Result = {
println(s"Build for AFP id ${ afp.hg_id }")
Result.ok
}
Build_Config(
include = List(afp.thys_dir), pre_hook = pre_hook, selection =
Sessions.Selection(
all_sessions = true,
exclude_sessions = List("HOL-Proofs", "HOL-ODE-Numerics", "Linear_Programming", "HOL-Nominal-Examples", "HOL-Analysis"),
exclude_session_groups = List("slow")))
})
val slow =
Job("slow", "builds the AFP slow sessions", Profile.from_host.copy(threads = 8, jobs = 1),
{
val afp = AFP_Structure()
def pre_hook(options: Options): Result = {
println(s"Build for AFP id ${ afp.hg_id }")
Result.ok
}
Build_Config(
include = List(afp.thys_dir), pre_hook = pre_hook,
selection = Sessions.Selection(session_groups = List("slow")))
})
val testboard =
Job("testboard", "builds the AFP testboard", Profile.from_host,
{
val afp = AFP_Structure()
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
def pre_hook(options: Options): Result = {
println(s"AFP id ${ afp.hg_id }")
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
Result.ok
}
def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
val metadata = Metadata_Tools.load(afp, options)
val status = metadata.by_entry(results.sessions.toList).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
}.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, status_as_html(status))
print_section("COMPLETED")
Result.ok
}
Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow")))
})
}
class CI_Builds extends Isabelle_CI_Builds(
AFP_Build.afp,
AFP_Build.all,
AFP_Build.slow,
AFP_Build.mac,
AFP_Build.testboard)
diff --git a/tools/afp_check_metadata.scala b/tools/afp_check_metadata.scala
--- a/tools/afp_check_metadata.scala
+++ b/tools/afp_check_metadata.scala
@@ -1,202 +1,198 @@
/* Author: Fabian Huch, TU Muenchen
Tool to check metadata consistency.
*/
package afp
import isabelle.*
import afp.Metadata.{Author, DOI, Email, Homepage, TOML, Topic}
import isabelle.TOML.{parse, Format, Key, Table}
object AFP_Check_Metadata {
def diff(t1: Table, t2: Table): List[Key] =
(t1.domain diff t2.domain).toList ++ t1.table.values.flatMap {
case (k, tr1) => t2.table.get(k).toList.flatMap(diff(tr1, _))
}
def afp_check_metadata(
afp_structure: AFP_Structure,
strict: Boolean = false,
reformat: Boolean = false,
format_all: Boolean = false,
slow: Boolean = false,
verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
def warn(msg: String): Unit = if (strict) error(msg) else progress.echo_warning(msg)
progress.echo_if(verbose, "Loading metadata...")
- val orig_authors = afp_structure.load_authors
- val orig_topics = afp_structure.load_topics
- val orig_licenses = afp_structure.load_licenses
- val orig_releases = afp_structure.load_releases
- val authors = orig_authors.map(author => author.id -> author).toMap
- val topics = Utils.grouped_sorted(orig_topics.flatMap(_.all_topics), (t: Topic) => t.id)
- val licenses = orig_licenses.map(license => license.id -> license).toMap
- val releases = orig_releases.groupBy(_.entry)
+ val authors = afp_structure.load_authors
+ val topics = afp_structure.load_topics
+ val licenses = afp_structure.load_licenses
+ val releases = afp_structure.load_releases
val entries = afp_structure.entries.map(name =>
afp_structure.load_entry(name, authors, topics, licenses, releases))
/* TOML encoding/decoding */
def check_toml[A](kind: String, a: A, from: A => Table, to: Table => A): Unit =
if (to(from(a)) != a) error("Inconsistent toml encode/decode: " + kind)
progress.echo_if(verbose, "Checking toml conversions...")
check_toml("authors", authors.values.toList, TOML.from_authors, TOML.to_authors)
- check_toml("topics", orig_topics, TOML.from_topics, TOML.to_topics)
+ check_toml("topics", Metadata.Topics.root_topics(topics), TOML.from_topics, TOML.to_topics)
check_toml("licenses", licenses.values.toList, TOML.from_licenses, TOML.to_licenses)
check_toml("releases", releases.values.flatten.toList, TOML.from_releases, TOML.to_releases)
entries.foreach(entry => check_toml("entry " + entry.name, entry, TOML.from_entry, t =>
TOML.to_entry(entry.name, t, authors, topics, licenses, releases.getOrElse(entry.name, Nil))))
/* duplicate ids */
var seen_ids = Set.empty[String]
def check_id(id: String): Unit =
if (seen_ids.contains(id)) error("Duplicate id: " + id) else seen_ids += id
progress.echo_if(verbose, "Checking for duplicate ids...")
authors.values.foreach { author =>
check_id(author.id)
author.emails.map(_.id).foreach(check_id)
author.homepages.map(_.id).foreach(check_id)
}
topics.values.map(_.id).foreach(check_id)
licenses.values.map(_.id).foreach(check_id)
entries.map(_.name).foreach(check_id)
/* unread fields */
progress.echo_if(verbose, "Checking for unused fields...")
def check_unused_toml[A](file: Path, to: Table => A, from: A => Table): Unit = {
val toml = parse(File.read(file))
val recoded = from(to(toml))
val diff_keys = diff(parse(File.read(file)), recoded)
if (diff_keys.nonEmpty) warn("Unused fields: " + commas_quote(diff_keys))
}
check_unused_toml(afp_structure.authors_file, TOML.to_authors, TOML.from_authors)
check_unused_toml(afp_structure.topics_file, TOML.to_topics, TOML.from_topics)
check_unused_toml(afp_structure.licenses_file, TOML.to_licenses, TOML.from_licenses)
check_unused_toml(afp_structure.releases_file, TOML.to_releases, TOML.from_releases)
entries.foreach(entry => check_unused_toml(afp_structure.entry_file(entry.name), t =>
TOML.to_entry(entry.name, t, authors, topics, licenses, releases.getOrElse(entry.name, Nil)),
TOML.from_entry))
/* unused values */
def warn_unused(name: String, unused: Set[String]): Unit =
if (unused.nonEmpty) warn("Extra (unused) " + name + ": " + commas_quote(unused.toList))
progress.echo_if(verbose, "Checking for unused values...")
val all_affils = entries.flatMap(entry => entry.authors ++ entry.contributors ++ entry.notifies)
warn_unused("authors", authors.keySet diff all_affils.map(_.author).toSet)
def author_affil_id(author: Author.ID, affil: String): String = author + " " + affil
val affils = authors.values.flatMap(author =>
(author.emails.map(_.id) ++ author.homepages.map(_.id)).map(author_affil_id(author.id, _)))
val used_affils = all_affils.collect {
case Email(author, id, _) => author_affil_id(author, id)
case Homepage(author, id, _) => author_affil_id(author, id)
}
warn_unused("affiliations", affils.toSet diff used_affils.toSet)
val leaf_topics = topics.values.filter(_.sub_topics.isEmpty).map(_.id)
warn_unused("topics", leaf_topics.toSet diff entries.flatMap(_.topics).map(_.id).toSet)
warn_unused("licenses", licenses.keySet diff entries.map(_.license.id).toSet)
/* formatting of commonly patched files */
if (reformat) {
- afp_structure.save_authors(orig_authors)
+ afp_structure.save_authors(authors.values.toList)
if (format_all) {
- afp_structure.save_topics(orig_topics)
- afp_structure.save_licenses(orig_licenses)
- afp_structure.save_releases(orig_releases)
+ afp_structure.save_topics(Metadata.Topics.root_topics(topics))
+ afp_structure.save_licenses(licenses.values.toList)
+ afp_structure.save_releases(releases.values.toList.flatten)
entries.foreach(afp_structure.save_entry)
}
}
else {
def check_toml_format(toml: Table, file: Path): Unit = {
val present = File.read(file)
val formatted = Format(toml)
if (present != formatted) progress.echo_warning("Badly formatted toml: " + file)
}
progress.echo_if(verbose, "Checking formatting...")
- check_toml_format(TOML.from_authors(orig_authors), afp_structure.authors_file)
+ check_toml_format(TOML.from_authors(authors.values.toList), afp_structure.authors_file)
if (format_all) {
check_toml_format(TOML.from_topics(topics.values.toList), afp_structure.topics_file)
check_toml_format(TOML.from_licenses(licenses.values.toList), afp_structure.licenses_file)
check_toml_format(TOML.from_releases(releases.values.toList.flatten),
afp_structure.releases_file)
entries.foreach(entry =>
check_toml_format(TOML.from_entry(entry), afp_structure.entry_file(entry.name)))
}
}
/* extra */
if (slow) {
progress.echo_if(verbose, "Checking DOIs...")
entries.flatMap(entry => entry.related).collect { case d: DOI => d.formatted() }
}
progress.echo_if(verbose, "Checked " + authors.size + " authors with " + affils.size +
" affiliations, " + topics.size + " topics, " + releases.values.flatten.size + " releases, " +
licenses.size + " licenses, and " + entries.size + " entries.")
}
val isabelle_tool = Isabelle_Tool("afp_check_metadata", "Checks the AFP metadata files",
Scala_Project.here,
{ args =>
var slow = false
var reformat = false
var format_all = false
var strict = false
var verbose = false
val getopts = Getopts("""
Usage: isabelle afp_check_metadata [OPTIONS]
Options are:
-a check formatting of all metadata
-s activate slow checks
-v verbose
-R reformat metadata files
-S strict mode (fail on warnings)
Check AFP metadata files for consistency.
""",
"a" -> (_ => format_all = true),
"s" -> (_ => slow = true),
"v" -> (_ => verbose = true),
"R" -> (_ => reformat = true),
"S" -> (_ => strict = true))
getopts(args)
val progress = new Console_Progress()
val afp_structure = AFP_Structure()
afp_check_metadata(afp_structure, strict = strict, reformat = reformat, format_all = format_all,
slow = slow, verbose = verbose, progress = progress)
})
}
diff --git a/tools/afp_release.scala b/tools/afp_release.scala
--- a/tools/afp_release.scala
+++ b/tools/afp_release.scala
@@ -1,108 +1,108 @@
/* Author: Fabian Huch, TU Muenchen
Tooling to manage AFP releases.
*/
package afp
import isabelle.*
import afp.Metadata.{Entry, Isabelle, Release}
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_structure = AFP_Structure(base_dir)
val isabelle_releases =
split_lines(File.read(afp_structure.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) => Release(entry, date, isabelle)
case None => error("No Isabelle version found for " + date_str)
}
}
afp_structure.save_releases(releases)
}
}
def afp_release(date: LocalDate, isabelle: Isabelle.Version, base_dir: Path): Unit = {
def add_release(entry: Entry): Entry =
entry.copy(releases = entry.releases :+ Release(entry.name, date, isabelle))
val afp_structure = AFP_Structure(base_dir)
- val releases = afp_structure.load().map(add_release).flatMap(_.releases)
+ val releases = afp_structure.load().values.toList.map(add_release).flatMap(_.releases)
afp_structure.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)
case _ => error("Invalid remote: " + quote(releases))
}
}
else {
if (isabelle.isEmpty) getopts.usage()
afp_release(date, isabelle, base_dir)
}
})
}
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,490 +1,485 @@
/* 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_structure: 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_structure.load_topics
- val topics_by_id =
- Utils.grouped_sorted(topics.flatMap(_.all_topics), (t: Metadata.Topic) => t.id)
+ val root_topics = Metadata.Topics.root_topics(topics)
- layout.write_data(Path.basic("topics.json"), JSON.from_topics(topics))
+ layout.write_data(Path.basic("topics.json"), JSON.from_topics(root_topics))
/* add licenses */
progress.echo("Preparing licenses...")
- val licenses_by_id = Utils.grouped_sorted(afp_structure.load_licenses,
- (l: Metadata.License) => l.id)
+ val licenses = afp_structure.load_licenses
/* add releases */
progress.echo("Preparing releases...")
- val releases_by_entry = afp_structure.load_releases.groupBy(_.entry)
+ val releases = afp_structure.load_releases
/* prepare authors and entries */
progress.echo("Preparing authors...")
- val full_authors = afp_structure.load_authors
- val authors_by_id = Utils.grouped_sorted(full_authors, (a: Metadata.Author) => a.id)
+ val authors = afp_structure.load_authors
var seen_affiliations: List[Affiliation] = Nil
val entries =
afp_structure.entries.flatMap { name =>
- val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, licenses_by_id,
- releases_by_entry)
-
+ val entry = afp_structure.load_entry(name, authors, topics, licenses, releases)
seen_affiliations = seen_affiliations :++ entry.authors ++ entry.contributors
Some(entry)
}
- val authors =
+ 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_by_id(id).copy(emails = seen_emails, homepages = seen_homepages)
+ authors(id).copy(emails = seen_emails, homepages = seen_homepages)
}
- layout.write_data(Path.basic("authors.json"), JSON.from_authors(authors.toList))
+ 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_structure.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_structure.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).groups.contains("AFP")
dep <- session_entry.get(dep_session)
if dep != entry
} yield dep.name
val sessions =
afp_structure.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.groups.contains("AFP")
} write_session_json(session_name, JSON.Object("rss" -> false))
/* add statistics */
progress.echo("Preparing statistics...")
val statistics_json =
afp_stats(sessions_deps, afp_structure, 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 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_structure = AFP_Structure(base_dir)
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_structure = afp_structure,
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,129 +1,134 @@
/* Author: Fabian Huch, TU Muenchen
AFP Metadata file structure with save and load operations.
*/
package afp
import isabelle.*
class AFP_Structure private(val base_dir: Path) {
/* files */
val metadata_dir = base_dir + Path.basic("metadata")
val thys_dir = 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: 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_authors: Metadata.Authors =
+ Metadata.Authors(load(authors_file, Metadata.TOML.to_authors))
- def load_topics: List[Metadata.Topic] = load(topics_file, Metadata.TOML.to_topics)
+ def load_releases: Metadata.Releases =
+ Metadata.Releases(load(releases_file, Metadata.TOML.to_releases))
- 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]]
+ 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(): List[Metadata.Entry] = {
- val authors = load_authors.map(author => author.id -> author).toMap
- val topics = Utils.grouped_sorted(load_topics.flatMap(_.all_topics), (t: Metadata.Topic) => t.id)
- val licenses = load_licenses.map(license => license.id -> license).toMap
- val releases = load_releases.groupBy(_.entry)
- entries.map(name => load_entry(name, authors, topics, licenses, releases))
+ def load(): Metadata.Entries = {
+ val authors = load_authors
+ val topics = load_topics
+ val licenses = load_licenses
+ val releases = load_releases
+ 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(topics: List[Metadata.Topic]): Unit =
- save(topics_file, Metadata.TOML.from_topics(topics))
+ 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 + Path.basic("ROOTS"))
val session_set = session_entries.toSet
val metadata_set = entries_unchecked.toSet
if (session_set != metadata_set) {
val inter = session_set.intersect(metadata_set)
val session_without_metadata =
if (session_set.subsetOf(inter)) ""
else "No metadata for session in ROOTS: " + commas_quote(session_set -- inter)
val metadata_without_session =
if (metadata_set.subsetOf(inter)) ""
else "Metadata entries missing in ROOTS: " + commas_quote(metadata_set -- inter)
error("Metadata does not match sessions:\n" + session_without_metadata + metadata_without_session)
} else session_entries
}
def sessions_structure: Sessions.Structure =
Sessions.load_structure(options = Options.init(), select_dirs = List(thys_dir))
def entry_sessions(name: Metadata.Entry.Name): List[Sessions.Session_Entry] =
Sessions.parse_root(thys_dir + Path.make(List(name, "ROOT"))).collect { case e: Sessions.Session_Entry => e }
def hg_id: String = Mercurial.repository(base_dir).id()
}
object AFP_Structure {
def apply(base_dir: Path = AFP.BASE): AFP_Structure = new AFP_Structure(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,1625 +1,1613 @@
/* Author: Fabian Huch, TU Muenchen
AFP submission system backend.
*/
package afp
import isabelle.*
import isabelle.HTML.*
import afp.Web_App.{ACTION, API, FILE, Params}
import afp.Web_App.Params.{List_Key, Nest_Key, empty}
import afp.Web_App.More_HTML.*
-import afp.Metadata.{Affiliation, Author, DOI, Email, Entry, Formatted, Homepage, License, Orcid, Reference, Release, Topic, Unaffiliated}
+import afp.Metadata.{Affiliation, Author, Authors, DOI, Email, Entry, Formatted, Homepage, License, Licenses, Orcid, Reference, Release, Releases, Topic, Topics, Unaffiliated}
import java.text.Normalizer
import java.time.LocalDate
-import scala.collection.immutable.StringView
+import scala.collection.immutable.{ListMap, StringView}
import scala.util.matching.Regex
object AFP_Submit {
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 */
object Model {
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
}
}
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)
}
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 update_entry(num: Int, entry: Create_Entry): Create =
copy(entries = Val.ok(entries.v.updated(num, entry)))
- def updated_authors(old_authors: Map[Author.ID, Author]): Map[Author.ID, Author] =
+ def updated_authors(old_authors: Authors): Authors =
(old_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 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)
- def create(authors: Map[Author.ID, Author]): (Map[Author.ID, Author], List[Entry]) =
+ def create(authors: Authors): (Authors, List[Entry]) =
(updated_authors(authors), entries.v.map(entry =>
Entry(
name = entry.name.v,
title = entry.title.v,
authors = entry.affils.v,
date = LocalDate.now(),
topics = entry.topics.v,
`abstract` = entry.`abstract`.v.trim,
notifies = entry.notifies.v,
license = entry.license,
note = "",
related = entry.related)))
}
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)
- case class Metadata(authors: Map[Author.ID, Author], entries: List[Entry]) {
- def new_authors(old_authors: Map[Author.ID, Author]): Set[Author] =
+ case class Metadata(authors: Authors, entries: List[Entry]) {
+ def new_authors(old_authors: Authors): Set[Author] =
entries.flatMap(_.authors).map(_.author).filterNot(old_authors.contains).toSet.map(authors)
- def new_affils(old_authors: Map[Author.ID, Author]): Set[Affiliation] =
+ def new_affils(old_authors: Authors): Set[Affiliation] =
entries.flatMap(entry => entry.authors ++ entry.notifies).toSet.filter {
case _: Unaffiliated => false
case e: Email => !old_authors.get(e.author).exists(_.emails.contains(e))
case h: Homepage => !old_authors.get(h.author).exists(_.homepages.contains(h))
}
}
sealed trait T
case object Invalid extends T
case class Upload(meta: Metadata, message: String, error: String = "") extends T
case class Created(id: String) extends T
case class Submission(
id: Handler.ID,
meta: Metadata,
message: String,
build: Build.Value,
status: Option[Status.Value],
log: String) extends T
case class Submission_List(submissions: List[Overview]) extends T
}
/* Physical submission handling */
trait Handler {
def create(
date: Date,
meta: Model.Metadata,
message: String,
archive: Bytes,
ext: String
): Handler.ID
def list(): Model.Submission_List
- def get(id: Handler.ID,
- topics: Map[Topic.ID, Topic],
- licenses: Map[License.ID, License]
- ): Option[Model.Submission]
+ def get(id: Handler.ID, topics: Topics, licenses: Licenses): 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 {
import Model._
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_structure: AFP_Structure) extends Handler {
- val authors = afp_structure.load_authors.map(author => author.id -> author).toMap
- val topics = afp_structure.load_topics.flatMap(_.all_topics)
- val all_topics = topics.map(topic => topic.id -> topic).toMap
- val licenses = afp_structure.load_licenses.map(license => license.id -> license).toMap
- val releases = afp_structure.load_releases.groupBy(_.entry)
- val dates = afp_structure.load().map(entry => entry.name -> entry.date).toMap
+ val authors = afp_structure.load_authors
+ val topics = afp_structure.load_topics
+ val licenses = afp_structure.load_licenses
+ val releases = afp_structure.load_releases
+ val dates = afp_structure.load().view.mapValues(_.date).toMap
def create(
date: Date,
meta: Metadata,
message: String,
archive: Bytes,
ext: String
): ID = {
val entry =
meta.entries match {
case e :: Nil => e
case _ => isabelle.error("Must be a single entry")
}
- val old = afp_structure.load_entry(entry.name, authors, all_topics, licenses, releases)
+ val old = afp_structure.load_entry(entry.name, authors, topics, licenses, releases)
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_structure.save_entry(updated)
// TODO what happens to the authors
entry.name
}
def list(): Submission_List =
Submission_List(afp_structure.entries.sortBy(dates.get).reverse.map { entry =>
Overview(entry, dates(entry), entry, Status.Added)
})
- def get(
- id: ID, topics: Map[ID, Topic], licenses: Map[ID, License]
- ): Option[Submission] =
+ def get(id: ID, topics: Topics, licenses: Licenses): Option[Submission] =
if (!afp_structure.entries.contains(id)) None
else {
- val entry = afp_structure.load_entry(id, authors, all_topics, licenses, releases)
+ val entry = afp_structure.load_entry(id, authors, topics, licenses, releases)
val meta = Metadata(authors, List(entry))
Some(Submission(id, meta, "", Model.Build.Success, Some(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_structure: 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): Build.Value = {
val build = down(id) + Path.basic("result")
if (!build.file.exists) Build.Pending
else File.read(build).trim match {
case "" => Build.Running
case "NOT_FINISHED" => Build.Running
case "FAILED" => if (is_signal(id, "kill")) Build.Aborted else Build.Failed
case "SUCCESS" => 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[Status.Value] = {
val status = status_file(id)
if (!status.file.exists()) None
else File.read(status).trim match {
case "SUBMITTED" => Some(Status.Submitted)
case "PROCESSING" => Some(Status.Review)
case "REJECTED" => Some(Status.Rejected)
case "ADDED" => Some(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 create(date: Date, meta: Metadata, message: String, archive: Bytes, ext: String): ID = {
val id = ID(date)
val dir = up(id)
dir.file.mkdirs()
val structure = AFP_Structure(dir)
structure.save_authors(meta.authors.values.toList.sortBy(_.id))
meta.entries.foreach(structure.save_entry)
val archive_file = dir + Path.basic(archive_name + ext)
Bytes.write(archive_file, archive)
val metadata_rel =
File.relative_path(afp_structure.base_dir, afp_structure.metadata_dir).getOrElse(
afp_structure.metadata_dir)
val metadata_patch =
make_partial_patch(afp_structure.base_dir, metadata_rel, structure.metadata_dir)
File.write(patch_file(id), metadata_patch)
val info =
JSON.Format(JSON.Object(
"comment" -> message,
"entries" -> meta.entries.map(_.name),
"notify" -> meta.entries.flatMap(_.notifies).map(_.address).distinct))
File.write(info_file(id), info)
signal(id, "done")
id
}
def list(): Submission_List =
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(Overview(id, day, AFP_Structure(up(id)).entries_unchecked.head, _))
})
- def get(
- id: ID,
- topics: Map[Topic.ID, Topic],
- licenses: Map[License.ID, License]
- ): Option[Submission] =
+ def get(id: ID, topics: Topics, licenses: Licenses): Option[Submission] =
ID.check(id).filter(up(_).file.exists).map { id =>
val structure = AFP_Structure(up(id))
- val authors = structure.load_authors.map(author => author.id -> author).toMap
+ val authors = structure.load_authors
val entries = structure.entries_unchecked.map(
- structure.load_entry(_, authors, topics, licenses, Map.empty))
+ structure.load_entry(_, authors, topics, licenses, Releases.empty))
val log_file = down(id) + Path.basic("isabelle.log")
val log = if (log_file.file.exists) File.read(log_file) else ""
JSON.parse(File.read(info_file(id))) match {
case JSON.Object(m) if m.contains("comment") =>
val meta = Metadata(authors, entries)
Submission(id, meta, m("comment").toString, read_build(id), read_status(id), log)
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: Status.Value): Unit =
check(id).foreach { id =>
val content =
status match {
case Status.Submitted => "SUBMITTED"
case Status.Review => "PROCESSING"
case Status.Added => "ADDED"
case 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(_))
}
}
}
/* server */
object Mode extends Enumeration {
val EDIT, SUBMISSION = Value
}
class Server(
api: API,
afp_structure: AFP_Structure,
mode: Mode.Value,
handler: Handler,
devel: Boolean,
verbose: Boolean,
progress: Progress,
port: Int = 0
) extends Web_App.Server[Model.T](api, port, verbose, progress) {
val repo = Mercurial.the_repository(afp_structure.base_dir)
- var authors: Map[Author.ID, Metadata.Author] = Map.empty
- var topics: List[Topic] = Nil
- var all_topics: Map[Topic.ID, Topic] = Map.empty
- var licenses: Map[License.ID, License] = Map.empty
- var releases: Map[Entry.Name, List[Release]] = Map.empty
+ var authors: Authors = Authors.empty
+ var topics: Topics = Topics.empty
+ var licenses: Licenses = Licenses.empty
+ var releases: Releases = Releases.empty
var entries: Set[Entry.Name] = Set.empty
private def load(): Unit = synchronized {
- authors = afp_structure.load_authors.map(author => author.id -> author).toMap
- topics = afp_structure.load_topics.flatMap(_.all_topics)
- all_topics = topics.map(topic => topic.id -> topic).toMap
- licenses = afp_structure.load_licenses.map(license => license.id -> license).toMap
- releases = afp_structure.load_releases.groupBy(_.entry)
+ authors = afp_structure.load_authors
+ topics = afp_structure.load_topics
+ licenses = afp_structure.load_licenses
+ releases = afp_structure.load_releases
entries = afp_structure.entries.toSet
}
load()
/* endpoints */
val SUBMIT = Path.explode("submit")
val SUBMISSION = Path.explode("submission")
val SUBMISSIONS = Path.explode("submissions")
val API_SUBMISSION = Path.explode("api/submission")
val API_SUBMISSION_UPLOAD = Path.explode("api/submission/upload")
val API_SUBMISSION_CREATE = Path.explode("api/submission/create")
val API_SUBMISSION_STATUS = Path.explode("api/submission/status")
val API_RESUBMIT = Path.explode("api/resubmit")
val API_BUILD_ABORT = Path.explode("api/build/abort")
val API_SUBMIT = Path.explode("api/submit")
val API_SUBMISSION_AUTHORS_ADD = Path.explode("api/submission/authors/add")
val API_SUBMISSION_AUTHORS_REMOVE = Path.explode("api/submission/authors/remove")
val API_SUBMISSION_AFFILIATIONS_ADD = Path.explode("api/submission/affiliations/add")
val API_SUBMISSION_AFFILIATIONS_REMOVE = Path.explode("api/submission/affiliations/remove")
val API_SUBMISSION_ENTRIES_ADD = Path.explode("api/submission/entries/add")
val API_SUBMISSION_ENTRIES_REMOVE = Path.explode("api/submission/entries/remove")
val API_SUBMISSION_ENTRY_TOPICS_ADD = Path.explode("api/submission/entry/topics/add")
val API_SUBMISSION_ENTRY_TOPICS_REMOVE = Path.explode("api/submission/entry/topics/remove")
val API_SUBMISSION_ENTRY_AUTHORS_ADD = Path.explode("api/submission/entry/authors/add")
val API_SUBMISSION_ENTRY_AUTHORS_REMOVE = Path.explode("api/submission/entry/authors/remove")
val API_SUBMISSION_ENTRY_NOTIFIES_ADD = Path.explode("api/submission/entry/notifies/add")
val API_SUBMISSION_ENTRY_NOTIFIES_REMOVE = Path.explode("api/submission/entry/notifies/remove")
val API_SUBMISSION_ENTRY_RELATED_ADD = Path.explode("api/submission/entry/related/add")
val API_SUBMISSION_ENTRY_RELATED_REMOVE = Path.explode("api/submission/entry/related/remove")
val API_SUBMISSION_DOWNLOAD = Path.explode("api/download/patch")
val API_SUBMISSION_DOWNLOAD_ZIP = Path.explode("api/download/archive.zip")
val API_SUBMISSION_DOWNLOAD_TGZ = Path.explode("api/download/archive.tar.gz")
val API_CSS = Path.explode("api/main.css")
/* fields */
val ABSTRACT = "abstract"
val ADDRESS = "address"
val AFFILIATION = "affiliation"
val ARCHIVE = "archive"
val AUTHOR = "author"
val DATE = "date"
val ENTRY = "entry"
val ID = "id"
val INPUT = "input"
val KIND = "kind"
val LICENSE = "license"
val MESSAGE = "message"
val NAME = "name"
val NOTIFY = "notify"
val ORCID = "orcid"
val RELATED = "related"
val STATUS = "status"
val TITLE = "title"
val TOPIC = "topic"
/* 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 indexed[A, B](l: List[A], key: Params.Key, field: String, f: (A, Params.Key) => B) =
l.zipWithIndex map {
case (a, i) => f(a, List_Key(key, field, i))
}
def fold[A](it: List[Params.Data], a: A)(f: (Params.Data, A) => Option[A]): Option[A] =
it.foldLeft(Option(a)) {
case (None, _) => None
case (Some(a), param) => f(param, 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(api.app_url(path, params), body) + ("target" -> "_parent")
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: String, validated: Val[_]): XML.Body =
validated.err.map(error =>
break ::: List(css("color: red")(label(for_elem, error)))).getOrElse(Nil)
/* view */
def render_create(model: Model.Create): XML.Body = {
val updated_authors = model.updated_authors(authors)
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(topic: Topic, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, ID), topic.id) ::
text(topic.id) :::
action_button(api.api_url(API_SUBMISSION_ENTRY_TOPICS_REMOVE), "x", key) :: Nil)
def render_affil(affil: Affiliation, key: Params.Key): XML.Elem = {
val author = updated_authors(affil.author)
val affils = author.emails ::: author.homepages ::: Unaffiliated(author.id) :: Nil
par(
hidden(Nest_Key(key, ID), affil.author) ::
text(author_string(updated_authors(affil.author))) :::
selection(Nest_Key(key, AFFILIATION),
Some(affil_id(affil)),
affils.map(affil => option(affil_id(affil), affil_string(affil)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_AUTHORS_REMOVE), "x", key) :: Nil)
}
def render_notify(email: Email, key: Params.Key): XML.Elem = {
val author = updated_authors(email.author)
par(
hidden(Nest_Key(key, ID), email.author) ::
text(author_string(updated_authors(email.author))) :::
selection(
Nest_Key(key, AFFILIATION),
Some(affil_id(email)),
author.emails.map(affil => option(affil_id(affil), affil_string(affil)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_NOTIFIES_REMOVE), "x", key) :: Nil)
}
def render_related(related: Reference, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, KIND), Model.Related.get(related).toString) ::
hidden(Nest_Key(key, INPUT), related_string(related)) ::
text(related_string(related)) :::
action_button(api.api_url(API_SUBMISSION_ENTRY_RELATED_REMOVE), "x", key) :: Nil)
def render_entry(entry: Model.Create_Entry, key: Params.Key): XML.Elem =
fieldset(legend("Entry") ::
par(
fieldlabel(Nest_Key(key, TITLE), "Title of article") ::
textfield(Nest_Key(key, TITLE), "Example Submission", entry.title.v) ::
render_error(Nest_Key(key, TITLE), entry.title)) ::
par(
fieldlabel(Nest_Key(key, NAME), "Short name") ::
textfield(Nest_Key(key, NAME), "Example_Submission", entry.name.v) ::
explanation(Nest_Key(key, NAME),
"Name of the folder where your ROOT and theory files reside.") ::
render_error(Nest_Key(key, NAME), entry.name)) ::
fieldset(legend("Topics") ::
indexed(entry.topics.v, key, TOPIC, render_topic) :::
selection(Nest_Key(key, TOPIC),
entry.topic_input.map(_.id),
- topics.map(topic => option(topic.id, topic.id))) ::
+ topics.values.toList.map(topic => option(topic.id, topic.id))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_TOPICS_ADD), "add", key) ::
render_error("", entry.topics)) ::
par(List(
fieldlabel(Nest_Key(key, LICENSE), "License"),
radio(Nest_Key(key, LICENSE),
entry.license.id,
licenses.values.toList.map(license => license.id -> license.name)),
explanation(Nest_Key(key, LICENSE),
"Note: For LGPL submissions, please include the header \"License: LGPL\" in each file"))) ::
par(
fieldlabel(Nest_Key(key, ABSTRACT), "Abstract") ::
placeholder("HTML and MathJax, no LaTeX")(
textarea(Nest_Key(key, ABSTRACT), entry.`abstract`.v) +
("rows" -> "8") +
("cols" -> "70")) ::
explanation(Nest_Key(key, ABSTRACT),
"Note: You can use HTML or MathJax (not LaTeX!) to format your abstract.") ::
render_error(Nest_Key(key, ABSTRACT), entry.`abstract`)) ::
fieldset(legend("Authors") ::
indexed(entry.affils.v, key, AUTHOR, render_affil) :::
selection(Nest_Key(key, AUTHOR),
entry.author_input.map(_.id),
authors_list.map(author => option(author.id, author_string(author)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_AUTHORS_ADD), "add", key) ::
explanation(Nest_Key(key, AUTHOR),
"Add an author from the list. Register new authors first below.") ::
render_error(Nest_Key(key, AUTHOR), entry.affils)) ::
fieldset(legend("Contact") ::
indexed(entry.notifies.v, key, NOTIFY, render_notify) :::
selection(Nest_Key(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(api.api_url(API_SUBMISSION_ENTRY_NOTIFIES_ADD), "add", key) ::
explanation(Nest_Key(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("", entry.notifies)) ::
fieldset(legend("Related Publications") ::
indexed(entry.related, key, RELATED, render_related) :::
selection(Nest_Key(Nest_Key(key, RELATED), KIND),
entry.related_kind.map(_.toString),
Model.Related.values.toList.map(v => option(v.toString, v.toString))) ::
textfield(Nest_Key(Nest_Key(key, RELATED), INPUT),
"10.1109/5.771073", entry.related_input.v) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_RELATED_ADD), "add", key) ::
explanation(Nest_Key(Nest_Key(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(Nest_Key(Nest_Key(key, RELATED), INPUT), entry.related_input)) ::
render_if(mode == Mode.SUBMISSION,
action_button(api.api_url(API_SUBMISSION_ENTRIES_REMOVE), "remove entry", key)))
def render_new_author(author: Author, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, ID), author.id) ::
hidden(Nest_Key(key, NAME), author.name) ::
hidden(Nest_Key(key, ORCID), author.orcid.map(_.identifier).getOrElse("")) ::
text(author_string(author)) :::
render_if(!model.used_authors.contains(author.id),
action_button(api.api_url(API_SUBMISSION_AUTHORS_REMOVE), "x", key)))
def render_new_affil(affil: Affiliation, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, AUTHOR), affil.author) ::
hidden(Nest_Key(key, ID), affil_id(affil)) ::
hidden(Nest_Key(key, AFFILIATION), affil_address(affil)) ::
text(author_string(updated_authors(affil.author)) + ": " + affil_string(affil)) :::
render_if(!model.used_affils.contains(affil),
action_button(api.api_url(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(api.api_url(API_SUBMISSION),
indexed(model.entries.v, Params.empty, ENTRY, render_entry) :::
render_error("", model.entries) :::
render_if(mode == Mode.SUBMISSION,
par(List(
explanation("",
"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(api.api_url(API_SUBMISSION_ENTRIES_ADD), "additional entry")))) :::
break :::
fieldset(legend("New Authors") ::
explanation("", "If you are new to the AFP, add yourself here.") ::
indexed(model.new_authors.v, Params.empty, AUTHOR, render_new_author) :::
fieldlabel(Nest_Key(AUTHOR, NAME), "Name") ::
textfield(Nest_Key(AUTHOR, NAME), "Gerwin Klein", model.new_author_input) ::
fieldlabel(Nest_Key(AUTHOR, ORCID), "ORCID id (optional)") ::
textfield(Nest_Key(AUTHOR, ORCID), "0000-0002-1825-0097", model.new_author_orcid) ::
api_button(api.api_url(API_SUBMISSION_AUTHORS_ADD), "add") ::
render_error("", model.new_authors)) ::
fieldset(legend("New email or homepage") ::
explanation("",
"Add new email or homepages here. " +
"If you would like to update an existing, " +
"submit with the old one and write to the editors.") ::
indexed(model.new_affils.v, Params.empty, AFFILIATION, 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(Nest_Key(AFFILIATION, ADDRESS), "Email or Homepage") ::
textfield(Nest_Key(AFFILIATION, ADDRESS), "https://proofcraft.org",
model.new_affils_input) ::
api_button(api.api_url(API_SUBMISSION_AFFILIATIONS_ADD), "add") ::
render_error("", model.new_affils)) ::
break :::
fieldset(List(legend(upload),
api_button(api.api_url(API_SUBMISSION_UPLOAD), preview))) :: Nil))
}
def render_metadata(meta: Model.Metadata): XML.Body = {
def render_topic(topic: Topic, key: Params.Key): XML.Elem =
item(hidden(Nest_Key(key, ID), topic.id) :: text(topic.id))
def render_affil(affil: Affiliation, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, ID), affil.author) ::
hidden(Nest_Key(key, AFFILIATION), affil_id(affil)) ::
text(author_string(meta.authors(affil.author)) + ", " + affil_string(affil)))
def render_related(related: Reference, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, KIND), Model.Related.get(related).toString) ::
hidden(Nest_Key(key, INPUT), related_string(related)) ::
input_raw(related_string(related)) :: Nil)
def render_entry(entry: Entry, key: Params.Key): XML.Elem =
fieldset(List(
legend("Entry"),
par(
fieldlabel(Nest_Key(key, TITLE), "Title") ::
hidden(Nest_Key(key, TITLE), entry.title) ::
text(entry.title)),
par(
fieldlabel(Nest_Key(key, NAME), "Short Name") ::
hidden(Nest_Key(key, NAME), entry.name) ::
text(entry.name)),
par(
fieldlabel(Nest_Key(key, DATE), "Date") ::
hidden(Nest_Key(key, DATE), entry.date.toString) ::
text(entry.date.toString)),
par(List(
fieldlabel("", "Topics"),
list(indexed(entry.topics, key, TOPIC, render_topic)))),
par(
fieldlabel(Nest_Key(key, LICENSE), "License") ::
hidden(Nest_Key(key, LICENSE), entry.license.id) ::
text(entry.license.name)),
par(List(
fieldlabel(Nest_Key(key, ABSTRACT), "Abstract"),
hidden(Nest_Key(key, ABSTRACT), entry.`abstract`),
class_("mathjax_process")(span(List(input_raw(entry.`abstract`)))))),
par(List(
fieldlabel("", "Authors"),
list(indexed(entry.authors, key, AUTHOR, render_affil)))),
par(List(
fieldlabel("", "Contact"),
list(indexed(entry.notifies, key, NOTIFY, render_affil)))),
par(List(
fieldlabel("", "Related Publications"),
list(indexed(entry.related, key, RELATED, render_related))))))
def render_new_author(author: Author, key: Params.Key): XML.Elem =
par(List(
hidden(Nest_Key(key, ID), author.id),
hidden(Nest_Key(key, NAME), author.name),
hidden(Nest_Key(key, ORCID), author.orcid.map(_.identifier).getOrElse(""))))
def render_new_affil(affil: Affiliation, key: Params.Key): XML.Elem =
par(List(
hidden(Nest_Key(key, AUTHOR), affil.author),
hidden(Nest_Key(key, ID), affil_id(affil)),
hidden(Nest_Key(key, AFFILIATION), affil_address(affil))))
indexed(meta.entries, Params.empty, ENTRY, render_entry) :::
indexed(meta.new_authors(authors).toList, Params.empty, AUTHOR, render_new_author) :::
indexed(meta.new_affils(authors).toList, Params.empty, AFFILIATION, render_new_affil)
}
def render_submission(submission: Model.Submission): 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."
val archive_url =
if (handler.get_archive(submission.id).exists(_.get_ext == "zip"))
API_SUBMISSION_DOWNLOAD_ZIP
else API_SUBMISSION_DOWNLOAD_TGZ
val resubmit = mode match {
case Mode.EDIT => "Update"
case Mode.SUBMISSION => "Resubmit"
}
List(submit_form(api.api_url(SUBMISSION, List(ID -> submission.id)),
render_if(mode == Mode.SUBMISSION,
download_link(api.api_url(archive_url, List(ID -> submission.id)), text("archive")) ::
download_link(api.api_url(API_SUBMISSION_DOWNLOAD, List(ID -> 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) :::
section("Status") ::
span(text(status_text(submission.status))) ::
render_if(submission.build != Model.Build.Running,
action_button(api.api_url(API_RESUBMIT), resubmit, submission.id)) :::
render_if(submission.build == Model.Build.Running,
action_button(api.api_url(API_BUILD_ABORT), "Abort build", submission.id)) :::
render_if(submission.build == Model.Build.Success && submission.status.isEmpty,
action_button(api.api_url(API_SUBMIT), "Send submission to AFP editors", submission.id)) :::
render_if(mode == Mode.SUBMISSION,
fieldset(legend("Build") ::
bold(text(submission.build.toString)) ::
par(text("Isabelle log:") ::: source(submission.log) :: Nil) ::
Nil))))
}
def render_upload(upload: Model.Upload): XML.Body = {
val submit = mode match {
case Mode.EDIT => "save"
case Mode.SUBMISSION => "submit"
}
List(submit_form(api.api_url(API_SUBMISSION), List(
fieldset(legend("Overview") :: render_metadata(upload.meta)),
fieldset(legend("Submit") ::
api_button(api.api_url(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(api.api_url(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(overview: Model.Overview, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, ID), overview.id) ::
hidden(Nest_Key(key, DATE), overview.date.toString) ::
hidden(Nest_Key(key, NAME), overview.name) ::
span(text(overview.date.toString)) ::
span(List(frontend_link(SUBMISSION, List(ID -> overview.id),
text(overview.name)))) ::
render_if(mode == Mode.SUBMISSION,
class_("right")(span(List(
selection(Nest_Key(key, STATUS), Some(overview.status.toString),
Model.Status.values.toList.map(v => option(v.toString, v.toString))),
action_button(api.api_url(API_SUBMISSION_STATUS), "update", key))))))
def list1(ls: List[XML.Elem]): XML.Elem = if (ls.isEmpty) par(Nil) else list(ls)
val ls = indexed(submission_list.submissions, Params.empty, ENTRY, (o, k) => (o, k))
val finished =
ls.filter(t => Set(Model.Status.Added, Model.Status.Rejected).contains(t._1.status))
List(submit_form(api.api_url(API_SUBMISSION_STATUS),
render_if(mode == Mode.SUBMISSION,
text("Open") :::
list1(ls.filter(_._1.status == Model.Status.Submitted).map(render_overview)) ::
text("In Progress") :::
list1(ls.filter(_._1.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(SUBMISSION, List(ID -> created.id),
text(api.app_url(SUBMISSION, List(ID -> created.id)))) ::
break :::
render_if(mode == Mode.SUBMISSION, span(text("(keep that url!).")))))
}
def render_invalid: XML.Body = text("Invalid request")
def render(model: Model.T): XML.Body =
model match {
case create: Model.Create => render_create(create)
case upload: Model.Upload => render_upload(upload)
case submission: Model.Submission => render_submission(submission)
case submissions: Model.Submission_List => render_submission_list(submissions)
case created: Model.Created => render_created(created)
case Model.Invalid => render_invalid
}
/* validation */
def validate_topic(id: String, selected: List[Topic]): Val_Opt[Topic] =
if (id.isEmpty) Val_Opt.user_err("Select topic first")
else {
- topics.find(_.id == id) match {
+ 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: Map[Author.ID, Author]
+ 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)
}
}
/* param parsing */
def parse_create(params: Params.Data): Option[Model.Create] = {
def parse_topic(topic: Params.Data, topics: List[Topic]): Option[Topic] =
validate_topic(topic.get(ID).value, topics).opt
- def parse_email(email: Params.Data, authors: Map[Author.ID, Author]): Option[Email] =
+ def parse_email(email: Params.Data, authors: Authors): Option[Email] =
authors.get(email.get(ID).value).flatMap(
_.emails.find(_.id == email.get(AFFILIATION).value))
- def parse_affil(affil: Params.Data, authors: Map[Author.ID, Author]): Option[Affiliation] =
+ def parse_affil(affil: Params.Data, authors: Authors): Option[Affiliation] =
authors.get(affil.get(ID).value).flatMap { author =>
val id = affil.get(AFFILIATION).value
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(related: Params.Data, references: List[Reference]): Option[Reference] =
Model.Related.from_string(related.get(KIND).value).flatMap(
validate_related(_, related.get(INPUT).value, references).opt)
- def parse_new_author(author: Params.Data, authors: Map[Author.ID, Author]): Option[Author] =
+ def parse_new_author(author: Params.Data, authors: Authors): Option[Author] =
validate_new_author(
author.get(ID).value, author.get(NAME).value, author.get(ORCID).value, authors).opt
- def parse_new_affil(affil: Params.Data, authors: Map[Author.ID, Author]): Option[Affiliation] =
+ def parse_new_affil(affil: Params.Data, authors: Authors): Option[Affiliation] =
authors.get(affil.get(AUTHOR).value).flatMap(author =>
validate_new_affil(affil.get(ID).value, affil.get(AFFILIATION).value, author).opt)
- def parse_entry(entry: Params.Data, authors: Map[Author.ID, Author]): Option[Model.Create_Entry] =
+ def parse_entry(entry: Params.Data, authors: Authors): Option[Model.Create_Entry] =
for {
topics <-
fold(entry.list(TOPIC), List.empty[Topic]) {
case (topic, topics) => parse_topic(topic, topics).map(topics :+ _)
}
affils <-
fold(entry.list(AUTHOR), List.empty[Affiliation]) {
case (affil, affils) => parse_affil(affil, authors).map(affils :+ _)
}
notifies <-
fold(entry.list(NOTIFY), List.empty[Email]) {
case (email, emails) => parse_email(email, authors).map(emails :+ _)
}
related <-
fold(entry.list(RELATED), List.empty[Reference]) {
case (related, references) => parse_related(related, references).map(references :+ _)
}
license <- licenses.get(entry.get(LICENSE).value)
} yield Model.Create_Entry(
name = Val.ok(entry.get(NAME).value),
title = Val.ok(entry.get(TITLE).value),
topics = Val.ok(topics),
topic_input = parse_topic(entry.get(TOPIC), Nil),
license = license,
`abstract` = Val.ok(entry.get(ABSTRACT).value),
author_input = authors.get(entry.get(AUTHOR).value),
notify_input = authors.get(entry.get(NOTIFY).value),
affils = Val.ok(affils),
notifies = Val.ok(notifies),
related = related,
related_kind = Model.Related.from_string(entry.get(RELATED).get(KIND).value),
related_input = Val.ok(entry.get(RELATED).get(INPUT).value))
for {
(new_author_ids, all_authors) <-
fold(params.list(AUTHOR), (List.empty[Author.ID], authors)) {
case (author, (new_authors, authors)) =>
parse_new_author(author, 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 (affil, (new_affils, authors)) =>
parse_new_affil(affil, 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 (entry, entries) => parse_entry(entry, all_authors).map(entries :+ _)
}
} yield Model.Create(
entries = Val.ok(entries),
new_authors = Val.ok(new_authors),
new_author_input = params.get(AUTHOR).get(NAME).value,
new_author_orcid = params.get(AUTHOR).get(ORCID).value,
new_affils = Val.ok(new_affils),
new_affils_author = all_authors.get(params.get(AFFILIATION).value),
new_affils_input = params.get(AFFILIATION).get(ADDRESS).value)
}
def parse_submission_list(params: Params.Data): Option[Model.Submission_List] = {
def parse_overview(entry: Params.Data): Option[Model.Overview] =
for {
date <-
Exn.capture(LocalDate.parse(entry.get(DATE).value)) match {
case Exn.Res(date) => Some(date)
case Exn.Exn(_) => None
}
status <- Model.Status.from_string(entry.get(STATUS).value)
} yield Model.Overview(entry.get(ID).value, date, entry.get(NAME).value, status)
val submissions =
fold(params.list(ENTRY), List.empty[Model.Overview]) {
case (entry, overviews) => parse_overview(entry).map(overviews :+ _)
}
submissions.map(Model.Submission_List.apply)
}
/* control */
def add_entry(params: Params.Data): Option[Model.T] = parse_create(params).map { model =>
model.copy(entries = Val.ok(model.entries.v :+ Model.Create_Entry(license = licenses.head._2)))
}
def remove_entry(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
} yield model.copy(entries = Val.ok(Utils.remove_at(num_entry, model.entries.v)))
def add_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
} yield
entry.author_input match {
case None =>
model.update_entry(num_entry, entry.copy(
affils = entry.affils.with_err("Select author first")))
case Some(author) =>
val default_affil = author.emails.headOption.orElse(
author.homepages.headOption).getOrElse(Unaffiliated(author.id))
model.update_entry(num_entry, entry.copy(
author_input = None, affils = Val.ok(entry.affils.v :+ default_affil)))
}
def remove_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_affil) <- List_Key.split(AUTHOR, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield
model.update_entry(num_entry, entry.copy(affils =
Val.ok(Utils.remove_at(num_affil, entry.affils.v))))
def add_notify(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
entry1 <-
entry.notify_input match {
case Some(author) =>
author.emails.headOption.map(email => entry.copy(
notify_input = None, notifies = Val.ok(entry.notifies.v :+ email)))
case None =>
Some(entry.copy(notifies = entry.notifies.with_err("Select author first")))
}
} yield model.update_entry(num_entry, entry1)
def remove_notify(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_notify) <- List_Key.split(NOTIFY, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield
model.update_entry(num_entry, entry.copy(notifies =
Val.ok(Utils.remove_at(num_notify, entry.notifies.v))))
def add_topic(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
entry_params <- params.list(ENTRY).unapply(num_entry)
} yield {
val topic = validate_topic(entry_params.get(TOPIC).value, entry.topics.v)
val topic_input = if (topic.is_empty) entry.topic_input else None
model.update_entry(num_entry, entry.copy(
topic_input = topic_input,
topics = Val.ok(entry.topics.v ++ topic.opt).perhaps_err(topic)))
}
def remove_topic(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_topic) <- List_Key.split(TOPIC, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 = entry.copy(topics = Val.ok(Utils.remove_at(num_topic, entry.topics.v)))
model.copy(entries = Val.ok(model.entries.v.updated(num_entry, entry1)))
}
def add_related(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 =
entry.related_kind match {
case None =>
entry.copy(related_input =
entry.related_input.with_err("Select reference kind first"))
case Some(kind) =>
val reference = validate_related(kind, entry.related_input.v, entry.related)
val related_input = if (reference.is_empty) entry.related_input.v else ""
entry.copy(
related = entry.related ++ reference.opt,
related_input = Val.ok(related_input).perhaps_err(reference))
}
model.update_entry(num_entry, entry1)
}
def remove_related(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_related) <- List_Key.split(RELATED, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 = entry.copy(related = Utils.remove_at(num_related, entry.related))
model.copy(entries = Val.ok(model.entries.v.updated(num_entry, entry1)))
}
def add_new_author(params: Params.Data): Option[Model.T] = parse_create(params).map { model =>
val name = model.new_author_input.trim
if (name.isEmpty)
model.copy(new_authors = model.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 updated_authors = model.updated_authors(authors)
var ident = suffix.toLowerCase
for {
c <- prefix.toLowerCase
if updated_authors.contains(ident)
} ident += c.toString
Utils.make_unique(ident, updated_authors.keySet)
}
val id = make_author_id(name)
val author = validate_new_author(id, model.new_author_input, model.new_author_orcid,
model.updated_authors(authors))
val new_author_input = if (author.is_empty) model.new_author_input else ""
val new_author_orcid = if (author.is_empty) model.new_author_orcid else ""
model.copy(
new_author_input = new_author_input,
new_author_orcid = new_author_orcid,
new_authors = Val.ok(model.new_authors.v ++ author.opt).perhaps_err(author))
}
}
def remove_new_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_author <- List_Key.num(AUTHOR, params.get(Web_App.ACTION).value)
author <- model.new_authors.v.unapply(num_author)
if !model.used_authors.contains(author.id)
} yield model.copy(new_authors =
Val.ok(Utils.remove_at(num_author, model.new_authors.v)))
def add_new_affil(params: Params.Data): Option[Model.T] =
parse_create(params).map { model =>
model.new_affils_author match {
case Some(author) =>
val address = model.new_affils_input.trim
if (address.isEmpty)
model.copy(new_affils = model.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)
val new_affils_input = if (affil.is_empty) model.new_affils_input else ""
model.copy(
new_affils_input = new_affils_input,
new_affils = Val.ok(model.new_affils.v ++ affil.opt).perhaps_err(affil))
}
case None => model.copy(new_affils = model.new_affils.with_err("Select author first"))
}
}
def remove_new_affil(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_affil <- List_Key.num(AFFILIATION, params.get(Web_App.ACTION).value)
affil <- model.new_affils.v.unapply(num_affil)
if !model.used_affils.contains(affil)
} yield model.copy(new_affils = Val.ok(Utils.remove_at(num_affil, model.new_affils.v)))
def upload(params: Params.Data): Option[Model.T] = parse_create(params).map { create =>
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 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 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 mode match {
case Mode.EDIT =>
if (Server.this.entries.contains(name)) Val.ok(name)
else Val.err(name, "Entry does not exist")
case Mode.SUBMISSION =>
if (Server.this.entries.contains(name)) Val.err(name, "Entry already exists")
else Val.ok(name)
}
def 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 new_authors(authors: List[Author]): Val[List[Author]] =
if (!authors.forall(author => create.used_authors.contains(author.id)))
Val.err(authors, "Unused authors")
else Val.ok(authors)
def new_affils(affils: List[Affiliation]): Val[List[Affiliation]] =
if (!affils.forall(affil => create.used_affils.contains(affil)))
Val.err(affils, "Unused affils")
else Val.ok(affils)
def 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 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 topics(topics: List[Topic]): Val[List[Topic]] =
if (topics.isEmpty) Val.err(topics, "Must contain at least one topic") else Val.ok(topics)
def `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 validated = create.copy(
entries = validate(
entries, create.entries.v.map(entry => entry.copy(
name = validate(name, entry.name.v),
title = validate(title, entry.title.v),
affils = validate(entry_authors, entry.affils.v),
notifies = validate(notifies, entry.notifies.v),
topics = validate(topics, entry.topics.v),
`abstract` = validate(`abstract`, entry.`abstract`.v)
))),
new_authors = validate(new_authors, create.new_authors.v),
new_affils = validate(new_affils, create.new_affils.v))
if (ok) {
val (updated_authors, entries) = create.create(authors)
Model.Upload(Model.Metadata(updated_authors, entries), params.get(MESSAGE).value, "")
} else validated
}
def create(params: Params.Data): Option[Model.T] = {
upload(params) match {
case Some(upload: Model.Upload) =>
mode match {
case Mode.EDIT =>
handler.create(Date.now(), upload.meta, upload.message, Bytes.empty, "")
Some(Model.Created(upload.meta.entries.head.name))
case Mode.SUBMISSION =>
val archive = Bytes.decode_base64(params.get(ARCHIVE).get(FILE).value)
val file_name = params.get(ARCHIVE).value
if (archive.is_empty || file_name.isEmpty) {
Some(upload.copy(error = "Select a file"))
} else if (!file_name.endsWith(".zip") && !file_name.endsWith(".tar.gz")) {
Some(upload.copy(error = "Only .zip and .tar.gz archives allowed"))
} else {
val ext = if (file_name.endsWith(".zip")) ".zip" else ".tar.gz"
val id = handler.create(Date.now(), upload.meta, upload.message, archive, ext)
Some(Model.Created(id))
}
}
case _ => None
}
}
def empty_submission: Option[Model.T] =
Some(Model.Create(entries =
Val.ok(List(Model.Create_Entry(license = licenses.head._2)))))
def get_submission(props: Properties.T): Option[Model.Submission] =
- Properties.get(props, ID).flatMap(handler.get(_, all_topics, licenses))
+ Properties.get(props, ID).flatMap(handler.get(_, topics, licenses))
def resubmit(params: Params.Data): Option[Model.T] =
- handler.get(params.get(ACTION).value, all_topics, licenses).map(submission =>
+ handler.get(params.get(ACTION).value, topics, licenses).map(submission =>
Model.Upload(submission.meta, submission.message, ""))
def submit(params: Params.Data): Option[Model.T] =
- handler.get(params.get(ACTION).value, all_topics, licenses).flatMap { submission =>
+ handler.get(params.get(ACTION).value, topics, licenses).flatMap { submission =>
if (submission.status.nonEmpty) None
else {
handler.submit(submission.id)
Some(submission.copy(status = Some(Model.Status.Submitted)))
}
}
def abort_build(params: Params.Data): Option[Model.T] =
- handler.get(params.get(ACTION).value, all_topics, licenses).flatMap { submission =>
+ handler.get(params.get(ACTION).value, topics, licenses).flatMap { submission =>
if (submission.build != Model.Build.Running) None
else {
handler.abort_build(submission.id)
Some(submission.copy(build = Model.Build.Aborted))
}
}
def set_status(params: Params.Data): Option[Model.T] = {
for {
list <- parse_submission_list(params)
num_entry <- List_Key.num(ENTRY, params.get(ACTION).value)
changed <- list.submissions.unapply(num_entry)
} yield {
if (changed.status == Model.Status.Added && !devel) {
progress.echo_if(verbose, "Updating server data...")
val id_before = repo.id()
repo.pull()
repo.update()
val id_after = repo.id()
if (id_before != id_after) {
load()
progress.echo("Updated repo from " + id_before + " to " + id_after)
}
}
handler.set_status(changed.id, changed.status)
list
}
}
def submission_list: Option[Model.T] = Some(handler.list())
def download(props: Properties.T): Option[Path] =
for {
id <- Properties.get(props, ID)
patch <- handler.get_patch(id)
} yield patch
def download_archive(props: Properties.T): Option[Path] =
for {
id <- Properties.get(props, ID)
archive <- handler.get_archive(id)
} yield archive
def style_sheet: Option[Path] =
Some(afp_structure.base_dir + Path.make(List("tools", "main.css")))
val error_model = Model.Invalid
val endpoints = List(
Get(SUBMIT, "empty submission form", _ => empty_submission),
Get(SUBMISSION, "get submission", get_submission),
Get(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", parse_create),
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 =
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(api.api_url(API_CSS)))
}
/* 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_url = Url("http://localhost:8080")
var devel = false
var verbose = false
var port = 8080
var dir: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle afp_submit [OPTIONS]
Options are:
-a PATH backend path (if endpoint is not server root)
-b URL application frontend url. Default: """ + frontend_url + """"
-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.
""",
"a:" -> (arg => backend_path = Path.explode(arg)),
"b:" -> (arg => frontend_url = Url(arg)),
"d" -> (_ => devel = true),
"p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true),
"D:" -> (arg => dir = Some(Path.explode(arg))))
getopts(args)
val afp_structure = AFP_Structure()
val progress = new Console_Progress(verbose = verbose)
val (handler, mode) = dir match {
case Some(dir) => (Handler.Adapter(dir, afp_structure), Mode.SUBMISSION)
case None => (Handler.Edit(afp_structure), Mode.EDIT)
}
val api = new API(frontend_url, backend_path, devel = devel)
val server = new Server(api = api, afp_structure = afp_structure, mode = mode,
handler = handler, devel = devel, verbose = verbose, progress = progress, port = port)
server.run()
})
}
diff --git a/tools/metadata.scala b/tools/metadata.scala
--- a/tools/metadata.scala
+++ b/tools/metadata.scala
@@ -1,418 +1,460 @@
/* Author: Fabian Huch, TU Muenchen
AFP metadata model and TOML serialization.
*/
package afp
import isabelle.*
import java.time.LocalDate
import java.net.URI
+import scala.collection.immutable.ListMap
+
object Metadata {
/* affiliations */
sealed trait Affiliation {
def author: Author.ID
}
case class Unaffiliated(override val author: Author.ID)
extends Affiliation
case class Email(override val author: Author.ID, id: Email.ID, address: String)
extends Affiliation {
private val Address = "([^@]+)@(.+)".r
val (user, host) = address match {
case Address(user, host) => (user, host)
case _ => error("Invalid address: " + address)
}
}
object Email {
type ID = String
def apply(author: Author.ID, id: Email.ID, user: String, host: String): Email =
Email(author, id, user + "@" + host)
}
case class Homepage(override val author: Author.ID, id: Homepage.ID, url: Url) extends Affiliation
object Homepage {
type ID = String
}
/* authors */
case class Orcid(identifier: String) {
require(
"^([0-9]{4})-([0-9]{4})-([0-9]{4})-([0-9]{3}[0-9X])$".r.matches(identifier),
"Invalid format for orcid: " + quote(identifier))
def url: Url = Url("https://orcid.org/" + identifier)
}
case class Author(
id: Author.ID,
name: String,
emails: List[Email] = Nil,
homepages: List[Homepage] = Nil,
orcid: Option[Orcid] = None
)
object Author {
type ID = String
}
+ type Authors = ListMap[Author.ID, Author]
+ object Authors {
+ def empty: Authors = Authors(Nil)
+ def apply(authors: List[Author]): Authors =
+ ListMap.from(authors.map(author => author.id -> author))
+ }
+
/* topics */
sealed trait Classification {
def desc: String
def url: Url
}
case class ACM(id: String, override val desc: String) extends Classification {
val url = Url("https://dl.acm.org/topic/ccs2012/" + id)
}
case class AMS(id: String, hierarchy: List[String]) extends Classification {
val code: String = id.length match {
case 2 => id + "-XX"
case 3 => id + "xx"
case 5 => id
case _ => error("Invalid ams id:" + id)
}
override val desc: String = hierarchy.mkString(" / ")
override val url: Url = Url("https://mathscinet.ams.org/mathscinet/msc/msc2020.html?t=" + code)
}
case class Topic(
id: Topic.ID,
name: String,
classification: List[Classification] = Nil,
sub_topics: List[Topic] = Nil
) {
def all_topics: List[Topic] = this :: sub_topics.flatMap(_.all_topics)
}
object Topic {
type ID = String
}
+ type Topics = ListMap[Topic.ID, Topic]
+ object Topics {
+ def empty: Topics = Topics(Nil)
+ def apply(root_topics: List[Topic]): Topics =
+ ListMap.from(root_topics.flatMap(_.all_topics).map(topic => topic.id -> topic))
+
+ def root_topics(topics: Topics): List[Topic] = {
+ val sub_topics = topics.values.flatMap(_.sub_topics).map(_.id).toSet
+ topics.values.filterNot(topic => sub_topics.contains(topic.id)).toList
+ }
+ }
+
+
/* releases */
type Date = LocalDate
object Isabelle {
type Version = String
}
case class Release(entry: Entry.Name, date: Date, isabelle: Isabelle.Version)
+ type Releases = ListMap[Entry.Name, List[Release]]
+ object Releases {
+ def empty: Releases = Releases(Nil)
+ def apply(releases: List[Release]): Releases =
+ Utils.group_sorted(releases, (release: Release) => release.entry)
+ }
+
/* license */
case class License(id: License.ID, name: String)
object License {
type ID = String
}
+ type Licenses = ListMap[License.ID, License]
+ object Licenses {
+ def empty: Licenses = Licenses(Nil)
+ def apply(licenses: List[License]): Licenses =
+ ListMap.from(licenses.map(license => license.id -> license))
+ }
+
/* references */
sealed trait Reference
case class DOI(identifier: String) extends Reference {
require("^10.([1-9][0-9]{3,})/(.+)".r.matches(identifier),
"invalid format for DOI: " + quote(identifier))
def uri: URI = new URI("doi:" + identifier)
def url: Url = Url("https://doi.org/" + identifier)
def formatted(style: String = "apa"): String =
Utils.fetch_text(url, Map("Accept" -> ("text/x-bibliography; style=" + style)))
}
case class Formatted(rep: String) extends Reference
/* misc */
type Change_History = Map[Date, String]
type Extra = Map[String, String]
/* entry */
case class Entry(
name: Entry.Name,
title: String,
authors: List[Affiliation],
date: Date,
topics: List[Topic],
`abstract`: String,
notifies: List[Email],
license: License,
note: String,
contributors: List[Affiliation] = Nil,
change_history: Change_History = Map.empty,
extra: Extra = Map.empty,
releases: List[Release] = Nil,
statistics_ignore: Boolean = false,
related: List[Reference] = Nil)
object Entry {
type Name = String
}
+ type Entries = ListMap[Entry.Name, Entry]
+ object Entries {
+ def empty: Entries = Entries(Nil)
+ def apply(entries: List[Entry]) = ListMap.from(entries.map(entry => entry.name -> entry))
+ }
+
/* 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.keys)))
object TOML {
import isabelle.TOML.{Array, Boolean, Key, Local_Date, String, Table}
/* affils */
def from_email(email: Email): Table =
Table(
"user" -> Array(email.user.split('.').map(String(_))),
"host" -> Array(email.host.split('.').map(String(_))))
def to_email(author_id: Author.ID, email_id: Email.ID, email: Table): Email = {
val user = email.array("user").string.values.map(_.rep)
val host = email.array("host").string.values.map(_.rep)
Email(author_id, email_id, user.mkString("."), host.mkString("."))
}
/* author */
def from_author(author: Author): Table =
Table(
"name" -> String(author.name),
"emails" -> Table(author.emails.map(e => e.id -> from_email(e))),
"homepages" -> Table(author.homepages.map(h => h.id -> String(h.url.toString)))) ++
author.orcid.map(orcid => Table("orcid" -> String(orcid.identifier))).getOrElse(Table())
def to_author(author_id: Author.ID, author: Table): Author = {
val emails = author.table("emails").table.values.map {
case (id, email) => to_email(author_id, id, email)
}
val homepages = author.table("homepages").string.values.map {
case (id, url) => Homepage(author = author_id, id = id, url = Url(url.rep))
}
val orcid = author.string.get("orcid").map(_.rep).map(Orcid(_))
Author(
id = author_id,
name = author.string("name").rep,
orcid = orcid,
emails = emails,
homepages = homepages)
}
def from_authors(authors: List[Author]): Table =
Table(authors.map(author => author.id -> from_author(author)))
def to_authors(authors: Table): List[Author] = authors.table.values.map(to_author)
/* topics */
def from_acm(acm: ACM): Table =
Table("id" -> String(acm.id), "desc" -> String(acm.desc))
def to_acm(acm: Table): ACM =
ACM(acm.string("id").rep, acm.string("desc").rep)
def from_ams(ams: AMS): Table =
Table("id" -> String(ams.id), "hierarchy" -> Array(ams.hierarchy.map(String(_))))
def to_ams(ams: Table): AMS =
AMS(ams.string("id").rep, ams.array("hierarchy").string.values.map(_.rep))
def from_classifications(classifications: List[Classification]): Table =
Table(classifications.map {
case acm: ACM => "acm" -> from_acm(acm)
case ams: AMS => "ams" -> from_ams(ams)
})
def to_classifications(classifications: Table): List[Classification] =
classifications.table.values.map {
case ("ams", ams) => to_ams(ams)
case ("acm", acm) => to_acm(acm)
case (c, _) => error("Unknown topic classification: " + quote(c))
}
def from_topics(root_topics: List[Topic]): Table =
Table(root_topics.map(t => t.name -> (
Table("classification" -> from_classifications(t.classification)) ++
from_topics(t.sub_topics))))
def to_topics(root_topics: Table): List[Topic] = {
def to_topics_rec(topics: List[(Key, Table)], root: Topic.ID): List[Topic] = {
topics.map {
case (name, data) =>
val id = (if (root.nonEmpty) root + "/" else "") + name
val classifications = to_classifications(data.table("classification"))
val sub_topics = data.table.values.filterNot(_._1 == "classification")
Topic(id, name, classifications, to_topics_rec(sub_topics, id))
}
}
to_topics_rec(root_topics.table.values, "")
}
/* releases */
def from_releases(releases: List[Release]): Table =
Table(Utils.group_sorted(releases, (r: Release) => r.entry).view.mapValues { entry_releases =>
Table(entry_releases.map(r => r.date.toString -> String(r.isabelle)))
}.toList)
def to_releases(map: Table): List[Release] =
map.table.values.flatMap {
case (entry, releases) => releases.string.values.map {
case (date, version) =>
Release(entry = entry, date = LocalDate.parse(date), isabelle = version.rep)
}
}
/* affiliation */
def from_affiliations(affiliations: List[Affiliation]): Table =
Table(Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues(vs =>
Table(vs.collect {
case Email(_, id, _) => "email" -> String(id)
case Homepage(_, id, _) => "homepage" -> String(id)
})).toList)
- def to_affiliations(affiliations: Table, authors: Map[Author.ID, Author]): List[Affiliation] = {
+ def to_affiliations(affiliations: Table, authors: Authors): List[Affiliation] = {
def to_affiliation(affiliation: (Key, String), author: Author): Affiliation = {
affiliation match {
case ("email", id) => author.emails.find(_.id == id.rep) getOrElse
error("Email not found: " + quote(id.rep))
case ("homepage", id) => author.homepages.find(_.id == id.rep) getOrElse
error("Homepage not found: " + quote(id.rep))
case e => error("Unknown affiliation type: " + e)
}
}
affiliations.table.values.flatMap {
case (id, author_affiliations) =>
val author = by_id(authors, id)
if (author_affiliations.is_empty) List(Unaffiliated(author.id))
else author_affiliations.string.values.map(to_affiliation(_, author))
}
}
def from_emails(emails: List[Email]): Table =
Table(emails.map(email => email.author -> String(email.id)))
- def to_emails(emails: Table, authors: Map[Author.ID, Author]): List[Email] =
+ def to_emails(emails: Table, authors: Authors): List[Email] =
emails.string.values.map {
case (author, id) => by_id(authors, author).emails.find(_.id == id.rep) getOrElse
error("Email not found: " + quote(id.rep))
}
/* license */
def from_licenses(licenses: List[License]): Table =
Table(licenses.map(license => license.id -> Table("name" -> String(license.name))))
def to_licenses(licenses: Table): List[License] = {
licenses.table.values.map {
case (id, license) => License(id, license.string("name").rep)
}
}
- def to_license(license: String, licenses: Map[License.ID, License]): License =
+ def to_license(license: String, licenses: Licenses): License =
licenses.getOrElse(license.rep, error("No such license: " + quote(license.rep)))
/* history */
def from_change_history(change_history: Change_History): Table =
Table(change_history.map { case (date, str) => date.toString -> String(str) })
def to_change_history(change_history: Table): Change_History =
change_history.string.values.map {
case (date, entry) => LocalDate.parse(date) -> entry.rep
}.toMap
/* references */
def from_related(references: List[Reference]): Table = {
val dois = references.collect { case d: DOI => d }
val formatted = references.collect { case f: Formatted => f }
Table(
"dois" -> Array(dois.map(_.identifier).map(String(_))),
"pubs" -> Array(formatted.map(_.rep).map(String(_))))
}
def to_related(references: Table): List[Reference] = {
val dois = references.array.get("dois").toList.flatMap(_.string.values.map(_.rep))
val pubs = references.array.get("pubs").toList.flatMap(_.string.values.map(_.rep))
dois.map(DOI(_)) ++ pubs.map(Formatted(_))
}
/* entry */
def from_entry(entry: Entry): Table = {
Table(
"title" -> String(entry.title),
"authors" -> from_affiliations(entry.authors),
"contributors" -> from_affiliations(entry.contributors),
"date" -> Local_Date(entry.date),
"topics" -> Array(entry.topics.map(_.id).map(String(_))),
"abstract" -> String(entry.`abstract`),
"notify" -> from_emails(entry.notifies),
"license" -> String(entry.license.id),
"note" -> String(entry.note),
"history" -> from_change_history(entry.change_history),
"extra" -> Table(entry.extra.view.mapValues(String(_)).toList),
"related" -> from_related(entry.related)) ++
(if (entry.statistics_ignore) Table("statistics_ignore" -> Boolean(true)) else Table())
}
def to_entry(
name: Entry.Name,
entry: Table,
- authors: Map[Author.ID, Author],
- topics: Map[Topic.ID, Topic],
- licenses: Map[License.ID, License],
+ authors: Authors,
+ topics: Topics,
+ licenses: Licenses,
releases: List[Release]
): Entry =
Entry(
name = name,
title = entry.string("title").rep,
authors = to_affiliations(entry.table("authors"), authors),
date = entry.local_date("date").rep,
topics = entry.array("topics").string.values.map(_.rep).map(by_id(topics, _)),
`abstract` = entry.string("abstract").rep,
notifies = to_emails(entry.table("notify"), authors),
license = to_license(entry.string("license"), licenses),
note = entry.string("note").rep,
contributors = to_affiliations(entry.table("contributors"), authors),
change_history = to_change_history(entry.table("history")),
extra = entry.table("extra").string.values.map((k, v) => (k, v.rep)).toMap,
releases = releases,
statistics_ignore = entry.boolean.get("statistics_ignore").map(_.rep).getOrElse(false),
related = to_related(entry.table("related")))
}
}