Open
Description
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