September 2006

Current Status of "automatic" FDL content projection:

Rich has provided some test sets.
For current content see Entry Points

NOTES and PLANS:

When it's good enough this method will supplant those used to produce the Standard Projections.
Those older methods require too much effort by too few, making them unsuitable for larger scale and more timely projection of content.

There are two sets of Event Systems data used for this experiment one being the the latest stable version (taken from the FDL markb-s) and the other being more up-to-date but still under development, including a formalization of van Renesse and Schneider's Chain Replication Protocol.

Many postings omits proofs, just showing theorem statements instead, presumably justified by reference to the lemmas indicated on the page. (All these links were provided by the Web Projector by Rich Eaton.)
More proofs will be projected, as inference step trees or dags, as in the little testbed Agatha puzzle.

The conversion of the projector process into an automatic system with minimal human intervention is nearly realized.

The projector code needs to be improved to allow multiple projector processes to cooperate on a single projection (for faster projection using mulitple machines).

Notable Features

Generation of latex code for the content of each object and renderings in postscript and pdf.
See upper right and along the right side (example), -- we're experimenting with placement.
On the new pages were are linking to latex without ambles for formulas, and linking to postscript and pdf only for the whole page content.
The whole page as printable content is valuable not only for seeing what the latex code will produce in proper context, but it also compensates for the fact that the html for these pages tends to be bad and misleading when printed because of hacks used for indentation and alignment control.
Elaboration of definition pages to include a rendition exposing any components ordinarily elided. (example)
A short "version" indicator is now prominently placed on the title line of each page. It's a pair of numbers indicating content and presentation versions of a projection, and links to the origin page for the projection.
The point is to make it plain if one is looking at two similar pages that differ by coming from different projections, and which could, therefore, differ.

Suggestions for improvement as of September 2006

Here are a number of suggestions submitted via Email; the bold faced ones near the top are considered high-priority and pending.

On the page for a nuprl theorem statement, we should have links to the defs and primitives that are mentioned in the statement.
For example, it would be good to link to the defs of ES and E since they appear in the theorem statement.
Further, the defs for ops that occur in the statement should be obviously distinguished, perhaps grouping them together, since it's tedious to follow the meaning of the expressions when they're embedded in an excess of other ops, such as here.
Also, what is currently listed as defs should be renamed to "other defs mentioned in the proof".
Include statements of relevant well-formedness thms on definition pages.
On a definition page show the full underlying structure of the lhs, as though it were displayed with special display forms.
Link pages with declarations of primitives to online documentation. (Most already exists under Nuprl Basics.)
Wherever one links to definitions used in some way, such as mentioned in a theorem, also link to primitives used in that way.
We should have one page that has links to the standard logical operators (member, equal,and, cand, or, implies, rev_implies, iff, all, exists, prop, universe)
Then in lists of definitions mentioned in the proof, we should filter out any of the logical operators and replace them with one link to the "logic page". (example)
Notation for large iterated dependent product formulas should be improved. (example)
If practical, make the default display forms not break if the display will fit on a line. An example of unattractive breaking is the lhs of the clarification.
Add some kind of shopping-for-latex functionality to web pages to make it easier for an author to collect needed latex code. (Mark has some ideas about this, and Rich has implemented similar functions elsewhere.)
In a directory listing that points to another directory, attach to the pointer an indication of the number of non-directory objects that are below it (recursively).
Some keywords, or better, short glosses or content descriptions, should be attached to FDL objects that get web projected with their content suitable for Google searching for our content pages.
In order to help people know what to search (Google) for to find FDL pages of some kind, include on each page a list of keywords (say at the bottom) that would help find a similar page.

Earlier suggestions for improvement that have been incorporated in to the latest projections:

Include links to relevant well-formedness thms on definition pages.
Provide some kind of context link for each object (heuristic), so the reader can find "nearby" objects. Perhaps links to the nearest directories.

sfa