Generating documentation

The VS Code extension for IPL includes a built-in documentation creation system, which can be accessed via a dedicated VSCode command. Simply running the command Ipl:Generate Documentation on an IPL file will produce a document in HTML format containing detailed information on the various IPL entities defined in the model, including messages, enumeration types, and repeating groups. The documentation generation process is fully automatic by default, but it can optionally be customized via user-defined Markdown files specifying the desided structure and format of the generated documents.

The following sections explain how to generate documentation via the VS Code extension for IPL, and how to use Markdown files to customize the generation process.

To access the document generation functionality from VS Code, please make sure to

Documentation can be generated by opening an IPL file and invoking the VS Code command Ipl:Generate Documentation. Upon successfull completion, a documentation page in HTML format will be saved in the same location and with the same file name of the source IPL file. Note that this process will not succeed if

  • the IPL model contains errors, or
  • there is no internet connection, or
  • the user is not authenticated into their Imandra account

Authentication

The documentation generation command is only available to authenticated users. The IPL extension will guide the user through authentication if they have not logged in yet; however, a valid Imandra account and a working installation of the Imandra CLI are prerequisites.

If the VS Code command Ipl:Generate Documentation is invoked on an unauthenticated machine, the extension will instruct the user to log in:

Upon clicking “Proceed”, a login page will open in a new browser window. After successfully logging in, the browser page will show an authentication code, which must be copied and pasted into the following text box back in VS Code.

After entering the authentication code, the extension will ask to select the computing zone.

After this last step, the user will be authenticated and the IPL extension will proceed to generate documentation.

Formatting documentation with Markdown

By default, the IPL extension formats the output HTML file automatically, following a standard document structure that lists all messages, fields, enumeration types, and repeating groups defined in the IPL model. Documentation generated using this standard format is highly detailed and thus likely to be sufficient for most use cases, however it is possible to intruct the extension to use a custom format instead.

The IPL extension supports full customization of the documentation generation process via Markdown. This feature allows the user to provide a Markdown file with their own content and formatting, which will be used to render the final HTML documentation file. The extension supports a custom version of Markdown that allows to insert in-document references to IPL entities (like messages and enumeration types) that get automatically rendered into rich documentation for those entities. This enables the user to write content to the desired level of detail, leaving the generation of complex data-based lists and tables to IPL.

To use Markdown formatting to drive the documentation generation process, simply add a Markdown file in the same location of the IPL model. The Markdown file should have the same file name as the IPL file, but with .md extension.

When invoking the command Ipl:Generate Documentation, the extension will look for a matching Markdown file in the same location of the target IPL file and, if present, use it to render documentation.

See Markdown formatting for details on the Markdown syntax supported by the extension.

The Markdown format supported by the Ipl:Generate Documentation command is a subset of v0.30 of the CommonMark standard, augmented with special code blocks that can be used to insert references to various entities from the IPL model (such as messages and enumeration types) and automatically generate richly-formatted documentation for them. Thus, one can use Markdown formatting to manually specify the textual content and overall structure of the document, while leaving detailed technical documentation to the automated process.

Supported Markdown constructs

Headings are formatted as lines of text preceded by number signs (#). The amount of number signs denotes the heading level:

# Title
## Subtitle
### Subsubtitle

Paragraphs are written as normal blocks of text, and are separated by one or more blank lines.

This is
a paragraph.

This is another paragraph.

Text can be formatted as bold, italic, or monospaced:

This is __bold__ text.
This is _italic_ text.
This is `monospaced` text.

Code blocks are formatted as paragraphs surrounded by three backticks:

```
code
block
```

Items can be organised into lists:

* Item 1
* Item 2
* Item 3

Currently, only unordered lists are supported.

One can also organise data into tables:

| Header 1  | Header 2  |
|:----------|:----------|
| Cell 1    | Cell 2    |
| Cell 3    | Cell 4    |

The code block above produces the following table:

Header 1 Header 2
Cell 1 Cell 2
Cell 3 Cell 4

Labelled hyperlinks are inserted as follows:

Click [here](https://www.imandra.ai) for the homepage.

Heading metadata

Section headings can be tagged with metadata describing the specific IPL entity that they refer to. For example, given a heading for a section on ExecutionReport messages:

## ExecutionReport (8)

we can attach semantic IPL metadata with the following syntax:

## ExecutionReport (8){msg=ExecutionReport}

In general, heading metadata is attached with the following syntax, respectively for messages, enumeration types, and repeating groups:

## Some section title{msg=MessageName}
## Some section title{enum=EnumName}
## Some section title{rg=RepeatingGrouName}

Adding IPL metadata to section headings has two effects on the generated documentation. Firstly, it adds a jump-to-definition button/hyperlink next to the heading, which navigates to the source location of the referenced IPL entity. Secondly, it allows to add in-text references to those headings, in the form of hyperlinks that, when clicked, jump back to the corresponding section within the document. For example:

## Execution Report messages (8){msg=ExecutionReport} 

Click [here](msg=ExecutionReport) for more info on `ExecutionReport` messages.
Click [here](enum=OrdType) for more info on the `OrdType` enumeration type.
Click [here](rg=Parties) for more info on the `Parties` repeating group.

Note that

  • entities mentioned in the metadata must be valid IPL entities defined in the corresponding IPL model;
  • within a document there should be only one heading reference per IPL entity;
  • currently, jump-to-definition links are only supported for messages and enums;

When formatting IPL documentation in Markdown, one can leverage the reasoning and formatting capabilities of Imandra FIX Wizard via embedded queries. FIX wizard queries can be embedded in the markdown source as special code blocks featuring an additional “fixWizard” keyword:

```fixWizard
describe ExecutionReport messages
```

As a result of the process of rendering documentation from the Markdown file, fixWizard code blocks get replaced with the formatted output that FIX Wizard produces in response to the embedded query. The documentation fragments produced by FIX Wizard are Markdown-aware, thus any mentions of IPL entities contained in them will automatically feature hyperlinks to corresponding sections in the document, as long as the headings of those sections have been metadata-enriched as illustrated above.

fixWizard code blocks allow to embed any query, however some queries are better suited than others to be embedded in documentation, depending on the output they produce.

The following is a list of recommended FIX Wizard queries to use when editing documentation as Markdown:

  • Generate a table describing all fields of a given message, including tags, types and validations for each field:
(Query(Describe(Msg(Msg_of_name ExecutionReport))))
  • Generate a list of all validation statements for a given message:
(Query(Validations(Msg(Msg_of_name ExecutionReport))))
  • Print the textual description for a given message. This is sourced from the textual metadata in the IPL file:
(Query(Descriptions(Msg(Msg_of_name OrderCancelReject))))
  • Generate a table of all fields used in the spec, including, for each field, a list of messages using that field:
(Query (Fields All))
  • Print the textual description for a given enum type:
(Query(Descriptions(Enum CrossType)))
  • Generate a list of constructors for a given enum type:
(Query(Describe(Enum CrossType)))

In this example we want to generate documentation for the IPL model described in the advanced tutorial, which we assume is saved somewhere under filename tutorial.ipl. The fastest way to do this is to simply open the model in VS Code, and let the IPL extension generate the document automatically for us. The result of this process can be found here.

However, suppose we are not happy with the default documentation format produced by IPL, and want to edit our own version of the document that only mentions ExecutionReport messages, the enumeration type ExecType, and the repeating group Parties. We can easily do so by creating a Markdown file containing the desired markup:

# Custom documentation for the model 'Advanced Tutorial'

This is a stripped-down version of the 'Advanced Tutorial' model documentation,
that only contains information about [Execution Report](msg=ExecutionReport)
messages, [ExecType](enum=ExecType) enumeration types, and [Parties](rg=Parties)
repeating groups.

## Execution Report messages{msg=ExecutionReport}

These are the _fields_ of `ExecutionReport` messages:

```fixWizard
(Query(Describe(Msg(Msg_of_name ExecutionReport))))
```

These are the _validation statements_ of `ExecutionReport` messages:

```fixWizard
(Query(Validations(Msg(Msg_of_name ExecutionReport))))
```

## Execution type{enum=ExecType}

The type `ExecType` supports the following constructors:

```fixWizard
(Query(Describe(Enum ExecType)))
```

The underlying encoding is `char`. Fields of type `ExecType` as commonly used as
part of [`ExecutionReport`](msg=ExecutionReport) messages.

## Parties{rg=Parties}

The full list of fields of `Parties` repeating groups can be found below:

```fixWizard
(Query(Describe(Repeating_group Parties)))
```

After saving this Markdown code under filename tutorial.md, we can go back to the IPL model file tutorial.ipl and invoke the VS Code command Ipl:Generate Documentation, which results in the documentation shown here. Note that most of the Markdown content is prose, since the complex data rendering of lists and tables is offloaded to FIX Wizard via the fixWizard code blocks.