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,
)