Feature: Modules Support

[liamoc]

Support for multi-document "books" and libraries is becoming necessary, but a number of design options present themselves.

• Book-style: Each document is a chapter in the book, and Chapters 1 through N-1 are implicitly imported by Chapter N. Simple to implement but not very flexible. Also heavily pollutes the namespace of later chapters and may cause performance issues if large-scale formalisations are conducted.
• Isabelle-style: Each module is in a flat namespace. Modules can be imported by other modules, but the import graph is always a DAG and the order of processing is linearised into topological order. The book table of contents is just an ordering on these modules, and doesn't have any impact on the import graph.
• More sophisticated options: First class or parameterised modules/locales, etc. This could be integrated with things like typeclasses etc. later too. However, this would stray the furthest from straightforward textbook-style presentation of material, and risks introducing concepts that are too Holbert-specific and would make Holbert materials too focused on Holbert as a tool rather than their intended subject matter.

Some technical considerations: Currently the set of available theorems and syntax declarations is taken just by taking the prefix of the current document before the current entry. Therefore changes to a theorem definition are just propagated to the suffix of the document after its definition (wiping invalidated proofs). To support very large developments, we'd have to extend this mechanism to traverse the entire import graph. This is potentially slow. I'm not sure what solution there is.

[sertel]

Dear Liam,

thanks for setting up this issue.

I really like your book-style idea. We could expand on that as follows to arrive at the DAG that you mentioned in your Isabelle-style approach:

For a book with a story the dependency graph for the chapter is of cause as you describe, i.e., one chapter depends on all previous chapters.

But for books that convey knowledge this must not be the case. Such books often do not only have a table of contents but also a page with an explicit dependency graph for the chapters. For example, Pierce's "Types and Programming Languages" (Preface, xvi) has. I like to have such a graph at the beginning of a book to focus my reading.

I feel like it could be nice to have such an explicit graph for Holbert developments too.

• Holbert itself gets a rather easy way of understanding the dependencies between chapters and guide the checker.
• The reader becomes a very good overview of the dependencies in the development.
• The developer does not have to clutter individual chapters with imports but rather specifies all dependencies in this one graph. (No more cycles.)
• (It is also a good starting point to optimize checking times as you mentioned to only the very minimal dependency subset.)

So for every development there would be

1. a table of contents listing a pre-defined order for the chapters
2. a dependency graph of the chapters
3. the individual chapters (holbert files)

Of course, later on a more visually fancy frontend could merge 1 and 2 into one view (where the chapters are connected on the right-hand side).

What do you think?