informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

Conventions for specification versioning #17

Closed josef-widder closed 3 years ago

josef-widder commented 4 years ago

Outcome of Discussion of Igor and myself on semantic versioning of English and TLA+ specs

josef-widder commented 4 years ago

I think it should be part of the name of the file and of the title of the document.

Regarding the time of changing the name (w.r.t. a PR), I am also not super clear what to do. Let's take a step back and look at the general problem: I guess internally, while we work on it, we understand quite well the maturity of a spec, and we trace the progress via PRs and issues. The problem is that 1) since we work in the open, we need to communicate to "the outside" the maturity of a document. I agree with your concern about duplication, but I am not sure that for documenting our work for others, it is enough to have the information in PRs. People might take anything on the main branch as "definitive" version. Especially for TLA+ specs this is problematic, as there are huge differences in maturity between a written spec that has been reviewed, and one that has been thoroughly checked with the help of a tool. 2) the maturity of the spec should be visible from the document and not just the progress of PRs. If we choose to abandon a spec for some months, it should be clear from the naming and versioning that it is not "finished".

konnov commented 4 years ago

In the context of a PR, does this mean we’ll have to rename a spec from e.g. “Draft Foo” to “Proposal Foo” after it has been reviewed in a or bit prior to it being merged into the main branch? If so, that seems a bit suspect to me, just insofar as it means we’re duplicating versioning branching information into the body of the text.

We should think of specs more like of protocol standards or RFCs. They are not released just once but are revised from time to time, and different revisions co-exist. I am also worried that somebody would start implementing a protocol using the Reviewed spec and later we will introduce bugfixes when validating it. For that reason, we should have the status and the version in the title, so the authors can also just refer to that. If we later update the spec, everybody would be able to see that just from the version number (and the status). Github is great, but it does not replace the librarian's work :-)