document extensible and additional in QL reference and spec

[ginsbach]

• This fixes https://github.com/github/codeql-core/issues/4843.

The first two commits are unrelated changes to fill in other missing references.

When incorporating extensible into the spec (commit 6), I essentially just did a textual search for external and made sure to always mention extensible alongside it as appropriate. That's when I noticed the mention of external on member predicates (commit 5). I'm unsure whether in the past we allowed external on member predicates, but as far as I can tell from looking at QLChecker, we don't allow it now.

Note that I have not added anything further in the language spec on additional. The reason is that the annotation doesn't do anything aside from affecting errors.

[Copilot]

Pull Request Overview

This PR documents the extensible and additional annotations in QL reference documentation and language specification to address a missing documentation issue. The changes ensure these annotations are properly explained alongside existing annotations like external.

• Added comprehensive documentation for extensible and additional annotations in the annotations reference
• Updated language specification to mention extensible alongside external in relevant contexts
• Added missing index entries and cross-references for signatures documentation

Reviewed Changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
docs/codeql/ql-language-reference/signatures.rst	Added index entries and section references for predicate, type, and module signatures
docs/codeql/ql-language-reference/ql-language-specification.rst	Updated specification to include extensible predicates alongside external predicates in evaluation context and body requirements
docs/codeql/ql-language-reference/annotations.rst	Added documentation for additional and extensible annotations, updated availability lists for other annotations, and added signature-related cross-references

[kaspersv]

What does directly in declarations directly inside of modules mean here? I assume it relates to nested modules.

Can't we simplify it to something along the lines of:

The `additional` annotation can be used on declarations in modules. All declarations in modules with |module signatures| that are not required by a module signature must be annotated with `additional`.

[ginsbach]

What does directly in declarations directly inside of modules mean here? I assume it relates to nested modules.

Yes.

What does directly in declarations directly inside of modules mean here? I assume it relates to nested modules.

Can't we simplify it to something along the lines of:

The `additional` annotation can be used on declarations in modules. All declarations in modules with |module signatures| that are not required by a module signature must be annotated with `additional`.

I've pushed another commit. I didn't take your wording directly, because I want to keep "modules that implement module signatures" rather than "modules with module signatures" to avoid ambiguity with modules that contain a module signature declaration.