[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Jasmin Christian Blanchette]

> 
>> Perhaps Jasmin has some experience.
> 
> His manuals are not even formally checked by Isabelle, so this is two steps backwards.

Considering that you do not take objection to the manuals' actual accuracy, completeness, structure, typesetting, quality of writing, examples, or ease of use as references, and that you restrict your scope to a small fraction of the technical documentation I have written in the last ten years (and for the rest, I could explain to you in detail how and to what extent it was formally checked if that interests you), your criticism is rather toothless.

To answer Tjark's question: No, I don't have experience with linking from software to documentation. Qt was a library, not an application, so it didn't have any help system. But if you need to refer to a section of the documentation from a message, what I would do in these cases is spell out the title of the section and omit the section number, and add a comment in the .tex file right above the section heading to remind myself to update the software. This I find superior to leaving the user helpless, even if it's more risky and could get out of sync.

Jasmin