Book-length living documentation

[sorear]

Currently most of what you want is either in old papers or in the code; we should have a document that is continuously updated and cross-referenced so that a complete newcomer can get useful information from it.

Unlike most high efforts this can be done incrementally on master and will be immediately useful.

Quick thoughts on possible organization:

• Guide (task oriented)
  • System requirements and dependencies
  • Downloading the compiler
  • Write, compile, and run code with the concrete syntax compiler
  • Same but with the pure function translator; [other translators?]
  • Writing FFI code
  • Build from source, proofs, tests
• User reference
  • Overview: motivation, design decisions
  • Language semantics: values, types, expressions, declarations, basis
  • Operating environment: targets (including references to asm semantics), FFI assumptions, machine setup assumptions, invocation of executables generated with basis_ffi
  • Standalone compiler manual: concrete syntax, options index, system requirements and invocation
  • Translator manual: what translators exist, detailed rules for what they accept, invocation of compilationLib, HOL setup requirements
  • Optimization manual: exactly enough information about the passes to predict time and space complexity, optimization options, description of the explorer and its output
  • Debugging manual: representation of values and frames for when you need an assembly debugger, runtime tracing options
• Developer reference
  • Include language and asm semantics by reference from user manual
  • Detailed semantics of all intermediate languages
  • Detailed description of motivation, behavior and invariants of all passes