kani icon indicating copy to clipboard operation
kani copied to clipboard

Generate `benchcomp.yaml` documentation from schema

Open karkhaz opened this issue 1 year ago • 1 comments

Description of changes:

This PR adds a validation schema for the benchcomp configuration file format, as well as code to emit that schema into the Kani book. This is in preparation for further PRs that will add similar schemas for the format that a benchcomp parser should emit, and the format that benchcomp visualizers should expect, both of which will also be rendered in the book.

Here is a rendered version.

Resolved issues:

Resolves #2592

Related RFC:

None

Call-outs:

N/A

Testing:

  • How is this change tested?[

Rendered version](https://karkhaz.github.io/kani/benchcomp-conf.html) on my fork

  • Is this a refactor change?

No

Checklist

  • [ ] Each commit message has a non-empty body, explaining why the change was made
  • [x] Methods or procedures are documented
  • [x] Regression or unit tests are included, or existing tests cover the modified code
  • [ ] My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

karkhaz avatar Jul 10 '23 16:07 karkhaz

Here is how it looks, the text is slightly out of date (I've since made the example shorter)

Screen Shot 2023-07-10 at 17 45 07

karkhaz avatar Jul 11 '23 15:07 karkhaz