Subject: FormalContent

Keywords: ::version
          ::implementation
          ::html
          ::theory

Title: Exporting theories to the Web

--------------------------------------------------

Closed theories are periodically exported to the web.

By default proofs are not exported.
To cause a proof to be exported add it to the list of objects in the 
".simple_projection_proofs" object in the theory group (eg "Standard" or "Standard2")
directory 

Currently, the process is not automated and so the period between exports
can sometimes be lengthy.


The following is still under-development:

The formal content in nuprl is updated frequently. The wip links will refer to the
latest content exported. On occasion a user would like to reference html content that
is not subject to change. For this reason Snapshots are periodically frozen. Such
a snapshot will have a link prefix like: 
"www.nuprl.org/LibrarySnaphosts/Published/Version1/group/theory/thm.html".
The latest version is a link to the wip. When a freeze occurs then current wip
is effectively copied and the version link is redirected to the copy.
Even though all content is subject to change, a fair amount does not change.
It might be sensible to attempt to share such stable content, however as the 
objects are so highly linked, a modification of an early object may cause a
significant proportion of the html pages to be updated. FTTB, when a version is frozen
an actual copy will be made.

Note to self: to find which objects had proofs exported irrespective of 
.simple_projection_proofs look at code standard_proof_urls_to_objects for example.
⋅
--------------------------------------------------

Authors: RICH:t

⋅

Home