Skip to content

Combined schema for YAML witnesses

Simmo Saan requested to merge github/fork/sim642/yaml-schema into main

Changes

  1. Replace loop_invariant schema with a combined schema that also specifies loop_invariant_certificate.
  2. Add descriptions to schema.
  3. Extract reusable $defs in schema to simplify new entry type specification (c.f. https://github.com/sosy-lab/sv-witnesses/pull/59#discussion_r894263041).
  4. Remove hand-written descriptions from README.
  5. Add GitHub Actions workflow GitLab pipeline for automatically generating and deploying HTML documentation from schema. Result in my fork: https://sim642.gitlab.io/sv-witnesses/yaml/.

TODO

  • Review/complete descriptions which need to be generic (not loop_invariant specific) in $defs.
  • Fix format inconsistencies between README and schema.
  • Specify location_invariant from !59 (merged)? Merged !62 (closed) into this as !59 (merged) was merged to main.
  • Add long descriptions to schema.
  • Change workflow branch before merge.
  • Switch GitHub Pages to GitLab Pages.

There are tools that can convert JSON schemas to human-readable HTML/Markdown documentation, e.g. https://github.com/coveooss/json-schema-for-humans. So here's a radical idea: ditch the fine-grained specifications in YAML README and only maintain the schema as the authoritative source. Markdown documentation could be generated from it (instead of manually having to keep the two in sync) and more interactive HTML documentation could be generated (and automatically published to this repository's GitHub Pages). Thoughts?

Edited by Simmo Saan

Merge request reports