Documentation Guidelines

In an effort to discuss and resolve any issues with documentation standards (or guidelines) for Idris. This wiki page serves as a place to document such ideas.

Documentation Markup

For documenting code many languages have a default markup: Haskell has Haddock, Java has Javadoc, Python has reST, /et cetera/. There are also language agnostic markups such as Doxygen. If a documentation system (to be named) is to be created for Idris what markup should be used for documenting code?

Section Documentation

For documenting sections of code, the following styles are seen within libs/.

• Should we adopt one of these styles out right as the 'preferred way'?
• Is there an alternative format that is better? For example: Haddock's * and Doxygen's \section

Style 1

--------------------------------------------------------------------------------
-- <name>
--------------------------------------------------------------------------------

Style 2

---- <name>

Style 3

-- ------------------------------------------------------------------ [ <name> ]

Alternative: first-class section structure

If these kinds of comments get syntactic meaning, then it might make more sense to simply add sections to Idris source. This would allow things like:

• Querying the compiler about the section structure of a source file - useful for editor support for navigation and code folding
• Reporting errors by their section location in addition to just line and column
• Understanding of structure by both source-focused and documentation-focused tools

Potential syntax:

%section Properties of Nat
%subsection Properties of addition

Alternatively, it is already possible to put things in namespaces, which can be inspected with :browse, and IDE-mode should already make this sort of thing possible then.

Module Documentation

For module documentation, Haskell uses the following Haddock format.

{- |
Module      :  <File name or $Header$ to be replaced automatically>
Description :  <optional short text displayed on contents page>
Copyright   :  (c) <Authors or Affiliations>
License     :  <license>

Maintainer  :  <email>
Stability   :  unstable | experimental | provisional | stable | frozen
Portability :  portable | non-portable (<reason>)

<module description starting at first column>
-}

• Is this something we want to adopt out right? What do Haskell users who know better say? Have we asked in #haskell?
• Is there an alternative format that is better?