FStarLang / FStarLang/FStar

Improving the usability of F* (master issue!)

Open
#614 16 comments 3 reactions 0 assignees View on GitHub
area/usability kind/meta-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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.