add a book

book/.gitignore

@@ -0,0 +1 @@
+book

book/book.toml

@@ -0,0 +1,5 @@
+[book]
+authors = ["Polonius authors"]
+multilingual = false
+src = "src"
+title = "Polonius"

book/src/SUMMARY.md

@@ -0,0 +1,9 @@
+# Summary
+
+- [What is Polonius?](./what_is_polonius.md)
+- [Current status and roadmap](./current_status.md)
+- [Getting started](./getting_started.md)
+- [Generating inputs from rustc](./generate_inputs.md)
+- [Rules](./rules.md)
+  - [Initialization](./rules/initialization.md)
+- [See also](./see_also.md)

book/src/current_status.md

@@ -0,0 +1,26 @@
+# Current status
+
+Polonius has been provisionally integrated into rustc. You can run a nightly
+rustc with the `-Zpolonius` flag to try it out. However, it is not really
+ready for widespread use.
+
+Our current roadmap is as follows:
+
+- **Complete the analysis:** Polonius represents only a portion of the full
+  borrow checker analysis. We would like to move as much as possible from the
+  handwritten Rust code in rustc into the datalog-based approach of polonius.
+- **Optimize:** Naively implementing the polonius rules can be quite
+  slow, so it's important that we optimize the rules and produce a
+  more optimized version.  This will also likely require some special
+  case optimizations to help with specific cases, such as large static
+  constants.
+
+After those two steps are done, and presuming all goes well, we expect
+to replace the existing rustc borrow checker with the polonius
+crate. The crate will continue to exist.
+
+## Want to help?
+
+Check out the [polonius working group][wg] of the compiler team.
+
+[wg]; https://rust-lang.github.io/compiler-team/working-groups/polonius/

book/src/generate_inputs.md

@@ -0,0 +1,24 @@
+# How to generate your own inputs
+
+To run the borrow checker on an input, you first need to generate the
+input facts.  For that, you will need to run rustc with the
+`-Znll-facts` option:
+
+```
+> rustc -Znll-facts inputs/issue-47680/issue-47680.rs
+```
+
+Or, for generating the input facts of a crate using the `#![feature(nll)]` flag:
+
+```
+> cargo rustc -- -Znll-facts
+```
+
+This will generate a `nll-facts` directory with one subdirectory per function:
+
+```bash
+> ls -F nll-facts
+{{impl}}-maybe_next/  main/
+```
+
+You can then run on these directories.

book/src/getting_started.md

@@ -0,0 +1,27 @@
+# Want to run the code?
+
+One of the goals with this repo is to experiment and compare different
+implementations of the same algorithm. You can run the analysis by using `cargo run`
+and you can choose the analysis with `-a`. So for example to run against an example
+extract from clap, you might do:
+
+```bash
+> cargo +nightly run --release -- -a DatafrogOpt inputs/clap-rs/app-parser-{{impl}}-add_defaults/
+    Finished release [optimized] target(s) in 0.05 secs
+     Running `target/release/borrow-check 'inputs/clap-rs/app-parser-{{impl}}-add_defaults/'`
+--------------------------------------------------
+Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
+Time: 3.856s
+```
+
+You could also try `-a Naive` to get the naive rules (more readable,
+slower) -- these are the exact rules described in [the
+blogpost][post]. You can also use `-a LocationInsensitive` to use a
+location insensitive analysis (faster, but may yield spurious errors).
+
+By default, `cargo run` just prints timing. If you also want to see
+the results, try `--show-tuples` (which will show errors) and maybe
+`-v` (to show more intermediate computations). You can supply `--help`
+to get more docs.
+
+[post]: http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/

book/src/rules.md

@@ -0,0 +1,4 @@
+# Rules
+
+These chapters document and explain the Polonius rules, primarily in
+datalog form.

book/src/rules/initialization.md

@@ -0,0 +1 @@
+# Initialization

book/src/see_also.md

@@ -0,0 +1,10 @@
+# See also
+
+There have been a number of blog posts related to Polonius as it evolves:
+
+- http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/
+- ... TODO add the rest ...
+
+The academic work "Oxide" is partially inspired by Polonius:
+
+- [Oxide](https://aaronweiss.us/pubs/draft19-oxide.pdf)

book/src/what_is_polonius.md

@@ -0,0 +1,14 @@
+# What is polonius?
+
+This is a core library that models the borrow check. It implements the analysis
+[described in this blogpost][post].
+
+[post]: http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/
+
+## Why the name "Polonius"?
+
+The name comes from the famous quote ["Neither borrower nor lender
+be"][nblnb], which comes from the character Polonius in Shakespeare's
+*Hamlet*.
+
+[nblnb]: https://literarydevices.net/neither-a-borrower-nor-a-lender-be/