One comment about the hyperbook in particular, the text
description building up proofs is good to follow along and
force you to think
but when there is a problem it's easy to get lost without reference to the
final working TLA+ text.
It might be helpful to have the actual TLA+ modules accompany the
hyperbook, rather than just the PDF versions (even the ASCII in PDF form).
Agreed.
In general, I have tried to present a complete module after developing it bit by bit. However, sometimes a module isn't developed bit by bit, but a first version is developed, then it is modified to form another version, then modified again and again. So, instead of having a single complete module, there are quite a few. In those cases, it seems impractical to provide a complete module for each of those versions. Perhaps someone has a suggestion on what to do in that case. However, it is possible that there are places where it would be reasonable to provide a complete module (or perhaps a complete proof) and I have failed to do so. I would appreciate having those exact places pointed out.
Thanks,
Leslie