# SF-in-Lean: Instructions for Alpha Testers

## Getting set up

- Fork the [repo](https://github.com/plclub/sf-in-lean) into your own GitHub account.

- Clone your copy onto your local machine.

- Tell your clone where the original repo lives, so you can pick up our changes later:

  ```sh
  git remote add upstream https://github.com/plclub/sf-in-lean.git
  ```

- Install VS Code if you don't already have it.

- Install the Lean 4 extension from its Extensions tab.

- Open your clone in VS Code and open any `.lean` file in the `LF`
  directory. The first time you do this, the extension will offer to
  install Lean itself; accept, and it will fetch the version this book
  needs. (Open a fresh terminal afterwards, so that `elan` and `lake`
  are in your `PATH`.)

## Building the book

- In a terminal, at the top level of your clone:

  ```sh
  make lf-student
  ```

  This builds the _Logical Foundations_ volume in its student form
  (full prose, with solutions elided) and writes two things to
  `_out/lf/student/`:

  + `html/`, an HTML-formatted version of the whole book; and
  + `lean/`, a standalone Lean project holding the same
    chapters as `.lean` files, with solutions to exercises omitted.

- Use `make student` instead if you also want _Type Systems_ (`ts`)
  and _Hoare Logic_ (`hl`). The first build compiles the whole
  dependency tree and takes a while; later builds are incremental.

## Reading the book in a browser

- Start a local HTTP server for the generated HTML files:

  ```sh
  python3 -m http.server 8000 -d _out/lf/student/html
  ```

- Visit <http://localhost:8000> and start reading.

## Working the exercises in VS Code

- To work on exercises, open the generated Lean project as its own
  folder — not as a file inside your clone:

  ```sh
  code _out/lf/student/lean
  ```

  or

  ```sh
  cd _out/lf/student/lean
  code .
  ```

  You can also use File → Open Folder.

  Treat this as a scratch copy: *every `make` regenerates it from the
  Verso sources, overwriting whatever is there.*  Work on your proofs
  here, but keep anything you want to survive somewhere else.

## Making fixes and leaving comments

- Fixes and comments go in the Verso sources at the top level of your
  clone (`LF/`, `TS/`, or `HL/`) and _not_ in the autogenerated files
  under `_out/`. For example, edits to the Basics chapter go in `LF/Basics.lean`.

- If you see opportunities for clear improvements, make fixes directly
  in the appropriate `.lean` file.

- If you want to leave a comment, add it to the `.lean` file like this:

  ```lean
    :::dev "Your Real Name (@your_github_handle)"
    ... Your suggestions ...
    :::
  ```

- Before you submit, check that the chapter you edited still builds:

  ```sh
  lake build LF.Basics
  ```

## Submitting your changes

- Make a GitHub PR for any changes to a given chapter once you finish
  reading it. (We prefer chapter-level PRs so they don't get too large
  or too stale.)

- When you open the PR, leave the "Allow edits by maintainers" box
  checked (it is checked by default). It lets anyone with write
  access to the SF-in-Lean repo push a small fixup directly to your
  branch — a typo, a build fix — instead of asking you to round-trip
  it, which will get your contributions merged faster.

- We are actively working on all the chapters, so if you're reading a
  chapter over a long period, make sure to merge in changes from the
  source repo often.

  ```sh
  git fetch upstream
  git merge upstream/main
  ```