[KIP] - We should have a comprehensive, user-facing reference manual for K.

Start by reviewing the existing tutorials, online documents, academic papers, and pending documentation mentioned in the issue. Use the proposed structure as a planning checklist, covering K usage, syntax, rewriting, modules, analysis, debugging, and command reference. Done means producing a comprehensive, cohesive user-facing manual that links to related resources.

[KIP] - We should have a comprehensive, user-facing reference manual for K.

Motivation

It can be difficult for K users to hop around tutorials and multiple references (online documents and academic papers) every time they need to learn about specific features that they want to use in their projects. Furthermore, having one resource to which we can refer people can significantly improve their user experience while working with K, and can make our lives easier as well (think of the various support channels we have --- riot channel, stackoverflow, ... etc).

Suggestion

I’d like to suggest having a comprehensive, user-facing reference manual for K. The objective would be to have one reference that we can point people to to learn about K or look up information about any specific feature of K, and from which they may be referred to other resources (existing tutorials, online projects, academic papers, .. etc).

Unlike existing resources, the reference manual will be

• comprehensive: describing all features of K and K tools designed for K users — the whole spectrum of users, and
• cohesive: describing related features and feature design decisions in a structured way.

I think this will complement existing resources quite well. The pending documentation we have right now can focus more on recent and experimental features that haven’t made their way to the reference manual yet. Also, the manual will not be a guide to defining different semantic styles in K, like the K tutorials, although it will probably include many smaller examples to illustrate concepts.

Example Structure

The following is a suggested general structure of the manual (Note: we probably already have material for most of these topics):

1. Introduction (what K is, its philosophy, highlights of why K, perhaps also a quick overview of its foundations, manual structure)
2. Using K (a quick tutorial on getting K, installing it, highlighting its tools and the different K backends and how they are used with a simple hello-world-like example)
3. Syntax and Parsing (everything that has to do with defining syntax in K and generating language parsers, with examples)
4. Rules and Rewriting (everything that has to do with defining semantics in K - configurations, continuations, matching, types of rules, rule attributes, … etc, and krun, with examples)
5. Modules and Predefined Data Modules (syntax vs. semantics modules, importing modules, modules included in K’s distribution- Sets, Lists, Maps, …, with examples)
6. Analyzing Programs (exploring the reachable state space of a program, proving invariants, model checking…, a quick overview of the theory behind it with appropriate pointers and with examples)
7. Advanced Features (optional)
8. Debugging K specs (methods and tools that help in debugging K specs)
9. Reference (A complete list of commands and their supported flags)
10. Index