Add CI job to validate Notes in source code
Motivation
The GHC source code is filled with notes, explaining a certain aspect of the compiler in detail, and references to these notes. While these are very helpful, it is a manual process, essentially without support by any tool. As such, it can happen that a code change leaves dangling references, and other infelicities. This proposal aims to provide a tool to validate the note references, in order to ensure that they point to existing notes.
As an additional benefit, this gives some guarantees to the format the notes are in, which makes it easier and more reliable to use custom tools to jump from a reference to the corresponding note.
Proposal
Roughly, a note has the following format:
Note [<note-name>]
~~~~~~~~~~~~~~~~~~
<note-body>
And a note reference can be either Note [<note-name>]
, or there can be multiple references with Notes [<note-name1>], [<note-name2>], and [<note-name3>]
(,
and and
are arbitrary separators, the script would accept any separator(s)).
Notes in other files or modules can also be referenced, with Note [<note-name>] in includes/example.h
or Note [<note-name>] in GHC.Example
.
With this proposal, a CI script is added to the compiler linting phase that reads in notes and note references from across the codebase, and then emits errors or warnings with the following severities:
- No errors or warnings
- There are notes that aren't referenced anywhere
- There are two notes with the same name in one file (same note name in different files is OK)
- There are dangling references
- There are malformed note headers or note references
- Catchall (likely incorrect usage of the script)
With the feature described in https://gitlab.com/gitlab-org/gitlab/-/issues/273157, the CI script could then be adjusted to configure what the highest acceptable severity is.
Implementation
There is an incomplete prototype implementation at !5839 (closed) .