Weeknotes 2025-W15 › Forester 5.0 development: canonical URLs, atom feeds, and LSP [01A0]

Work on Forester 5.0 proceeds apace, generously supported by ARIA who have engaged Kento Okura and myself on a consulting basis to support their internal use of Forester. My recent goals have been to bring Forester closer in line with the architecture of the World Wide Web; to that end, I have made two big improvements.

1. First cut at canonical URLs [01AA]

Trees are addressed by “canonical URLs” that are meant to be the place where they will ultimately be published. See my blog post on the design for more details. Canonical URLs are of the form https://www.my-host.net/tree-name/; the handling is a little fragile right now and you can expect bugs (but please write to me about them).

2. First cut at atom syndication [01AB]

It is now possible to syndicate the children of a tree as an Atom feed. This is done currently by including the following directive in the tree you wish to syndicate:

\syndicate-current-tree-as-atom-feed

Then, if your tree is located at https://www.my-host.net/tree-name/, you will find that there is an atom feed at https://www.my-host.net/tree-name/atom.xml. There are many subtleties to this, and the atom support will continue to evolve and improve. One thing I need to deal with is the fact that Forester produces nested hyperlinks—which are not valid in HTML! I came up with a pretty slick way to handle this in XSLT, but that Atom renderer is intended to bypass that entirely.

As a side note, I am very happy to see that I am not the only person using the new support for Atom feeds. Patrick’s fork of Forester is looking pretty cool, and I am excited to learn more from what he is doing. I’m also relieved that he was able to get rebased atop the ever-changing forester-5.0-dev branch.

3. Federation is still janky [01AC]

One thing I want to start designing soon is how best to handle federated forests. Right now, Forester bundles all the imported material under a foreign/my-friends-host/ directory and routes all links accordingly, but in many (but not all!) cases one would want to not bundle things at all and instead have links routed directly to the canonical URLs as published on the World Wide Web. I am not sure of the best design for this, so I welcome feedback. In the meanwhile, enjoy the janky prototype feel.

4. Language server; code completion via effects and handlers [01A9]

Kento is hard at work hardening Forester’s language server. I am hoping that we will have something to show on the scale of a week.

There were some subtleties about how to provide completion information at a source location—which is at least as complex as the expander itself, since scope emerges from the expansion process. We had something fairly broken in place, which I have spent Thursday and Friday morning replacing with something cool using OCaml 5’s effects and handlers. The idea is to instrument the expander with an effect that notifies observes that it has entered a source range; this can be handled as a no-op, or by querying the scope’s available symbols when it enters the desired range and throwing away the continuation, and resuming the continuation otherwise to keep searching. This approach allows all the scope-handling code to be unified into a single routine, whose behaviour is controlled by effect handlers on the outside.

As a side note, I am looking forward to when the next version of Topiary is released, which should contain support for formatting OCaml’s effect handlers. Right now we don’t use the nice notation because we are stuck on Topiary 0.6.0.

Context

    Weeknotes 2025-W15 [2025-W15]

    I have a lot to say this week, so strap in.

    Forester 5.0 development: canonical URLs, atom feeds, and LSP [01A0]

    Work on Forester 5.0 proceeds apace, generously supported by ARIA who have engaged Kento Okura and myself on a consulting basis to support their internal use of Forester. My recent goals have been to bring Forester closer in line with the architecture of the World Wide Web; to that end, I have made two big improvements.

    First cut at canonical URLs [01AA]

    Trees are addressed by “canonical URLs” that are meant to be the place where they will ultimately be published. See my blog post on the design for more details. Canonical URLs are of the form https://www.my-host.net/tree-name/; the handling is a little fragile right now and you can expect bugs (but please write to me about them).

    First cut at atom syndication [01AB]

    It is now possible to syndicate the children of a tree as an Atom feed. This is done currently by including the following directive in the tree you wish to syndicate:

    \syndicate-current-tree-as-atom-feed

    Then, if your tree is located at https://www.my-host.net/tree-name/, you will find that there is an atom feed at https://www.my-host.net/tree-name/atom.xml. There are many subtleties to this, and the atom support will continue to evolve and improve. One thing I need to deal with is the fact that Forester produces nested hyperlinks—which are not valid in HTML! I came up with a pretty slick way to handle this in XSLT, but that Atom renderer is intended to bypass that entirely.

    As a side note, I am very happy to see that I am not the only person using the new support for Atom feeds. Patrick’s fork of Forester is looking pretty cool, and I am excited to learn more from what he is doing. I’m also relieved that he was able to get rebased atop the ever-changing forester-5.0-dev branch.

    Federation is still janky [01AC]

    One thing I want to start designing soon is how best to handle federated forests. Right now, Forester bundles all the imported material under a foreign/my-friends-host/ directory and routes all links accordingly, but in many (but not all!) cases one would want to not bundle things at all and instead have links routed directly to the canonical URLs as published on the World Wide Web. I am not sure of the best design for this, so I welcome feedback. In the meanwhile, enjoy the janky prototype feel.

    Language server; code completion via effects and handlers [01A9]

    Kento is hard at work hardening Forester’s language server. I am hoping that we will have something to show on the scale of a week.

    There were some subtleties about how to provide completion information at a source location—which is at least as complex as the expander itself, since scope emerges from the expansion process. We had something fairly broken in place, which I have spent Thursday and Friday morning replacing with something cool using OCaml 5’s effects and handlers. The idea is to instrument the expander with an effect that notifies observes that it has entered a source range; this can be handled as a no-op, or by querying the scope’s available symbols when it enters the desired range and throwing away the continuation, and resuming the continuation otherwise to keep searching. This approach allows all the scope-handling code to be unified into a single routine, whose behaviour is controlled by effect handlers on the outside.

    As a side note, I am looking forward to when the next version of Topiary is released, which should contain support for formatting OCaml’s effect handlers. Right now we don’t use the nice notation because we are stuck on Topiary 0.6.0.

    Project Pterodactyl: yes, I’m building a new proof assistant [01A1]

    I swore after building cooltt, redtt, and RedPRL that I would never build another proof assistant, as the experience burned around four years of my PhD and resulted (at least directly) in very little publishable work—but, to be fair, I probably would not have made the key mathematical discovery of my PhD thesis if it were not for these engineering experiments. But I’m back on my bullshit, as the young people say, and hard at work building a new interactive proof assistant that I have code-named Project Pterodactyl.

    Locales in dependent type theory? [01A2]

    The goal of Pterodactyl is to explore the adaptation of locales from Isabelle to dependent type theory, as a lightweight but extremely expressive alternative to type classes. My colleague Larry Paulson has written some great blog posts about locales in Isabelle, and I strongly recommend reading Ballarin’s Exploring the Structure of an Algebra Text with Locales to get a feel for what is possible. Here is what locales do:

    1. Locales appear to completely solve the pain involved when building up hierarchies of mathematical structures and notations, allowing you to effortlessly combine theories along a common core (e.g. defining rings in terms of a multiplicative monoid and an Abelian group sharing the same carrier).
    2. Locales allow you to add new methods to a theory after the fact, and they will magically be available on anything that extended that theory. You can also add new links in the theory graph, and both cycles and diamonds are allowed so long as they are coherent; this is useful if you want to silently regard (e.g.) the space of endomaps on a set as a monoid, etc.

    In comparison to modules and type classes, the strength of locales is that you don’t have to decide ahead of time whether you want to “bundle” fields with their carriers, etc. In contrast, a great deal of the difficult work of mathematical library design and maintainance in tools like Rocq, Agda, and Lean is figuring out just what things to bundle, and fixing things when your choices inevitably lead to breakage, etc. Locales avoid these problems entirely.

    Finally, a reasonably usable locale implementation can be obtained without any higher-order unification whatsoever. I have a feeling that will be extremely important, given how unreliable (and incorrect!) most implementations of higher-order unification are; the situation is so bad that it is actually an open problem to define a correct higher-order unification algorithm in the presence of singleton types (such as the unit type). I do think that this can be solved (and may have already been solved by András Kovács), but my point is that the prognosis for unification in dependent type theory is bad.

    Experimental implementation in Lean [01A3]

    The other interesting thing about Pterodactyl is that I am implementing it in Lean; I am not verifying anything, and am making free use of Lean’s partial keyword (which hides potentially divergent code from definitional equality). Instead, I am thinking of Lean as a “better OCaml”: I can’t speak to the quality of the compiler and code generator, but I can absolutely say that from the perspective of day-to-day programming, Lean has a lot of affordances that make it extremely nice to use. On the other hand, Lean’s story for modularity is not so good; but I hope they don’t “fix” it any time soon, because I think that something like locales could be a good option for Lean itself in the future if I am able to demonstrate their potential in the context of Pterodactyl’s clean-room implementation.

    A taste of code [01A4]

    I will have more to say about Pterodactyl in the future, but let me leave you with a bit of demo code.

    locale Magma { A =>
  car : Type,
  car.isSet : isSet A·car,
  cmp : (x y : A·car) → A·car
}

locale Magma.Hom { f =>
  dom : Magma,
  cod : Magma,
  car : (x : f·dom·car) → f·cod·car,
  cmp : (x y : f·dom·car) → Id f·cod·car (f·car (f·dom·cmp x y)) (f·cod·cmp (f·car x) (f·car y))
}

locale Semigroup { A =>
  splice magma : Magma,
  cmp.assoc : (x y z : A·car) → Id A·car (A·cmp (A·cmp x y) z) (A·cmp x (A·cmp y z))
}

locale Semigroup.Hom {f =>
  dom : Semigroup,
  cod : Semigroup,
  splice magma.hom : Magma.Hom / {dom := f·dom·magma, cod := f·cod·magma}
}

locale Monoid { A =>
  splice semigroup : Semigroup,
  unit : A·car,
  cmp.leftUnit : (x : A·car) → Id A·car (A·cmp A·unit x) x,
  cmp.rightUnit : (x : A·car) → Id A·car (A·cmp x A·unit) x
}

locale Monoid.Hom {f =>
  dom : Monoid,
  cod : Monoid,
  splice semigroup.hom : Semigroup.Hom / {dom := f·dom·semigroup, cod := f·cod·semigroup},
  unit : Id f·cod·car (f·car f·dom·unit) f·cod·unit
}

locale Group { G =>
  splice monoid : Monoid,
  inv : (x : G·car) → G·car,
  inv.inv : (x : G·car) → Id G·car (G·inv (G·inv x)) x
}

locale AbelianGroup { A =>
  splice group : Group,
  splice commutativeOperation : CommutativeOperation / {car := A·car, cmp := A·cmp}
}

    Two papers to appear in LICS ’25 [01A5]

    This week I have had two papers accepted at LICS ’25; I’m excited about both of them.

    With Leoni Pugh: When is the partial map classifier a Sierpiński cone? [01A6]

    Leoni Pugh is my old Part III student from 2023–2024, and this work builds on her Part III dissertation. The goal of our paper was to better understand the relationship between two approaches to partial functions in denotational semantics:

    1. “Geometrical” partiality / “the Sierpiński cone”: freely add a lowest element to the space representing a given data type. This is useful for defining functions whose inputs are partially defined, because you can do a case-analysis on the definedness of the input.
    2. “Logical” partiality / “the partial map classifier”: representing partially defined elements of a space X by pairs ( p,x ) where p is a proposition and x is a function from isTrue ( p ) to X. This is useful for defining functions whose outputs are partially defined.

    In traditional domain theory as developed by Scott, the two kinds of partiality coincide—even constructively. I am, however, interested in synthetic domain theory which abstracts away from continuity and limits and lets you just use sets and functions rather than cpos and continuous functions—provided that you avoid non-constructive principles like the Axiom of Choice or the Law of Excluded Middle. The starting point of our work is my observation that the two notions cannot coincide absolutely in synthetic domain theory, but that there may be restricted subuniverses in which they do coincide. The main result of our paper is to define such a subuniverse, made possible by my discovery of the based Segal condition—a strengthening of the usual Segal condition for higher categories.

    A broader motivation of this work is to develop synthetic domain theory and synthetic higher category theory within the same framework. Whereas synthetic domain theory traditionally concerned itself with spaces that behaved like ω-complete partial orders (but where all functions are automatically monotone and continuous), the same ideas (if applied within homotopy type theory) allow you to consider spaces that behave like ∞-categories with colimits of ω-chains (but where all functions are automatically ∞-functorial and ω-continuous). I believe that unifying domain theory and higher category theory will prove useful for studying things like the denotational semantics of concurrency, which is inherently higher-dimensional.

    With Andrew Slattery: Hofmann–Streicher lifting of fibred categories [01A7]

    This year, Thomas Streicher (born 1958) passed away from cancer. Thomas was one of the Greats of dependent type theory and he also wrote an excellent textbook on domain theory for denotational semantics, but much more importantly he was kind and curious and patient and always made time for young people. While I was still finding my place in the community, Thomas was very generous to me with his time and advice, and he sent me many papers to referee.

    Although Thomas made many contributions to dependent type theory, domain theory, realisability theory, and category theory, he is most known to type theorists for two things—both in collaboration with the late Martin Hofmann: the groupoid interpretation of type theory and the eponymous Hofmann–Streicher universe lifting construction. Andrew and my paper pertains to the latter.

    The idea of Hofmann–Streicher lifting has to do with universes, which are “types of types” (typically defined in such a way as to avoid paradoxes). Martin-Löf type theory usually includes universes in order to be able to quantify over (small enough) types; in the simplest models of Martin-Löf type theory, types are interpreted as sets and so Martin-Löf’s universes are interpreted as certain sets of sets, such as Grothendieck universes. But it is important to be able to interpret the language of type theory in more sophisticated worlds than set theory: for example, in presheaves (which are functors from a fixed category C into Set). What Hofmann and Streicher did is show how to transform any universe of sets into a universe of presheaves!

    Although Hofmann and Streicher’s construction worked well and had good properties, they did not find a universal property for it—which is an abstract description of the object that determines it uniquely up to isomorphism, usually in terms of how it relates to other objects. Recently Awodey found a 1-dimensional universal property, which was the starting point of our work. What Andrew and I wanted to do is generalise Awodey’s analysis in two directions:

    1. We wanted a 2-dimensional version, which is useful because it captures more about the universe than can be said in just one dimension: for example, with a 2-dimensional version, you can see immediately (by “abstract nonsense”) that Hofmann–Streicher lifting preserves structures like monads, adjunctions, etc. that might be used for modelling computational effects, etc.
    2. We wanted a relative version, which would make it easier to iterate the Hofmann–Streicher lifting construction: the purpose of this is to be able to define presheaf models of type theory internal to other presheaf models. These kind of situations actually happen in practice! For example, the model of guarded cubical type theory that combines step-indexing with univalence ought to be an example of this.

    To develop this two-fold generalisation of Hofmann–Streicher lifting, we resituated the theory in terms of another of Thomas’s favourite topics: the theory of fibrations, on which Thomas had written the most wonderful lecture notes.

    We dedicated our paper to Thomas’s memory. May he rest in peace.

    Reading corner: The Fountains of Paradise [01A8]

    I recently read Arthur C. Clarke’s The Fountains of Paradise; although it was a pretty good read, I found that like many science fiction books of that era, one has to look past a lot in order to enjoy it. I wrote some commentary in my post entitled Ventriloquy of the Mid-Century Man on my culture blog The Jon Sterling Review of Books.

    Related

      Prerelease. Forester 5.0 [https://www.forester-notes.org/011P/]

      This is a major release of Forester that includes many changes under the hood, as well as breaking changes that will require manual adjustments to existing forests. We are sorry for the frustration that these changes may cause to existing users, but we strongly believe that this is necessary for Forester to reach its potential as a tool that enhances rather than replaces the World Wide Web; we also strongly believe that these changes will make Forester more useful for existing users as well as the next thousand users.

      Our thanks to Owen Lynch, davidad, and Anil Madhavapeddy for conversations leading to the design of this release. We are grateful to ARIA’s Safeguarded AI initiative for helping us get to 5.0.

      Many of the changes included here are meant to support the future of Forester as an authoring tool for a new kind of Internet of Science that will enable the federation of many different forests by extending existing protocols with new hypermedia controls for content transclusion applicable to scientific authoring.

      Tl;dr: migration guide [https://www.forester-notes.org/0126/]

      To migrate your forest to Forester 5.0, do the following:

      1. Update your configuration file (§ [https://www.forester-notes.org/0125/]).
      2. Remove all usage of \transclude/title and \transclude/taxon (see § [https://www.forester-notes.org/011T/]).
      3. Move all \import declarations to the top-level of any .tree files, as these can no longer occur in subtrees (see § [https://www.forester-notes.org/OYOU/]).
      4. Any \author or \contributor attributions must take a tree address as their argument; when you wish to attribute a resource to a person who is not represented by a tree, you can use \author/literal{Somebody’s Name} or \contributor/literal{Somebody’s Name} (see § [https://www.forester-notes.org/012N/]).
      5. Rewrite any queries to use the new datalog engine (see § [https://www.forester-notes.org/013A/]), as the legacy query engine has been removed.
      6. Take into account the renaming of several built-in relations (see § [https://www.forester-notes.org/013C/]).
      7. View your forest locally using an HTTP server rather than directly through the file system (see § [https://www.forester-notes.org/VNQ8/]).
      8. Begin dialing back your use of custom XML stylesheets (see § [https://www.forester-notes.org/0127/]). It is possible that support for customisation at this level will be removed in a future release; if you have innovative customisations that are very important for your use of Forester, consider discussing them on the mailing list so that maintainers can better understand the problems you are solving.

      An implementation of the language server protocol [https://www.forester-notes.org/0SOW/]

      Forester now ships with an implementation of the language server protocol. See our documentation for more information and configuration examples for various editors. Its status is still experimental. If you encounter crashes or other issues, please let the us know by opening an issue or by writing to the mailing list

      Changes to forest.toml format [https://www.forester-notes.org/0125/]

      Several changes have been made to the forest.toml configuration format.

      1. forest.root is renamed to forest.home.
      2. The forest.theme key has been removed; from now on, your theme must be located in the theme directory.
      3. A new field forest.foreign has been added; this is the entry-point for the experimental forest syndication feature discussed in § [https://www.forester-notes.org/30FN/].

      Canonical URLs for tree addresses [https://www.forester-notes.org/011Q/]

      Up until this release, Forester’s trees were addressed by short strings — which, by convention, might be of the form xxx-NNNN or NNNN or some arbitrary string like sterling-2021-thesis. In order to prepare for the future in which multiple forests can be glued together, we replace Forester’s short names with fully qualified URLs that point to the location on the World Wide Web where a given tree would be published (if you choose to publish it). By default, all local trees will be resolved against http://forest.local/, which you should change if you choose to publish your forest on the Web. In your forest.toml configuration, first set a base URL for your forest like the following:

      [forest]
url = "https://www.forester-notes.com/"

      Within this forest, a tree named foo is then associated to the canonical URL https://www.forester-notes.com/foo/. Forester’s renderer will produce the correct directory structure so that if you were to upload the contents of the output directory to https://www.forester-notes.com/, a link to https://www.forester-notes.com/foo/ would bring you to the foo tree.

      Hyperlinks in Forester source code to trees within your own forest will automatically expand the short name foo to the canonical URL https://www.forester-notes.com/foo/. Canonical URLs are used as vertices in the graph.

      What do we mean by “URL”? [https://www.forester-notes.org/011R/]

      Today, “URLs” are a mostly implementation-defined concept that can only be understood by looking at the source code of major web browsers; in the future, this may congeal into an actual standard but today is not that day (nor is tomorrow, if the state of the whatwg/url “living” [non-]standard is any indication). It is best to think of Forester’s approach to URLs as provisional and subject to evolution as the Web continues to mature.

      Simplifications to the source language [https://www.forester-notes.org/OYOT/]

      Removal of imports within subtrees [https://www.forester-notes.org/OYOU/]

      It is no longer permitted to have an \import declaration within a subtree: these can occur only at the top level of a file and therefore have file-level scope.

      Removing transclusion overrides [https://www.forester-notes.org/011T/]

      In prior versions of Forester, it was possible to override the title and the taxon of a transcluded tree using the fluid bindings \transclude/title and \transclude/taxon respectively. This feature is no longer supported in Forester 5.0, and existing users are encouraged to purge their use of it prior to upgrading to Forester 5.0.

      In short, supporting this feature was greatly complicating the planned transition to a genuine hypermedia format; it could also be argued that it might have led to scenarios where an original author’s intentions are violated at the transclusion site.

      Please note that transclusion options, such as \transclude/expanded, etc., are still supported.

      Removal of autocapitalisation [https://www.forester-notes.org/OYOV/]

      Titles and taxa will no longer be autocapitalised: this feature biases Forester toward specific languages and is annoyingly complex to maintain. Therefore, you must rename all your titles and taxa to be capitalised by hand. This can be done in VS Code using the following regexp: replace \\taxon\{([a-z]) with \\taxon{\U$1, etc.

      Changes to attribution links [https://www.forester-notes.org/012N/]

      In prior versions, the \author and \contributor command would detect whether its contents were the address of a tree; if so, it would create a wikilink to the tree and otherwise, the included text would appear directly. This feature was convenient for smoothly handling the case that an author of a given resource is not represented in the forest by a biographical tree; the downside is that it makes the assumption that at compiletime we shall know the entire contents of the forest (and, thus, whether a given address shall be bound to a tree).

      To simplify the handling of author links and make it compatible with the open-world future of Forester, the behaviour is changed as follows:

      1. The argument to \author and \author must be a (possibly relative) Forester URL. Thus, on my own forest, it would be OK to have either \author{jeanbénabou} or \author{https://www.jonmsterling.com/jeanbénabou} but it would not be OK to have \author{Jean Bénabou}.
      2. To make an unlinked attribution containing, use \author/literal{Jean Bénabou}.

      New datalog-based query engine [https://www.forester-notes.org/013A/]

      As the query engine has evolved, it has become a bit unwieldy and misshapen. In order to prevent further churn and facilitate the long-term development and use of Forester, we are replacing the query engine and graph analysis with a more general tool: datalog. With this change comes the ability to introduce arbitrary relations of any arity; this is a powerful and dangerous tool, so use it wisely.

      On performance trade-offs [https://www.forester-notes.org/013B/]

      Switching to datalog makes forests that make heavy use of queries a bit slower to render. We considered this trade-off carefully, but believe that for the long-term health of Forester, this is acceptable. In the near future, Forester will render trees on demand rather than all at once (except when you are preparing a static archive for upload/deployment); in this mode of use, Forester will be faster than ever.

      Renamed built-in relations [https://www.forester-notes.org/013C/]

      Forester’s built-in binary relations have been accessible via macros like \rel/authors, etc. In this release, these relations are being renamed to make them more pleasant and consistent to use with datalog.

      Old name New name
      \rel/tags \rel/has-tag
      \rel/taxa \rel/has-taxon
      \rel/authors \rel/has-author
      \rel/contributors \rel/has-direct-contributor
      \rel/transclusion \rel/transcludes
      \rel/links \rel/links-to

      New built-in relations [https://www.forester-notes.org/013D/]

      A few new built-in relations have been added.

      • \rel/is-node ?X is a unary relation that holds for any tree address ?X. This is needed when specifying reflexive binary relations: the clause R ?X ?X -: is not allowed by datalog, so one must use R ?X ?X -: {\rel/is-node X}.
      • \rel/transcludes/transitive-closure is the transitive closure of \rel/transcludes.
      • \rel/transcludes/reflexive-transitive-closure is the reflexive transitive closure of \rel/transcludes.
      • \rel/is-reference ?X holds when ?X is designated as a reference/bibliographical tree. Currently, the built-in rules of the database deduce \rel/is-reference ?X for any tree ?X with taxon reference. The purpose of abstracting from the taxon is to enable non-English users of Forester to benefit from the computation of bibliographies.
      • Similarly, \rel/is-person ?X holds when ?X is designated as a personal/biographical tree. Currently, the built-in rules of the database deduce \rel/is-reference ?X for any tree ?X with taxon person.
      • \rel/in-bundle-closure ?X ?Y is the reflexive transitive closure of the union of the transclusion relation with the relation of ?X requiring the asset ?Y. The purpose of this relation is to easily bundle up fragments of a forest (see § [https://www.forester-notes.org/30FN/]).

      All of these built-in relations can be defined in Forester’s dialect of datalog; they are predefined for convenience, and because they are used in the computation of backmatter.

      Example. An example datalog query [https://www.forester-notes.org/013E/]

      In order to illustrate the use of the datalog engine, I will show how to construct a query that will find all the trees with taxon reference written by jonmsterling that are tagged either accepted or refereed. The first thing we must do is define the smallest relation containing all trees tagged accepted or refereed; this is done by adding clauses to the database as follows.

      First we define the name of a relation. In the current release, relations are global strings and there is no facility to generate a “fresh” one; that may change in the future.

      \let\rel/accepted-or-refereed{jonmsterling.query.bibliography.accepted-or-refereed}

      Next, we add two defining clauses for our relation. In what follows, \datalog simply delimits content that should be parsed as a datalog expression, and \execute instructs Forester to execute the datalog expression.

      \execute\datalog{
 \rel/accepted-or-refereed ?X -: {\rel/has-tag ?X '{refereed}}
}

\execute\datalog{
 \rel/accepted-or-refereed ?X -: {\rel/has-tag ?X '{accepted}}
}

      The left-hand side of the reversed turnstile -: is a proposition representing the goal; the right hand side is given by propositions representing the premises, each surrounded in braces and separated by whitespace. Metavariables are written with a question mark sigil. Literal content is embedded into a datalog proposition by surrounding it in '{...}; we will see that literal content is one kind of vertex in the graph database.

      Now that we have actually defined the relation that we will use, we can run a query:

      \query\datalog{
 ?X -:
   {\rel/has-author ?X @{jonmsterling}}
   {\rel/is-reference ?X}
   {\rel/accepted-or-refereed ?X}
 }

      The structure of a query identifies the metavariable being solved behind the turnstile, and then lists the clauses that must hold. Whereas a content vertex is addressed via '{...}, a URL vertex is addressed using @{...}.

      Atom syndication support [https://www.forester-notes.org/30FO/]

      It is now possible to syndicate a given tree as an Atom feed; for example, if you have a tree for your blog and its subtrees/transclusions are your blog posts, you can include the following code to generate an Atom feed for this blog:

      \syndicate-current-tree-as-atom-feed

      If your blog is located at https://www.my-great-forest.net/my-blog/, then there will be an atom feed placed at https://www.my-great-forest.net/my-blog/atom.xml.

      This feature is experimental and has some limitations.

      Publishing and implanting forests [https://www.forester-notes.org/30FN/]

      Forester now includes an experimental feature to “publish” a portion of your forest to a JSON blob that can be read by Forester and implanted into another forest. For example, if you include the following code in a tree within your forest, then a file will be emitted at output/my-forest.json containing the compiled content of your entire forest, together with all the assets:

      \syndicate-query-as-json-blob{my-forest}{
 \datalog{
  ?X -: {\rel/in-host ?X '{www.my-great-forest.net}}
 }
}

      Of course, more sophisticated queries can be used. For example, you can emit all the items tagged public together as follows:

      \syndicate-query-as-json-blob{my-public-forest}{
 \datalog{
   ?X -: {\rel/has-tag ?Z '{public}}
 }
}

      To implant the resulting JSON file into another forest, simply copy over the file and add the following line to your configuration file:

      [forest]
foreign = [{ path = "my-public-forest.json" }]

      By default, implanted trees will be rendered to your output folder underneath a foreign/ directory; if you wish to instead that links to implanted trees be routed directly to their canonical URLs (which will likely be the case if you implant a public forest), then you may configure that as follows:

      [forest]
foreign = [{ path = "my-public-forest.json", route_locally = false }]

      This feature is highly experimental and has many limitations; it will change in breaking ways in the near future. Although we are very interested to learn about the limitations of this feature, we will be taking a hands-off approach to support until the feature has taken a more stable form.

      Changes to how forests are viewed locally and deployed [https://www.forester-notes.org/VNQ8/]

      In the past, Forester’s XML output used relative URLs for all links. This was tractable because the output had no directory structure, but this is increasingly becoming problematic—for example, foreign trees are going to be rendered to a subdirectory, but this breaks all the relative URLs. I have come to the conclusion that the only way forward is to use absolute URLs for everything, but this assumes that the output is being served from the root directory of some host. As a result, users must fire up an HTTP server in order to view their forest locally. With this release we will (TODO) include a built-in HTTP server, but early adopters can simply run python3 -m http.server 8000 from the output directory and open localhost:8000 in their browser.

      Some users may wish to deploy their forest somewhere other than the root directory of a given (sub)domain. To achieve this and have all your links work correctly, enter the following configuration:

      [forest]
url = "https://www.my-great-website.net/my-subfolder/"

      Changes to handling of assets [https://www.forester-notes.org/P9BN/]

      Assets in compiled forests are content-addressed by their hash; a new primitive \route-asset is provided for generating the correct URL of an asset that is stored in a designated assets directory. For example, to embed an image that is stored in assets/images/my-great-illustration.jpg, you would write the following code:

      \xmlns:html{http://www.w3.org/1999/xhtml}
\<html:img>[src]{\route-asset{assets/images/my-great-illustration.jpg}}{}

      The future of Forester’s XML format [https://www.forester-notes.org/0127/]

      Forester currently emits archival-quality output in a custom XML format that is then interpreted using an XSLT stylesheet (as part of the “theme”). This format has served us well, enabling users to customise the presentation of their forests to a great degree. An added benefit of the XML format is to be able to easily convert a tree to LaTeX using another stylesheet.

      However, the constantly changing XML format has been an equally frustrating source of churn for users of Forester, and I have for some time now been warning users who customise their theme that these customisations are technically possible but not supported (i.e. we make no promise not to break them).

      The time is coming when Forester’s interaction model and output format will be changed drastically; rest assured that the core principles behind Forester (including the ability to generate static archival output that can be hosted anywhere) will be retained. We aim to become a better citizen of the World Wide Web by moving toward a more standard hypermedia format.

      One possiblity is to extend HTML with just the hypermedia controls and embedded microformats needed for Forester’s operation. This re-coupling of presentation and data would, paradoxically, facilitate Forester to evolve more rapidly over time while simultaneously increasing the longevity of forests that have been compiled using older versions of the tool.

      Institution. Advanced Research + Invention Agency [00XB]

      Person. Kento Okura [kentookura]