A document is specified by a text file where the first
line has the form:
Document theoryid
The HOHF theory (for all reward bounties) has id
6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d
so the first line for documents in this theory would be:
Document 6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d
The remaining lines are declarations of local base type names (via Base), local abbreviations (via Let), transparent definitions (via Def), opaque definitions (via Param), imported known propositions (via Known) and proven theorems (via Thm). More information on the assembly style format for this file can be found here.
The command readdraft can be used to check correctness of the file. Upon publication the publisher will be given ownership of new definitions and newly proven propositions. If the proposition (or its negation) has a bounty, then the new owner will be able to claim the bounty.
Once the file with the document is prepared for publication, the commands addnonce and addpublisher can be used to include a nonce (so the hash of the document gives no information about the document before it is published) and a Proofgold address for the publisher. The publisher can also optionally include information about rights for future users to be able to import opaque defitions and knowns. By default all users will have the right to make such imports.
The command commitdraft creates a transaction that will publish a marker that commits to the current version of the documents. The document itself can only be published after the commitment transaction has been sent and has 12 confirmations. If the document is modified after the commitment is published, a new commitment will need to be published.
After the commitment has 12 confirmations, the command publishdraft creates a publication transaction. This transaction will also assign the new ownership information (with corresponding policy on rights to future imports).
After the document has been published, the publisher may have ownership of propositions with bounties. The command collectbounties can be used to ccreate a transaction to collect all bounties possible.