Combined schema for YAML witnesses

[sim642]

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. Introduce entry type 'location_invariant' for YAML-based witnesses. #59 (comment)).
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

• 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 Introduce entry type 'location_invariant' for YAML-based witnesses. #59?
• Add long descriptions to schema.
• 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?

[SvenUmbricht]

Very nice, the generated documentation looks good and I didn't notice any major problems. Regarding the new location_invariant entry type, it is probably better if I do this in #59, since the changes there have not yet been reviewed and it seems simple enough to extend the schema.

[SvenUmbricht]

It would be better to use enum instead of const here, so that when we have a new version witnesses in both the old and the new format are valid.

Having a single-value enum in the meantime shouldn't be a problem, and other fields already use this.

[sim642]

Any particular copy of the schema specifies a single version of the format though, not multiple incompatible versions. And the only reason to bump the version would be due to some (notable) incompatible changes to the schema.

Although this version is specified per-entry, so it's also unclear how the versioning is supposed to work. Is a single witness file allowed to contain entries with different versions, each one cohering to the respective version of the schema? If so, then that significantly complicates everything (beyond just this schema definition).
Since it's format-version, not entry-type-version, then the more reasonable thing is that all entries use the same version and for each version there could be a schema.

[SvenUmbricht]

That's a good point. I agree that allowing entries that adhere to different format versions would complicate things too much, but of course not doing so still has several disadvantages, most notably:

1. Validators will either have to be able to produce loop_invariant_certificate and similar entries in each format version that they support as input (potentially leading to unnecessary code duplication), or will have to able to transcribe (parts of) an old witness into a new format version. Otherwise we end up with validators for specific versions of the format.
2. Similarly, old witnesses might have to be transcribed to be of use to tools that only support newer versions of the format
3. Each new format version would require a separate copy of the schema that needs to be maintained (although only the latest one, if any, should be subject to change)

I guess this is something that has to be discussed further, but should not be blocking for this PR, especially since the old README (though not the old schema) already had this problem.

[SvenUmbricht]

Looks good to me now and can be merged once the branch name is changed in the workflow.
I'd leave the above two conversations unresolved for now so that they aren't forgotten, but I'm not sure whether Github blocks the merge because of that.

[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.

[SvenUmbricht]

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.

[PhilippWendler]

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?

[MartinSpiessl]

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?

[PhilippWendler]

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.

[MartinSpiessl]

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