Documenting Juvix programs with Judoc

If you want to share your Juvix code with others, or even for your own sake, it is important that you properly document your code. Juvix has a builtin simple documentation language called Judoc that you can use to write documentation for your modules, types, and functions. Also, you'll be able to export the documentation in a beautiful html format.

Let's look at an example:

--- This is a well documented module
module howto.judoc.Main;

--- ;Maybe; represents an optional value.
type Maybe (A : Type) :=
  | --- The value is missing
    nothing
  | --- The value is here
    just A;

--- Retrieves a value from a ;Maybe; or returns the default value if missing.
fromMaybe {A} (default : A) (maybeValue : Maybe A) : A :=
  case maybeValue of
    | nothing := default
    | just value := value;

As you can see, when we want to write Judoc comments, we write three dashes ---.

We can write Juvix expressions inside Judoc comments too. We do so by delimiting them with ;. Then, the Juvix code inside will be properly scoped and highlighted. Remember that only things that are in scope can be referenced.

For more information about the syntax of the Judoc markup language, you can refer to its reference.

Generating html

As mentioned before, we can generate html documentation by running the following command:

juvix html Main.juvix --open

This command will typecheck the Main.juvix module and all of its dependencies. Then it will generate pretty documentation with links that looks like this. Note that you can jump to the source of each of the definitions.

For more information about the available options, type juvix html --help.

Comments