diff --git a/etc/build.props b/etc/build.props
--- a/etc/build.props
+++ b/etc/build.props
@@ -1,19 +1,20 @@
title = AFP/Tools
module = $AFP_BASE/tools/lib/classes/afp_tools.jar
requirements = \
env:ISABELLE_SCALA_JAR
sources = \
tools/admin/afp_build_hugo.scala \
tools/admin/afp_build_python.scala \
tools/migration/afp_migrate_metadata.scala \
tools/afp_build_site.scala \
tools/afp_check_roots.scala \
tools/afp_dependencies.scala \
+ tools/afp_site_gen.scala \
tools/afp_structure.scala \
tools/afp_tool.scala \
tools/hugo.scala \
tools/metadata.scala \
tools/python.scala \
tools/toml.scala \
tools/utils.scala
services = afp.Tools
diff --git a/tools/afp_build_site.scala b/tools/afp_build_site.scala
--- a/tools/afp_build_site.scala
+++ b/tools/afp_build_site.scala
@@ -1,214 +1,52 @@
package afp
import isabelle._
object AFP_Build_Site
{
- /* json */
-
- object JSON
- {
- type T = isabelle.JSON.T
-
- object Object
- {
- type T = isabelle.JSON.Object.T
- }
-
- def from_authors(authors: List[Metadata.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, Metadata.Author]): JSON.Object.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): _*)
- }
-
-
- /* site generation */
-
def afp_build_site(
- html_dir: Path,
- afp_structure: AFP_Structure,
- layout: Hugo.Layout,
+ out_dir: Path, layout: Hugo.Layout,
+ do_watch: Boolean = false,
progress: Progress = new Progress()): Unit =
{
- /* add authors */
-
- progress.echo("Preparing authors...")
-
- val authors = afp_structure.load_authors
- val authors_by_id = Utils.grouped_sorted(authors, (a: Metadata.Author) => a.id)
-
- layout.write_data(Path.basic("authors.json"), JSON.from_authors(authors))
-
-
- /* add topics */
-
- progress.echo("Preparing topics...")
-
- val topics = afp_structure.load_topics
- def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] = topic :: topic.sub_topics.flatMap(sub_topics)
-
- val topics_by_id = Utils.grouped_sorted(topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id)
-
-
- /* add releases */
-
- progress.echo("Preparing releases...")
-
- val releases_by_entry = afp_structure.load_releases.groupBy(_.entry)
-
-
- /* add entries and theory listings */
-
- progress.echo("Preparing entries...")
-
- val sessions_structure = afp_structure.sessions_structure
- val deps = Sessions.deps(sessions_structure)
-
- for (name <- afp_structure.entries) {
- val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, releases_by_entry)
-
- val topo_theories =
- for {
- session <- afp_structure.entry_sessions(name)
- base = deps(session.name)
- node <- base.session_theories
- } yield node.theory_base_name
-
- val entry_json = JSON.from_entry(entry, authors_by_id) ++ Map("theories" -> topo_theories)
-
- layout.write_content(Path.make(List("entries", name + ".md")), entry_json)
-
- val entry_html = """dynamic"
+ if (do_watch) {
+ Hugo.watch(layout, out_dir, progress).check
+ } else {
+ progress.echo("Building site...")
- layout.write_asset(Path.make(List("theories", name + ".html")), entry_html)
- }
-
-
- /* add dependencies */
-
- progress.echo("Preparing dependencies...")
-
- val afp_dependencies = AFP_Dependencies.afp_dependencies(Path.explode("$AFP"))
- val dep_json = AFP_Dependencies.JSON.from_dependencies(afp_dependencies)
-
- layout.write_data(Path.basic("dependencies.json"), dep_json)
-
- val entries_dir = layout.content_dir + Path.basic("entries")
- val dep_file = layout.data_dir + Path.basic("dependencies.json")
- val dependencies_cmd = "from dependencies import *; add_dependencies(" +
- commas_quote(List(entries_dir.implode, dep_file.implode)) + ")"
- Python.run(dependencies_cmd).check
-
-
- /* add related entries */
-
- progress.echo("Preparing related entries...")
+ Hugo.build(layout, out_dir).check
- val related_cmd = "from related import *; add_related(" + quote(entries_dir.implode) + ")"
- Python.run(related_cmd).check
-
-
- /* add statistics */
-
- progress.echo("Preparing statistics...")
-
- val statistics_cmd = "from statistics import *; add_statistics(" +
- commas_quote(
- List(
- Path.explode("$AFP_BASE").absolute.implode,
- Path.explode("$AFP").absolute.implode,
- layout.data_dir.implode)) +
- ")"
- Python.run(statistics_cmd).check
- (layout.data_dir + Path.basic("statistics.html")).file.delete()
-
- progress.echo("Finished sitegen preparation.")
-
-
- /* hugo */
-
- progress.echo("Generating site...")
-
- layout.write_static()
- layout.build().check
-
- progress.echo("Finished sitegen")
+ progress.echo("Build in " + (out_dir + Path.basic("index.html")).absolute.implode)
+ }
}
- val isabelle_tool = Isabelle_Tool("afp_build_site", "generates afp website", Scala_Project.here, args =>
+ val isabelle_tool = Isabelle_Tool("afp_build_site", "build generated afp website source", Scala_Project.here, args =>
{
- var base_dir = Path.explode("$AFP_BASE")
- var hugo_dir = base_dir + Path.make(List("web", "hugo"))
- var out_dir = base_dir + Path.basic("web")
+ var hugo_dir = Path.explode("$AFP_BASE") + Path.make(List("web", "hugo"))
+ var out_dir = Path.explode("$AFP_BASE") + Path.basic("web")
+ var do_watch = false
val getopts = Getopts("""
-Usage: isabelle afp_build_site [OPTIONS] HTML_DIR
+Usage: isabelle afp_build_site [OPTIONS]
Options are:
- -B DIR afp base dir (default "$AFP_BASE")
- -H DIR generated hugo project dir (default "$AFP_BASE/web/hugo")
+ -H DIR generated sources dir (default "$AFP_BASE/web/hugo")
-O DIR output dir (default "$AFP_BASE/web")
+ -w watch sources and serve result
- Generates the AFP website. HTML files of entries are dynamically loaded.
+ Build the AFP website from generated sources.
""",
- "B:" -> (arg => base_dir = Path.explode(arg)),
"H:" -> (arg => hugo_dir = Path.explode(arg)),
- "O:" -> (arg => out_dir = Path.explode(arg)))
+ "O:" -> (arg => out_dir = Path.explode(arg)),
+ "w" -> (_ => do_watch = true))
- val html_dir = getopts(args) match {
- case dir :: Nil => Path.explode(dir)
- case _ => getopts.usage()
- }
+ getopts(args)
- val afp_structure = AFP_Structure(base_dir)
- val layout = Hugo.Layout(hugo_dir, out_dir)
+ val layout = Hugo.Layout(hugo_dir)
val progress = new Console_Progress()
- afp_build_site(html_dir = html_dir, afp_structure = afp_structure, layout = layout, progress = progress)
+ afp_build_site(out_dir = out_dir, layout = layout, progress = progress, do_watch = do_watch)
})
}
\ No newline at end of file
diff --git a/tools/afp_site_gen.scala b/tools/afp_site_gen.scala
new file mode 100644
--- /dev/null
+++ b/tools/afp_site_gen.scala
@@ -0,0 +1,226 @@
+package afp
+
+
+import isabelle._
+
+
+object AFP_Site_Gen
+{
+ /* json */
+
+ object JSON
+ {
+ type T = isabelle.JSON.T
+
+ object Object
+ {
+ type T = isabelle.JSON.Object.T
+ }
+
+ def from_authors(authors: List[Metadata.Author]): T =
+ 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, Metadata.Author]): JSON.Object.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): _*)
+ }
+
+
+ /* site generation */
+
+ def afp_site_gen(
+ html_dir: Path,
+ out_dir: Option[Path],
+ layout: Hugo.Layout,
+ afp_structure: AFP_Structure,
+ progress: Progress = new Progress()): Unit =
+ {
+ /* add authors */
+
+ progress.echo("Preparing authors...")
+
+ val authors = afp_structure.load_authors
+ val authors_by_id = Utils.grouped_sorted(authors, (a: Metadata.Author) => a.id)
+
+ layout.write_data(Path.basic("authors.json"), JSON.from_authors(authors))
+
+
+ /* add topics */
+
+ progress.echo("Preparing topics...")
+
+ val topics = afp_structure.load_topics
+ def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] = topic :: topic.sub_topics.flatMap(sub_topics)
+
+ val topics_by_id = Utils.grouped_sorted(topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id)
+
+
+ /* add releases */
+
+ progress.echo("Preparing releases...")
+
+ val releases_by_entry = afp_structure.load_releases.groupBy(_.entry)
+
+
+ /* add entries and theory listings */
+
+ progress.echo("Preparing entries...")
+
+ val sessions_structure = afp_structure.sessions_structure
+ val deps = Sessions.deps(sessions_structure)
+
+ for (name <- afp_structure.entries) {
+ val entry = afp_structure.load_entry(name, authors_by_id, topics_by_id, releases_by_entry)
+
+ val topo_theories =
+ for {
+ session <- afp_structure.entry_sessions(name)
+ base = deps(session.name)
+ node <- base.session_theories
+ } yield node.theory_base_name
+
+ val entry_json = JSON.from_entry(entry, authors_by_id) ++ Map("theories" -> topo_theories)
+
+ layout.write_content(Path.make(List("entries", name + ".md")), entry_json)
+
+ val entry_html = """dynamic"
+
+ layout.write_asset(Path.make(List("theories", name + ".html")), entry_html)
+ }
+
+
+ /* add dependencies */
+
+ progress.echo("Preparing dependencies...")
+
+ val afp_dependencies = AFP_Dependencies.afp_dependencies(Path.explode("$AFP"))
+ val dep_json = AFP_Dependencies.JSON.from_dependencies(afp_dependencies)
+
+ layout.write_data(Path.basic("dependencies.json"), dep_json)
+
+ val entries_dir = layout.content_dir + Path.basic("entries")
+ val dep_file = layout.data_dir + Path.basic("dependencies.json")
+ val dependencies_cmd = "from dependencies import *; add_dependencies(" +
+ commas_quote(List(entries_dir.implode, dep_file.implode)) + ")"
+ Python.run(dependencies_cmd).check
+
+
+ /* add related entries */
+
+ progress.echo("Preparing related entries...")
+
+ val related_cmd = "from related import *; add_related(" + quote(entries_dir.implode) + ")"
+ Python.run(related_cmd).check
+
+
+ /* add statistics */
+
+ progress.echo("Preparing statistics...")
+
+ val statistics_cmd = "from statistics import *; add_statistics(" +
+ commas_quote(
+ List(
+ Path.explode("$AFP_BASE").absolute.implode,
+ Path.explode("$AFP").absolute.implode,
+ layout.data_dir.implode)) +
+ ")"
+ Python.run(statistics_cmd).check
+ (layout.data_dir + Path.basic("statistics.html")).file.delete()
+
+
+ /* static */
+
+ progress.echo("Preparing static files")
+
+ layout.write_static()
+
+
+ /* hugo */
+
+ out_dir match {
+ case Some(out_dir) =>
+ progress.echo("Building site...")
+
+ Hugo.build(layout, out_dir).check
+
+ progress.echo("Finished building site")
+ case None =>
+ progress.echo("Finished sitegen preparation.")
+ }
+ }
+
+ val isabelle_tool = Isabelle_Tool("afp_site_gen", "generates afp website source", Scala_Project.here, args =>
+ {
+ var base_dir = Path.explode("$AFP_BASE")
+ var hugo_dir = base_dir + Path.make(List("web", "hugo"))
+ var out_dir: Option[Path] = None
+
+ val getopts = Getopts("""
+Usage: isabelle afp_site_gen [OPTIONS] HTML_DIR
+
+ Options are:
+ -B DIR afp base dir (default "$AFP_BASE")
+ -H DIR generated hugo project dir (default "$AFP_BASE/web/hugo")
+ -O DIR output dir (default none)
+
+ Generates the AFP website source. HTML files of entries are dynamically loaded.
+ Site will be built from generated source if output dir is specified.
+""",
+ "B:" -> (arg => base_dir = Path.explode(arg)),
+ "H:" -> (arg => hugo_dir = Path.explode(arg)),
+ "O:" -> (arg => out_dir = Some(Path.explode(arg))))
+
+ val html_dir = getopts(args) match {
+ case dir :: Nil => Path.explode(dir)
+ case _ => getopts.usage()
+ }
+
+ val afp_structure = AFP_Structure(base_dir)
+ val layout = Hugo.Layout(hugo_dir)
+ val progress = new Console_Progress()
+
+ afp_site_gen(html_dir = html_dir, out_dir = out_dir, layout = layout, afp_structure = afp_structure,
+ progress = 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,19 +1,20 @@
package afp
import isabelle._
import afp.migration._
class Admin_Tools extends Isabelle_Scala_Tools(
AFP_Migrate_Metadata.isabelle_tool,
AFP_Build_Python.isabelle_tool,
AFP_Build_Hugo.isabelle_tool,
)
class Tools extends Isabelle_Scala_Tools(
+ AFP_Site_Gen.isabelle_tool,
AFP_Build_Site.isabelle_tool,
AFP_Check_Roots.isabelle_tool,
AFP_Dependencies.isabelle_tool,
)
diff --git a/tools/hugo.scala b/tools/hugo.scala
--- a/tools/hugo.scala
+++ b/tools/hugo.scala
@@ -1,56 +1,62 @@
package afp
import isabelle._
object Hugo
{
val hugo_home = Isabelle_System.getenv("ISABELLE_HUGO")
val hugo_static = Path.explode("$AFP_BASE") + Path.make(List("admin", "site"))
- class Layout private(src_dir: Path, out_dir: Path)
+ class Layout private(private[Hugo] val src_dir: Path)
{
private def write(file: Path, content: String): Unit =
{
val path = src_dir + file
path.dir.file.mkdirs()
File.write(path, content)
}
val data_dir = src_dir + Path.basic("data")
def write_data(file: Path, content: JSON.T): Unit =
write(Path.basic("data") + file, isabelle.JSON.Format(content))
val content_dir = src_dir + Path.basic("content")
def write_content(file: Path, content: JSON.T): Unit =
write(Path.basic("content") + file, isabelle.JSON.Format(content))
def write_asset(file: Path, content: String): Unit =
write(Path.basic("assets") + file, content)
def write_static(): Unit =
{
for (name <- File.read_dir(hugo_static)) {
Isabelle_System.copy_dir(hugo_static + Path.basic(name), src_dir)
}
}
-
- def build(): Process_Result =
- {
- val exec = Path.explode(proper_string(hugo_home).getOrElse(error("No hugo component found"))) + Path.basic("hugo")
- Isabelle_System.bash(
- exec.implode + " -s " + quote(src_dir.implode) + " -d " + quote(out_dir.implode))
- }
}
object Layout
{
- private val web_dir = Path.explode("$AFP_BASE") + Path.basic("web")
+ def apply(src_dir: Path = Path.explode("$AFP_BASE") + Path.make(List("web", "hugo"))): Layout =
+ new Layout(src_dir.absolute)
+ }
- def apply(src_dir: Path = web_dir + Path.basic("hugo"), out_dir: Path = web_dir): Layout =
- new Layout(src_dir.absolute, out_dir.absolute)
+ private lazy val exec =
+ Path.explode(proper_string(hugo_home).getOrElse(error("No hugo component found"))) + Path.basic("hugo")
+
+ def build(layout: Layout, out_dir: Path = Path.explode("$AFP_BASE") + Path.basic("web")): Process_Result =
+ Isabelle_System.bash(exec.implode + " -s " + quote(layout.src_dir.implode) + " -d " + quote(out_dir.implode))
+
+ def watch(layout: Layout, out_dir: Path = Path.explode("$AFP_BASE") + Path.basic("web"),
+ progress: Progress = new Progress()): Process_Result =
+ {
+ Isabelle_System.bash(
+ exec.implode + " server -s " + quote(layout.src_dir.implode) + " -d " + quote(out_dir.implode),
+ progress_stdout = progress.echo,
+ progress_stderr = progress.echo_warning)
}
}
\ No newline at end of file