I found Adobe Reader to be fairly user hostile software in terms of
usability.
There are other pdf readers. I have found Foxit to be pretty good and
appears to have fewer bugs than Adobe Reader, but I find it somewhat
clunkier.
I think that ... HTML is a lot more feasible today that it would have
been ten years ago.
If anyone knows of a better way to display the Hyperbook than pdf that
is easily available on the three supported platforms and is likely to
still work in 20 years, please let me know about it.
If the sources for the hyperbook and the PlusCal manual are available
publicly with a creative commons license the community can experiment
with pulling the documentation into a new form.
I will be happy to assist anyone who wants to improve the
documentation, including by making the sources of the existing
documents available to them. However, one requirement is that it must
not make it less convenient for me to continue modifying the
documents--especially the Hyperbook. Since I have been developing my
personal LaTeX environment for the past 30 years, this is a
non-trivial requirement.
As I spent more time with TLA and PlusCal, the fractured nature of the
documentation became a bigger hassle for me.
It has been my intention to make the Hyperbook replace at least the
first part of Specifying Systems. Some "fracturing" of the
documentation is inevitable, since few people will want to read things
like the chapters of Specifying Systems on the semantics of TLA+, so
it's not worth the effort of making it as user-friendly as I want the
Hyperbook to be.
The one thing I intensely long for is a REPL;
I don't know what kind of REPL for TLA+ you (and Chris) would like.
Please describe explicit scenarios that you would like to have
supported. Be as fanciful as you like. The only constraint is that
the E(valuate) has to be performed by the TLC model checker, so forget
about anything that involves instantly reporting all errors in a spec
with 10^27 reachable states.
Leslie