Improving the usability of F* (master issue!)
- Dominant language
- F*
- Stars
- 3.1k
- Forks
- 266
- Avg merge
- 21h 1m
- Merged PRs (30d)
- 54
Description
- [x] move the Low\* libraries under the LowStar prefix (instead of FStar)
- [x] remove old libraries from ulib/
- [x] F\* doc (the tool) (#634)
- [x] write, generate and nightly-rebuild+upload documentation for F*'s ulib
- [x] wiki page that documents a typical workflow:
- [x] the "moving `admit`" strategy, and general pitfalls when starting with F\* (e.g. z3 does not report the first error)
- [ ] how to debug "unknown assertion failed", how to read cryptic F\* error messages with TOP in the middle, unknown assertion failed because no `noeq`, confusion if no `open FStar_Mul`, etc.)
- [ ] cheap functors to remove the duplication for integer types (see [Cheap functors proposal](https://github.com/FStarLang/FStar/wiki/Cheap-functors))
- [x] proper pretty-printer for types (good for F*doc) (#36)
- [ ] naming conventions and design principles for the standard library -- create a wiki page (foo_of_x vs x_to_foo and x_as_foo) (See also [Editing-files-in-the-library](https://github.com/FStarLang/FStar/wiki/Editing-files-in-the-library))
- [x] fix the compiler so that it bootstraps, which will in turn allow
- [x] removing lib/ and contrib/
- [x] fix the confusion between src/basic and lib/
- [x] update tutorial (#627)
- [x] have `fstar --compile` which takes care of extracting + calling ocaml with the right voodoo (e.g. running the right make command in ulib/ml depending on --use_native_int and whether HyperHeap is used or not) and right cmxa
- [x] fix the terrible `Fstar.Mul` problem by switching to a unicode lexer and advertising × everywhere
- [x] Add *printf-like functions to the standard library (see #637)
[Update 2016-11-22] Tahina added more tasks in a comment below https://github.com/FStarLang/FStar/issues/614#issuecomment-262386275
[Update 2016-11-22] Catalin: moved that discussion to separate issue (#770) about POPL release.
Contributor guide
Research direction
Start by separating one unchecked item from the master checklist, then read the referenced wiki pages and issues such as #770. Relevant areas named here include ulib/, lib/, contrib/, src/basic, and the fstar --compile entry point; completion means defining and verifying one selected usability task rather than addressing the whole list.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- ocaml
- Domain
- compilers, documentation, tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 20/100