Clarifications to herd documentation

[knatten]

In section 14.1 "Sequential consistency" in the documentation, there seems to be some mismatches between the included sc.cat and the following explanation, which makes it hard to follow.

The explanation says:

The computation of new relations from other relations, and their binding to a name with the let construct. Here, a new relation com is the union “|” of the three pre-defined communication relations.

However, there is no relation com in sc.cat, and the let construct is not being used.

The explanation continues:

The performance of some checks. Here the relation “po | com” (i.e. the union of program order po and of communication relations) is required to be acyclic.

Again there is no com in that example.

Finally, the line show sm\id as si is not explained, neither is the ;sm part in the sc definition.

It would be good if the explanation was updated to reflect the contents of sc.cat.

I btw noticed that there are two copies of sc.cat in the repository. Maybe it's better to use the other one in an introductory example like this, since it is a bit simpler:

diff ./herd/libdir/sc.cat ./herd-www/cat_includes/sc.cat

10,11c10
< show sm\id as si
< acyclic po | ((fr | rf | co);sm) as sc
---
> acyclic po | fr | rf | co as sc

``

[maranget]

Hi @knatten, thanks for reporting this. PR #986 is a tentative fix.

[knatten]

Hi @knatten, thanks for reporting this. PR #986 is a tentative fix.

Thanks for the quick fix, I think this helps a lot.