F* is an open source project developed in the open using an inclusive collaboration model meant to attract contributions from a broad and growing community, which includes various companies, universities, research institutes, and individuals.
The code of F* is released under the permissive Apache v2.0 License and is developed at https://github.com/FStarLang/FStar
Contributors to F* are required to sign a standard Contributor License Agreement (CLA) giving a non-exclusive license for their contribution to Microsoft, the main contributor to F*. The use of such a CLA is relatively common for open source projects where companies are involved.
Please make your contribution available as a pull request (PR). We expect all regression tests to pass on your PR before considering it eligible for review ("All checks have passed" green checkbox on GitHub).
The rationale for the PR should be explained, in the commit messages
and/or the Github PR. Ideally, PRs should come with comments and
documentation within the source tree, if applicable. If the PR
involves a non-backwards-compatible or possibly breaking change,
it should update CHANGES.md to reflect it.
Please add regression tests for your PR. Ideally, both positive and negative ones; especially so if the change is a bugfix, or touches a critical component. Failure attributes can help for that.
In case if build in CI fails, and you want to troubleshoot yourself, join Slack and go to #everest-all-builds channel and look for your broken build.
Finally, contributions should adhere to the following style guide: https://github.com/FStarLang/FStar/wiki/Style-guide
The F* compiler is written in F*, then extracted to OCaml. We keep a copy of the OCaml extracted compiler under version control. We do not expect external pull requests to refresh the snapshot. However, reviewers should take it upon themselves to update the snapshot before merging to master when this is needed to obtain a "Success" without breakages from CI (in particular without "snapshot-diff" breakages in the VSTS "Extra logs" = "Build Summary"). The reviewer may (in rare cases, when the change touches extraction) need to bootstrap twice to reach the fixpoint.
Historically, F* has favored merges over rebases, so we encourage pull requests
to merge master in frequently. We like commit dates to be consistent, and we
may try your pull request locally; finding that the remote has rebased tends to
make it harder to work with your pull request.
All of the important file formats should be in the .gitattributes, but we
expect any new file to have Unix line endings.
Internally, each regression build tests a new F* version against "important" projects, e.g. Vale, HACL*, etc. Should a new F* commit break one of these projects, the breakage will be flagged as a "Success with breakages" in the CI logs, but the CI system will still report a successful build on the GitHub PR.
It is up to the reviewer to detect such problems and if they occur parse the CI logs and figure out whether this is something that needs attention from you.
Right now, the "Details" link points to a Visual Studio instance that requires manual approval to read the build logs. We plan to make our CI bot post a message on a pull request after each build, with a link to publicly-hosted logs (they exist! ask a reviewer about them if you need them) along with a full report on the aforementioned "Success with breakages" builds.
NOTE: If you're developing a part of F* that changes the OCaml output, you could get stuck due to a dirty worktree; in that case, run:
$ git clean -dfx
$ git checkout -- src/ocaml-output
$ make -C src -j6 ocaml-fstar-ocaml
Caution: You might want to run git clean -dfx only in certain subdirectories, not the entire tree.
To help the review process, and reduce turnaround time, it helps if you can identify good reviewers for it. If you don't know who should review it, one way to obtain a set of candidates is to look at the Git history of the files the PR changes to see who worked on that code in the past.
Aside from the committers on the files that are being changed, various components of the repository have primary maintainers who are expected to review pull requests:
Antoine Delignat-Lavaud
Jonathan Protzenko
Tahina Ramananandro and Nik Swamy
Victor Dumitrescu
Aseem Rastogi, Guido Martinez, Nik Swamy
Aseem Rastogi, Guido Martinez, Nik Swamy
Nik Swamy, Jonathan Protzenko
Aseem Rastogi, Guido Martinez, Nik Swamy
Guido Martinez
Clement Pit-Claudel
Jonathan Protzenko, Victor Dumitrescu
Jonathan Protzenko, Tahina Ramananandro, Nik Swamy
Aseem Rastogi, Tahina Ramananandro
Guido Martinez
Nik Swamy
Many