diff --git a/.hgignore b/.hgignore --- a/.hgignore +++ b/.hgignore @@ -1,71 +1,72 @@ syntax: glob afp-export-20??-??-?? *.pyc *~ .DS_Store thys/Tree-Automata/code/haskell/generated/Nat.hs thys/Tree-Automata/code/haskell/generated/Ta.hs thys/Tree-Automata/code/ml/generated/Ta.ML thys/Tree-Automata/code/ocaml/generated/Ta.ml thys/BinarySearchTree/BinaryTree_Code.ML thys/BinarySearchTree/BinaryTree_TacticStyle_Code.ML thys/CAVA_LTL_Modelchecker/code/examples/mulog/Mulog_Export.sml thys/ClockSynchInst/document/abs_distrib_mult.cvc thys/ClockSynchInst/document/abs_distrib_mult.ics thys/ClockSynchInst/document/abs_distrib_mult2.cvc thys/ClockSynchInst/document/accur_pres.cvc thys/ClockSynchInst/document/accur_pres.ics thys/ClockSynchInst/document/bound_prec_enh.cvc thys/ClockSynchInst/document/bound_prec_enh.ics thys/ClockSynchInst/document/bound_prec_enh4.cvc thys/ClockSynchInst/document/bound_prec_enh7.cvc thys/Depth-First-Search/dfs.ML thys/Well_Quasi_Orders/generated/ thys/JinjaThreads/Execute/JVM_Execute2.ML thys/JinjaThreads/Execute/JWellForm.ML thys/JinjaThreads/Execute/J_Execute.ML thys/JinjaThreads/JVM_Execute2.ML thys/JinjaThreads/JWellForm.ML thys/JinjaThreads/J_Execute.ML thys/Vickrey_Clarke_Groves/VCG-withoutWrapper.scala thys/CAVA_LTL_Modelchecker/Nested_DFS/nested_dfs_hash.sml thys/CAVA_LTL_Modelchecker/code/CAVA_Export.sml thys/Collections/Examples/Autoref/nested_dfs.sml thys/Promela/Promela.sml thys/Formal_SSA/BraunSSA.ml thys/LTL_to_DRA/Code/LTL_to_DRA_Translator.sml thys/EdmondsKarp_Maxflow/evaluation/fofu-SML/Fofu_Export.sml thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/dijkstra_export.sml thys/Refine_Imperative_HOL/benchmarks/Heapmap/isabelle/heapmap_export.sml thys/Refine_Imperative_HOL/benchmarks/NestedDFS/isabelle/NDFS_Benchmark_export.sml thys/SPARCv8/SparcModel_MMU/sparc_seq thys/Tree-Automata/code/haskell/generated/Array.hs thys/Tree-Automata/code/haskell/generated/Data_Bits.hs thys/Tree-Automata/code/haskell/generated/Natural.hs thys/Tree-Automata/code/haskell/generated/Uint32.hs thys/Verified_SAT_Based_AI_Planning/code/generated admin/py-bootstrap admin/venv -tools/**.jar \ No newline at end of file +tools/**.jar +web/hugo \ No newline at end of file diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,13 +1,14 @@ title = AFP/Tools module = $AFP_BASE/tools/lib/classes/afp_tools.jar requirements = \ env:ISABELLE_SCALA_JAR sources = \ tools/migration/afp_migrate_metadata.scala \ + tools/afp_build_site.scala \ tools/afp_check_roots.scala \ tools/afp_dependencies.scala \ tools/afp_tool.scala \ tools/metadata.scala \ tools/toml.scala \ tools/utils.scala services = afp.Tools diff --git a/tools/afp_build_site.scala b/tools/afp_build_site.scala new file mode 100644 --- /dev/null +++ b/tools/afp_build_site.scala @@ -0,0 +1,162 @@ +package afp + + +import isabelle._ + +import afp.Metadata.Author + + +object AFP_Build_Site +{ + + object JSON + { + type T = isabelle.JSON.T + + object Object + { + type T = isabelle.JSON.Object.T + } + + def from_authors(authors: List[Author]): T = + Metadata.TOML.from_authors(authors) + + def from_affiliations( + affiliations: List[Metadata.Affiliation], + authors: Map[Metadata.Author.ID, Metadata.Author]): T = + { + Utils.group_sorted(affiliations, (a: Metadata.Affiliation) => a.author).toList.map { + case (author, author_affiliations) => + val homepage = author_affiliations.collectFirst { case Metadata.Homepage(_, _, url) => url } + val email = author_affiliations.collectFirst { case Metadata.Email(_, _, address) => address } + + var res = Utils.the_entry(authors, author).name + homepage.foreach(url => res = "" + res + "") + email.foreach(address => res += "" + "\uD83D\uDCE7") + res + } + } + + def from_change_history(history: Metadata.Change_History): Object.T = + { + if (history.isEmpty) { + Map.empty + } else { + Map("Change history" -> history.map { + case (date, str) => "[" + date.toString + "] " + str + }.mkString("\n")) + } + } + + def from_entry(entry: Metadata.Entry, authors: Map[Metadata.Author.ID, Author]): T = + isabelle.JSON.Object( + ("title" -> entry.title) :: + ("authors" -> from_affiliations(entry.authors, authors)) :: + (if (entry.contributors.nonEmpty) "contributors" -> from_affiliations(entry.contributors, authors) :: Nil + else Nil) ::: + ("date" -> entry.date.toString) :: + ("topics" -> entry.topics.map(_.id)) :: + ("abstract" -> entry.`abstract`) :: + ("license" -> entry.license) :: + (if (entry.releases.nonEmpty) + "releases" -> entry.releases.map(r => r.isabelle -> r.date.toString).toMap :: Nil + else Nil) ::: + (if (entry.note.nonEmpty) "note" -> entry.note :: Nil else Nil) ::: + (if (entry.change_history.nonEmpty || entry.extra.nonEmpty) + "extra" -> (from_change_history(entry.change_history) ++ entry.extra) :: Nil + else Nil): _*) + } + + private val gen_dir = Path.explode("$AFP_BASE/web/hugo") + + private def write_gen(file: Path, content: JSON.T): Unit = + { + val path = gen_dir + file + path.dir.file.mkdirs() + File.write(path, isabelle.JSON.Format(content)) + } + + def afp_build_site(progress: Progress = new Progress()): Unit = + { + val metadata_dir = Path.explode("$AFP_BASE") + Path.basic("metadata") + + + /* authors */ + + progress.echo("Preparing authors...") + + val authors_toml = TOML.parse(File.read(metadata_dir + Path.basic("authors.toml"))) + val authors = Metadata.TOML.to_authors(authors_toml) + val authors_by_id = Utils.grouped_sorted(authors, (a: Metadata.Author) => a.id) + + write_gen(Path.make(List("data", "authors.json")), JSON.from_authors(authors)) + + + /* topics */ + + progress.echo("Preparing topics...") + + val topics_toml = TOML.parse(File.read(metadata_dir + Path.basic("topics.toml"))) + val topics = Metadata.TOML.to_topics(topics_toml) + + def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] = topic :: topic.sub_topics.flatMap(sub_topics) + + val all_topics_by_id = Utils.grouped_sorted(topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id) + + + /* releases */ + + progress.echo("Preparing releases...") + + val toml_releases = TOML.parse(File.read(metadata_dir + Path.basic("releases.toml"))) + val all_releases = Metadata.TOML.to_releases(toml_releases).groupBy(_.entry) + + + /* entries */ + + val Entry = """([a-zA-Z0-9_+-]+)\.toml""".r + val entries_dir = metadata_dir + Path.basic("entries") + for (file <- File.read_dir(entries_dir)) { + val short_name = file match { + case Entry(short_name) => short_name + case _ => error("Unrecognized file in entries: " + file) + } + + progress.echo("Preparing entry " + short_name + "...") + + val content = File.read(entries_dir + Path.basic(file)) + val toml = TOML.parse(content) ++ TOML.T("short_name" -> short_name) + val releases = all_releases.getOrElse(short_name, error("No releases for entry: " + quote(short_name))) + val metadata = Metadata.TOML.to_entry(toml, authors_by_id, all_topics_by_id, releases) + + write_gen(Path.make(List("entries", short_name + ".json")), JSON.from_entry(metadata, authors_by_id)) + } + } + + val isabelle_tool = + Isabelle_Tool( + "afp_build_site", + "generates afp website", + Scala_Project.here, + args => { + val getopts = Getopts( + """ +Usage: isabelle afp_build_site [OPTIONS] + + Options are: + -B DIR afp base dir (default "$AFP_BASE") + -H DIR afp browser info dir (default "$AFP_BASE/web/browser_info") + -R DIR afp release dir (default "$AFP_BASE/web/release") + + Generates the AFP website. +""" + ) + + getopts(args) + + val progress = new Console_Progress() + + afp_build_site(progress) + } + ) +} \ No newline at end of file diff --git a/tools/afp_tool.scala b/tools/afp_tool.scala --- a/tools/afp_tool.scala +++ b/tools/afp_tool.scala @@ -1,16 +1,17 @@ package afp import isabelle.Isabelle_Scala_Tools import afp.migration._ class Admin_Tools extends Isabelle_Scala_Tools( AFP_Migrate_Metadata.isabelle_tool, ) class Tools extends Isabelle_Scala_Tools( + AFP_Build_Site.isabelle_tool, AFP_Check_Roots.isabelle_tool, AFP_Dependencies.isabelle_tool, )