Repository navigation
Conversation
|
We might want to discuss whether we want to introduce this library https://github.com/dnault/therapi-runtime-javadoc Which brings annotations and an annotation processor that writes annotations capturing the Javadoc to |
wadoon
added
Documentation
c868aae to
c23e0d6
Compare
c23e0d6 to
1ad9db8
Compare
373f1ed to
bbdd443
Compare
unp1
left a comment
unp1
left a comment
There was a problem hiding this comment.
Thanks! Concerning the failing WD test, that constructor for ConstantCondition takes a JAbstractSortedOperator which is not a parseable variable.
(also "\reference" does not take a variable)
2e7edc3 to
7fa9eb6
Compare
7fa9eb6 to
981dedd
Compare
wadoon
changed the title
|
Current version:
|
1f9fc2e to
c94ff2d
Compare
| .replace("<li>", "* ") | ||
| .replace("</li>", "") | ||
| .replace("{@link", "`") | ||
| .replace("}", "`") |
There was a problem hiding this comment.
This seems a bit radical. What about curly braces in {@code ...}?
And {@link ...} should be ideally translated to [...].
There was a problem hiding this comment.
I also have the heavyweight code of Javadoc parsing, but do you think we should go this here. Or just postpone this to the consumers of the documentation?
import java.io.IOException;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Deque;
import java.util.List;
import java.util.Set;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Converts a Javadoc comment into Markdown.
*
* <p>Usage:
* <pre>
* java JavadocToMarkdown.java MyClass.java // converts every Javadoc comment in the file
* cat comment.txt | java JavadocToMarkdown.java
* </pre>
*
* <p>Requires Java 11 or newer.
*/
public final class JavadocToMarkdown {
private JavadocToMarkdown() {}
// Private-use character that delimits placeholders for protected text.
private static final char MARK = '\uE000';
private static final Pattern COMMENT = Pattern.compile("/\\*\\*.*?\\*/", Pattern.DOTALL);
private static final Pattern BLOCK_TAG = Pattern.compile("^@([A-Za-z][\\w.-]*)\\b\\s*");
private static final Pattern PRE =
Pattern.compile("<pre\\b[^>]*>(.*?)</pre\\s*>", Pattern.CASE_INSENSITIVE | Pattern.DOTALL);
private static final Pattern PLACEHOLDER = Pattern.compile(MARK + "(\\d+)" + MARK);
private static final Set<String> HANDLED_TAGS =
Set.of("param", "return", "throws", "exception", "see", "deprecated",
"author", "version", "since");
// ------------------------------------------------------------------
// Public API
// ------------------------------------------------------------------
/** Converts one Javadoc comment (with or without the delimiters) to Markdown. */
public static String convert(String javadoc) {
Parsed parsed = parse(stripComment(javadoc));
List<String> blocks = new ArrayList<>();
// Deprecation notice first, as a block quote.
for (BlockTag t : parsed.tags) {
if (t.name.equals("deprecated")) {
String text = "**Deprecated.** " + inline(t.text.toString());
blocks.add("> " + text.strip().replace("\n", "\n> "));
break;
}
}
// Main description.
String description = inline(parsed.description.toString());
if (!description.isEmpty()) {
blocks.add(description);
}
// @param (type parameters like <T> are listed separately).
List<String> params = new ArrayList<>();
List<String> typeParams = new ArrayList<>();
for (BlockTag t : parsed.tags) {
if (t.name.equals("param")) {
String line = namedItem(t.text.toString());
(t.text.toString().strip().startsWith("<") ? typeParams : params).add(line);
}
}
addList(blocks, "Type parameters", typeParams);
addList(blocks, "Parameters", params);
// @return
for (BlockTag t : parsed.tags) {
if (t.name.equals("return")) {
blocks.add("**Returns**\n\n" + inline(t.text.toString()));
break;
}
}
// @throws / @exception
List<String> throwsList = new ArrayList<>();
for (BlockTag t : parsed.tags) {
if (t.name.equals("throws") || t.name.equals("exception")) {
throwsList.add(namedItem(t.text.toString()));
}
}
addList(blocks, "Throws", throwsList);
// @see
List<String> see = new ArrayList<>();
for (BlockTag t : parsed.tags) {
if (t.name.equals("see")) {
String text = t.text.toString().strip();
boolean freeform = text.startsWith("<") || text.startsWith("\"");
see.add("- " + (freeform ? inline(text) : "`" + text.replaceAll("\\s+", " ") + "`"));
}
}
addList(blocks, "See also", see);
// @since / @version / @author
for (String name : new String[] {"since", "version", "author"}) {
for (BlockTag t : parsed.tags) {
if (t.name.equals(name)) {
String label = Character.toUpperCase(name.charAt(0)) + name.substring(1);
blocks.add("**" + label + ":** " + inline(t.text.toString()));
}
}
}
// Anything else (custom or less common tags).
for (BlockTag t : parsed.tags) {
if (!HANDLED_TAGS.contains(t.name)) {
blocks.add("**@" + t.name + "** " + inline(t.text.toString()));
}
}
return String.join("\n\n", blocks) + "\n";
}
// ------------------------------------------------------------------
// Comment parsing
// ------------------------------------------------------------------
private static final class BlockTag {
final String name;
final StringBuilder text = new StringBuilder();
BlockTag(String name) {
this.name = name;
}
}
private static final class Parsed {
final StringBuilder description = new StringBuilder();
final List<BlockTag> tags = new ArrayList<>();
}
/** Removes the comment delimiters and the leading asterisks of each line. */
static String stripComment(String comment) {
String s = comment.strip().replaceFirst("^/\\*+", "").replaceFirst("\\*+/$", "");
StringBuilder sb = new StringBuilder();
for (String line : s.split("\\R", -1)) {
sb.append(line.replaceFirst("^\\s*\\* ?", "")).append('\n');
}
return sb.toString();
}
/** Splits the comment body into the main description and the block tags. */
private static Parsed parse(String body) {
Parsed parsed = new Parsed();
BlockTag current = null;
int preDepth = 0;
int braceDepth = 0;
for (String line : body.split("\\R", -1)) {
String trimmed = line.stripLeading();
Matcher m = BLOCK_TAG.matcher(trimmed);
// A line starting with @ is a block tag, unless we are inside <pre> or {@...}.
if (preDepth == 0 && braceDepth == 0 && m.find()) {
current = new BlockTag(m.group(1));
parsed.tags.add(current);
current.text.append(trimmed.substring(m.end()));
} else if (current != null) {
current.text.append('\n').append(line);
} else {
parsed.description.append(line).append('\n');
}
preDepth = Math.max(0, preDepth + count(line, "<pre") - count(line, "</pre"));
braceDepth = updateBraceDepth(braceDepth, line);
}
return parsed;
}
private static int count(String haystack, String needle) {
String h = haystack.toLowerCase();
int n = 0;
for (int i = h.indexOf(needle); i >= 0; i = h.indexOf(needle, i + needle.length())) {
n++;
}
return n;
}
private static int updateBraceDepth(int depth, String line) {
for (int i = 0; i < line.length(); i++) {
char c = line.charAt(i);
if (c == '{' && (depth > 0 || line.startsWith("{@", i))) {
depth++;
} else if (c == '}' && depth > 0) {
depth--;
}
}
return depth;
}
// ------------------------------------------------------------------
// Rendering helpers
// ------------------------------------------------------------------
private static void addList(List<String> blocks, String heading, List<String> items) {
if (!items.isEmpty()) {
blocks.add("**" + heading + "**\n\n" + String.join("\n", items));
}
}
/** Renders "name description" as a list item: - `name` — description. */
private static String namedItem(String raw) {
String text = raw.strip();
int ws = indexOfWhitespace(text);
String name = ws < 0 ? text : text.substring(0, ws);
String desc = ws < 0 ? "" : text.substring(ws).strip();
return "- `" + name + "`" + (desc.isEmpty() ? "" : " — " + inline(desc));
}
private static int indexOfWhitespace(String s) {
for (int i = 0; i < s.length(); i++) {
if (Character.isWhitespace(s.charAt(i))) {
return i;
}
}
return -1;
}
// ------------------------------------------------------------------
// Inline conversion: {@tags}, HTML, <pre> blocks
// ------------------------------------------------------------------
/** Converts running Javadoc text (inline tags and HTML) to Markdown. */
private static String inline(String text) {
List<String> store = new ArrayList<>();
String s = extractPre(text, store);
s = expandInline(s, false, store);
// Javadoc line breaks are just whitespace, so normalise each line.
String[] lines = s.split("\\R", -1);
for (int i = 0; i < lines.length; i++) {
lines[i] = lines[i].strip();
}
s = String.join("\n", lines);
s = convertHtml(s);
s = s.replaceAll("\n{3,}", "\n\n").strip();
return restore(s, store);
}
/** Replaces <pre> blocks with fenced code blocks (stored as placeholders). */
private static String extractPre(String text, List<String> store) {
Matcher m = PRE.matcher(text);
StringBuilder sb = new StringBuilder();
while (m.find()) {
String code = expandInline(m.group(1), true, store);
code = code.replaceAll("(?i)</?(code|tt)\\s*>", "");
code = unescapeHtml(code);
String fenced = "```java\n" + tidyCode(code) + "\n```";
m.appendReplacement(sb, Matcher.quoteReplacement("\n\n" + protect(fenced, store) + "\n\n"));
}
m.appendTail(sb);
return sb.toString();
}
/**
* Expands {@code {@tag ...}} constructs (with balanced braces).
*
* @param raw true inside a code block, where no Markdown decoration is added
*/
private static String expandInline(String s, boolean raw, List<String> store) {
StringBuilder out = new StringBuilder();
int i = 0;
while (i < s.length()) {
int start = s.indexOf("{@", i);
if (start < 0) {
out.append(s, i, s.length());
break;
}
out.append(s, i, start);
int end = findClosingBrace(s, start);
if (end < 0) { // unbalanced: leave as-is
out.append(s.substring(start));
break;
}
String inner = s.substring(start + 2, end);
int ws = indexOfWhitespace(inner);
String tag = ws < 0 ? inner : inner.substring(0, ws);
String arg = ws < 0 ? "" : inner.substring(ws + 1);
out.append(renderInlineTag(tag, arg, raw, store));
i = end + 1;
}
return out.toString();
}
private static int findClosingBrace(String s, int open) {
int depth = 0;
for (int i = open; i < s.length(); i++) {
char c = s.charAt(i);
if (c == '{') {
depth++;
} else if (c == '}' && --depth == 0) {
return i;
}
}
return -1;
}
private static String renderInlineTag(String tag, String arg, boolean raw, List<String> store) {
switch (tag) {
case "code":
return raw ? arg : codeSpan(arg.replaceAll("\\s*\\R\\s*", " ").strip(), store);
case "literal":
return raw ? arg : protect(arg.replaceAll("\\s*\\R\\s*", " ").strip(), store);
case "link":
case "linkplain": {
String[] parts = splitReference(arg.strip());
String display = parts[1].isEmpty() ? parts[0] : parts[1];
if (raw) {
return display;
}
return tag.equals("link") ? codeSpan(display, store) : protect(display, store);
}
case "value":
case "systemProperty":
return raw ? arg.strip() : codeSpan(arg.strip(), store);
case "inheritDoc":
return raw ? "" : "_(inherited documentation)_";
case "docRoot":
return "";
case "index": {
String term = arg.strip();
if (term.startsWith("\"")) {
int close = term.indexOf('"', 1);
term = close > 0 ? term.substring(1, close) : term.substring(1);
} else {
int ws = indexOfWhitespace(term);
term = ws < 0 ? term : term.substring(0, ws);
}
return protect(term, store);
}
default: // summary, return, snippet, unknown tags: keep the content
return expandInline(arg.strip(), raw, store);
}
}
/** Splits "Foo#bar(int, String) label" into reference and label. */
private static String[] splitReference(String arg) {
int paren = 0;
for (int i = 0; i < arg.length(); i++) {
char c = arg.charAt(i);
if (c == '(') {
paren++;
} else if (c == ')') {
paren--;
} else if (paren == 0 && Character.isWhitespace(c)) {
return new String[] {arg.substring(0, i), arg.substring(i).strip()};
}
}
return new String[] {arg, ""};
}
private static String codeSpan(String text, List<String> store) {
if (text.isEmpty()) {
return "";
}
int longest = 0;
int run = 0;
for (char c : text.toCharArray()) {
run = (c == '`') ? run + 1 : 0;
longest = Math.max(longest, run);
}
String fence = "`".repeat(longest + 1);
String pad = (text.startsWith("`") || text.endsWith("`")) ? " " : "";
return protect(fence + pad + text + pad + fence, store);
}
// ------------------------------------------------------------------
// HTML -> Markdown
// ------------------------------------------------------------------
private static String convertHtml(String s) {
// Links (and drop empty named anchors).
s = s.replaceAll("(?is)<a\\s+(?:name|id)\\s*=[^>]*>\\s*</a\\s*>", "");
s = s.replaceAll("(?is)<a\\s+[^>]*?href\\s*=\\s*[\"']([^\"']*)[\"'][^>]*>(.*?)</a\\s*>", "[$2]($1)");
// Headings.
s = Pattern.compile("(?is)<h([1-6])\\b[^>]*>(.*?)</h\\1\\s*>").matcher(s).replaceAll(r ->
Matcher.quoteReplacement("\n\n" + "#".repeat(Integer.parseInt(r.group(1)))
+ " " + r.group(2).strip() + "\n\n"));
// Lists.
s = convertLists(s);
// Inline code: if it already contains protected spans, just drop the tags.
s = Pattern.compile("(?is)<(code|tt)\\b[^>]*>(.*?)</\\1\\s*>").matcher(s).replaceAll(r ->
Matcher.quoteReplacement(r.group(2).indexOf(MARK) >= 0 ? r.group(2) : "`" + r.group(2) + "`"));
// Simple tags.
s = s.replaceAll("(?i)<p\\b[^>]*>|</p\\s*>", "\n\n");
s = s.replaceAll("(?i)<br\\s*/?>", " \n");
s = s.replaceAll("(?i)<hr\\s*/?>", "\n\n---\n\n");
s = s.replaceAll("(?i)</?(b|strong)\\s*>", "**");
s = s.replaceAll("(?i)</?(i|em)\\s*>", "*");
// Entities that read better decoded (< > & are valid Markdown as-is).
return s.replace("@", "@").replace("@", "@").replace(" ", " ");
}
/** Converts ul/ol/li into Markdown lists, including nesting. */
private static String convertLists(String s) {
Matcher m = Pattern.compile("(?i)<(/?)(ul|ol|li)\\b[^>]*>").matcher(s);
StringBuilder out = new StringBuilder();
Deque<int[]> stack = new ArrayDeque<>(); // {ordered ? 1 : 0, item counter}
int last = 0;
while (m.find()) {
out.append(s, last, m.start());
last = m.end();
boolean closing = !m.group(1).isEmpty();
String name = m.group(2).toLowerCase();
if (name.equals("li")) {
if (!closing && !stack.isEmpty()) {
int[] top = stack.peek();
if (top[1]++ > 0) { // not the first item: keep the list tight
while (out.length() > 0 && Character.isWhitespace(out.charAt(out.length() - 1))) {
out.setLength(out.length() - 1);
}
}
String bullet = top[0] == 1 ? top[1] + "." : "-";
out.append('\n').append(" ".repeat(stack.size() - 1)).append(bullet).append(' ');
}
} else if (!closing) {
if (stack.isEmpty()) {
out.append('\n');
}
stack.push(new int[] {name.equals("ol") ? 1 : 0, 0});
} else {
if (!stack.isEmpty()) {
stack.pop();
}
out.append('\n');
if (stack.isEmpty()) {
out.append('\n');
}
}
}
return out.append(s.substring(last)).toString();
}
private static String unescapeHtml(String s) {
return s.replace("<", "<").replace(">", ">").replace(""", "\"")
.replace(" ", " ").replace("@", "@").replace("@", "@")
.replace("&", "&");
}
/** Trims blank lines around code and removes common indentation. */
private static String tidyCode(String code) {
List<String> lines = new ArrayList<>(Arrays.asList(code.split("\\R", -1)));
while (!lines.isEmpty() && lines.get(0).isBlank()) {
lines.remove(0);
}
while (!lines.isEmpty() && lines.get(lines.size() - 1).isBlank()) {
lines.remove(lines.size() - 1);
}
int indent = Integer.MAX_VALUE;
for (String l : lines) {
if (!l.isBlank()) {
int n = 0;
while (n < l.length() && l.charAt(n) == ' ') {
n++;
}
indent = Math.min(indent, n);
}
}
if (indent == Integer.MAX_VALUE) {
indent = 0;
}
List<String> result = new ArrayList<>();
for (String l : lines) {
result.add(l.isBlank() ? "" : l.substring(Math.min(indent, l.length())).stripTrailing());
}
return String.join("\n", result);
}
// ------------------------------------------------------------------
// Placeholders: protect finished Markdown from later HTML processing
// ------------------------------------------------------------------
private static String protect(String text, List<String> store) {
store.add(text);
return MARK + String.valueOf(store.size() - 1) + MARK;
}
private static String restore(String s, List<String> store) {
return PLACEHOLDER.matcher(s).replaceAll(r -> Matcher.quoteReplacement(store.get(Integer.parseInt(r.group(1)))));
}
// ------------------------------------------------------------------
// Command line
// ------------------------------------------------------------------
public static void main(String[] args) throws IOException {
String input = args.length > 0
? Files.readString(Path.of(args[0]), StandardCharsets.UTF_8)
: new String(System.in.readAllBytes(), StandardCharsets.UTF_8);
List<String> results = new ArrayList<>();
Matcher m = COMMENT.matcher(input);
while (m.find()) {
results.add(convert(m.group()));
}
if (results.isEmpty() && !input.isBlank()) { // plain text without delimiters
results.add(convert(input));
}
System.out.print(String.join("\n---\n\n", results));
}
}Determining whether a varcond implementation supports negation no longer matches the declared ArgumentType classes against the constructor's parameter types. The argument types are only coarse categories used for parsing and do not match the concrete parameter types (e.g. \isConstant expects an ArgumentType.VARIABLE, but ConstantCondition's constructor takes a JAbstractSortedOperator). A failed match made isNegationSupported throw an IllegalStateException, which was swallowed by TacletPBuilder's manipulator application, so the varcond could not be applied at all and taclet files using \isConstant or \hasLabel failed to load, breaking all key.core.wd run-all-proofs tests. The negation support check is restored to the previous lenient behavior: the first declared public constructor's last parameter must be boolean. Constructor lookup for documentation purposes now matches by parameter count and falls back to empty javadoc if the class was not processed by the therapi scribe. Also fix the warning in TacletPBuilder to print the argument types array instead of its identity.
Reintroduces the check that a varcond implementation constructor matches the declared ArgumentTypes, which was dropped as part of the initial fix for the wd proof tests. The negation-support detection is now tiered: a constructor whose parameter types are compatible with the declared argument types is preferred and decides negation support by its trailing boolean parameter. Only if no type-compatible constructor exists (the ArgumentType categories only approximate the real parameter types, as for \isConstant and \hasLabel), the previous lenient fallback on the first public constructor is retained. findConstructor (used for documentation lookup) prefers a type-compatible constructor and falls back to matching by parameter count. Verified: :key.core.wd:testRunAllWdProofs passes 9/9.
The documentation generators (VarcondDoc, ScriptDoc) extract Javadocs via therapi from de.uka.ilkd.key.rule.conditions and de.uka.ilkd.key.scripts. Complete the gaps so the generated documentation is not empty: - rule.conditions: add missing class documentation (ArrayLength, DifferentInstantiation, DropEffectlessElementaries, DropEffectlessStores, EqualUnique, FreeLabelIn, MetaDisjoint, Observer, SimplifyIfThenElseUpdate) and constructor documentation with @PARAM descriptions for all variable condition implementations and TypeResolver's nested resolvers; fix the copy-pasted class documentation of IsThisReference. - scripts: document TermWithHoles and SequentWithHoles, fill the empty class documentation of the deprecated SchemaVarCommand, and add the missing class-level @documentation to the Parameters classes of branches, expandDef, rewrite, and set. - normalize license headers to the spotless template (ScriptDoc, VarcondDoc, TacletBuilderCommandInfo).
…build Add the Gradle tasks generateVarcondDoc and generateScriptDoc, which run the documentation generators (VarcondDoc, ScriptDoc) and write the resulting markdown to key.core/build/docs/keydocs. The nightly workflow additionally sets up JDK 25 for the generation step (therapi's scribe only extracts '///' markdown javadocs on JDK 23+), packages the generated files and uploads them as the artifact "varcond-script-docs" with a retention of 30 days.
- ArgumentsLifter: null-guard the therapi javadoc lookups, which return null for classes compiled with a JDK that does not recognize the used doc comment style, and format field javadoc comments with the CommentFormatter instead of printing the raw FieldJavadoc object. - TacletBuilderCommandInfoImpl: bound the @PARAM name lookup by the documented parameter count, which may be shorter than the declared argument types.
…riptDoc Extract the common functionality of the documentation generators into the new base class AbstractDocGenerator: - output handling: the generators write to stdout, or to the file given as the first command line argument (creating missing directories), which simplifies the Gradle tasks generateVarcondDoc/generateScriptDoc - javadoc post-processing: cleanJavadoc and indent are moved here and are now also applied by ScriptDoc - ScriptDoc additionally prints a section header per command, matching the format of VarcondDoc
The generators now also emit a structured JSON dump next to the markdown file (varconds.json, script-commands.json), containing the same information in a machine-readable form: names, categories, deprecation flags, descriptions, signatures with negation support, and arguments with kind, type, position and description. The shared base class AbstractDocGenerator gains a generateJsonData() hook; the new dependency-free JsonWriter serializes the data. The nightly workflow's packaging step picks the JSON files up unchanged.
- Annotate all program and term transformers with @TransformerMeta(name=...), using the internal meta-construct name passed as the first argument to super(..); mark the annotation @retention(RUNTIME) and read it from the new CodeTransformerDoc generator. - Add CodeTransformerDoc producing markdown + JSON dumps of all code transformers, register the generateCodeTransformerDoc Gradle task and run it in the nightly build (nightlydeploy.yml). - Rework AbstractDocGenerator.cleanJavadoc: parse inline tags with a brace-balanced scanner (preserving braces inside {code} and {snippet}), translate {link ...} to markdown links and {snippet : ...} to fenced code blocks; fix HTML entity/tag conversion. - Extend -Ajavadoc.packages to de.uka.ilkd.key.rule.metaconstruct.
The documentation generators (VarcondDoc, ScriptDoc, CodeTransformerDoc) previously ran two parallel traversals to produce markdown and JSON, which kept drifting apart (e.g. transformer parameters were javadoc names in the markdown but reflection names arg0/arg1 in the JSON). Generators now build a common data model once - List<DocItem> with DocSignature and DocParameter - that is both dumped verbatim as JSON and rendered to markdown by the shared AbstractDocGenerator base class. The records cover all three documentation types: variable conditions (overloads, negatable signatures), proof script commands (category, deprecated, argument kinds/position/varargs) and code transformers (constructors). JsonWriter serializes records via their record components. Markdown output additionally uses javadoc parameter names and shows a signatures section for script commands; all text is cleanJavadoc-processed in both outputs. Verification: compileJava and spotlessApply clean; generateVarcondDoc, generateScriptDoc and generateCodeTransformerDoc produce valid JSON with unchanged item counts (53 varconds, 39 script commands, 52 transformers).
d568894 to
9ced70c
Compare
|
@unp1 I also added the program/term transformer, but the documentation there is also rather poor:
|
Related Issue
This pull request does not resolve a specific issue; it continues and extends the
documentation-generation feature of this branch.
Intended Change
This PR adds the generation of user documentation for the taclet language constructs —
variable conditions (varconds), proof script commands, and code transformers — and fixes the
varcond builder machinery that was broken by the initial version of this feature:
Fix broken rule loading (regression on this branch):
TacletBuilderCommandInfo.isNegationSupported()threw an
IllegalStateExceptionfor varcond implementations whose constructorparameter types do not match the declared
ArgumentTypecategories (e.g.\isConstant,\hasLabel). The exception was swallowed byTacletPBuilderandsurfaced as
semanticError("Could not apply the given variable condition"),which made the wd rule files (
wdGeneralRules.key,wdFormulaRules.key) fail toload, breaking all 8 wd proofs. Negation detection is now tiered: a constructor
whose parameter types are compatible with the declared argument types decides
negation support by its trailing
booleanparameter; only if no type-compatibleconstructor exists, the lenient fallback on the first public constructor is used.
findConstructor(documentation lookup) prefers type-compatible constructors andfalls back to matching by parameter count.
Documentation generators for the three taclet-language construct types, built on a
single source of truth:
VarcondDoc(all registered varconds),ScriptDoc(all proof script commands), andCodeTransformerDoc(all program and term transformers, discovered via the new@TransformerMetaannotation that carries the internal meta-construct name).DocItems with nestedDocSignature/DocParameterrecords — that is both dumped verbatim as a structuredJSON file and used to render the Markdown document (in the shared base class
AbstractDocGenerator). This replaces the previous design with two paralleltraversals, in which the Markdown and JSON outputs drifted apart (e.g. transformer
parameters appeared under their javadoc names in the Markdown but under reflection
names
arg0/arg1in the JSON). The dependency-freeJsonWriterserializesrecords via their record components.
AbstractDocGenerator.cleanJavadoc()was overhauled: inline tags are now scannedbrace-balanced (unbalanced braces and
{@snippet}bodies are handled correctly),{@link}/{@linkplain}become Markdown links, and inline snippets(
{@snippet lang="..." : ...}) are rendered as fenced code blocks.de.uka.ilkd.key.rule.metaconstruct(includingarith)are annotated with
@TransformerMeta(name = "..."), using the internal name passedas the first argument of
super(...).Gradle integration: the tasks
:key.core:generateVarcondDoc,:key.core:generateScriptDoc, and:key.core:generateCodeTransformerDocwritevarconds.md/varconds.json,script-commands.md/script-commands.json, andcode-transformers.md/code-transformers.jsontokey.core/build/docs/keydocs.Nightly deployment: the nightly workflow additionally sets up JDK 25 (therapi's
scribe only extracts
///markdown javadocs on JDK 23+), runs the three generationtasks, and uploads
key.core/build/docs/keydocs/*as the artifactvarcond-script-docswith a retention of 30 days.
Javadoc completion: missing class and constructor documentation of the varcond
implementation classes in
de.uka.ilkd.key.rule.conditions(which feedVarcondDoc),gaps in
de.uka.ilkd.key.scripts(which feedScriptDoc), and the javadocs of thetransformer classes in
de.uka.ilkd.key.rule.metaconstruct(which feedCodeTransformerDoc) were completed, so the generated documentation is not empty.Plan
ArgumentType-vs-parameter-type check in a tiered designrule.conditions,scripts, andrule.metaconstruct@TransformerMeta(
DocItem/DocSignature/DocParameter) dumped as JSON and rendering the MarkdowngenerateVarcondDoc/generateScriptDoc/generateCodeTransformerDocKeYProject/key-docs) to download the artifact intodocs/userand add the pages to the nav
Type of pull request
Ensuring quality
./gradlew :key.core.wd:testRunAllWdProofspasses 9/9 with the reintroduced type checks../gradlew :key.core:generateVarcondDoc :key.core:generateScriptDoc :key.core:generateCodeTransformerDocproduce complete Markdown and JSON files (53 varconds, 39 proof script commands, 52 code
transformers); the 52 Markdown headings match the
@TransformerMetanames, and all JSONdumps parse as valid JSON.
./gradlew :key.core:compileJavaand:key.core:spotlessApplyrun cleanly.(The reflection-based matching is only used for negation detection and documentation
lookup, and the negation result is cached per command info.)
Additional information and contact(s)
The generated documentation is uploaded by the nightly workflow as the artifact
varcond-script-docs; the corresponding download step for the key-docs repository(
mkdocs.yml) will be contributed there separately.The contributions within this pull request are licensed under GPLv2, or (at your option) any later version, for inclusion in KeY.