sv-witnesses icon indicating copy to clipboard operation
sv-witnesses copied to clipboard

Combined schema for YAML witnesses

Open sim642 opened this issue 2 years ago • 6 comments

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 for automatically generating and deploying HTML documentation from schema. Result in my fork: https://sim642.github.io/sv-witnesses/yaml/.

TODO

  • [x] Review/complete descriptions which need to be generic (not loop_invariant specific) in $defs.
  • [x] Fix format inconsistencies between README and schema.
  • [ ] Specify location_invariant from #59?
  • [x] Add long descriptions to schema.
  • [x] Change workflow branch before merge.

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?

sim642 avatar Jun 13 '22 17:06 sim642

Looks good to me now and can be merged once the branch name is changed in the workflow.

That's now done as well. After merged, GitHub Pages needs to be configured in this repository's settings to deploy from the gh-pages branch root. There's something about the first deployment failing: https://github.com/peaceiris/actions-gh-pages#%EF%B8%8F-first-deployment-with-github_token.

sim642 avatar Aug 11 '22 15:08 sim642

After merged, GitHub Pages needs to be configured in this repository's settings to deploy from the gh-pages branch root.

This has to be done by @dbeyer.

At least in my fork there was no problem with the deployment.

SvenUmbricht avatar Aug 11 '22 15:08 SvenUmbricht

I think the idea is to move this repo to GitLab as well, like the other competition repos. Doesn't really make sense to introduce a new URL containing "github" before this, I guess?

PhilippWendler avatar Aug 11 '22 17:08 PhilippWendler

I do not know of any plans of moving this repo. We ran this PR against @dbeyer who approved, maybe some comment?

If the plan is to move this repo to gitlab, we should have done this when we moved the other repos, so there must be something that prevents this or it is oversight? Anyways I do not see a strong benefit from switching to gitlab, but of course it makes sense to have some consistency. I guess a github workflow can be transferred into a gitlab ci job quite easily, judging from the similar syntax?

MartinSpiessl avatar Aug 11 '22 18:08 MartinSpiessl

I guess a github workflow can be transferred into a gitlab ci job quite easily, judging from the similar syntax?

That's misleading because both just happen to use Yaml, but what happens inside is quite different. But it is easy to write a GitLab job that executes this single command and pushes the result, we have that in several other repositories.

But I guess we first also have to decide whether we want to use it on a GitLab domain or somewhere below sosy-lab.org.

PhilippWendler avatar Aug 12 '22 08:08 PhilippWendler

And whether we want to actually migrate it now. Seems like it would be better to just move forward here for now.

MartinSpiessl avatar Aug 12 '22 09:08 MartinSpiessl