Update docs for new download-examples CLI command

Update installation guide and tutorial to recommend `proof_frog
download-examples` as the primary way to obtain examples, replacing
`git clone`. Add download-examples to the CLI reference with full
documentation of --ref and --force options.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: dstebila

manual/cli-reference.md

@@ -7,7 +7,7 @@ nav_order: 60
 
 # CLI Reference
 
-The ProofFrog command-line interface (`proof_frog`) lets you parse, type-check, and verify cryptographic game-hopping proofs entirely from the terminal. Six public commands cover the full workflow from inspecting files to running complete proof verification. If you prefer a graphical environment, a browser-based editor is also available via the `web` command described below.
+The ProofFrog command-line interface (`proof_frog`) lets you parse, type-check, and verify cryptographic game-hopping proofs entirely from the terminal. Seven public commands cover the full workflow from inspecting files to running complete proof verification. If you prefer a graphical environment, a browser-based editor is also available via the `web` command described below.
 
 > **Activate your Python virtual environment first.** All of the commands below assume that the virtual environment in which ProofFrog was installed is activated in the current terminal session. If you opened a new terminal, re-activate it before running any `proof_frog` (or `python -m proof_frog`) command: 
 >
@@ -27,6 +27,7 @@ The ProofFrog command-line interface (`proof_frog`) lets you parse, type-check,
 | [`check`](#check) | Type-check and semantically analyze a FrogLang file. |
 | [`prove`](#prove) | Run proof verification on a `.proof` file. |
 | [`describe`](#describe) | Print a concise interface description of a FrogLang file. |
+| [`download-examples`](#download-examples) | Download the examples repository. |
 | [`web`](#web) | Start the ProofFrog web interface. |
 
 ---
@@ -222,6 +223,43 @@ python -m proof_frog describe --json examples/Primitives/SymEnc.primitive
 
 ---
 
+## download-examples
+
+### Synopsis
+
+```
+python -m proof_frog download-examples [OPTIONS] [DIRECTORY]
+```
+
+### Behavior
+
+Downloads the [ProofFrog examples repository](https://github.com/ProofFrog/examples) into the specified directory (default: `examples`). By default the command downloads the version of the examples that was pinned when your copy of ProofFrog was built, ensuring the examples are compatible with your installed version. Use `--ref` to override this and download a specific commit, tag, or branch instead. If the target directory already exists, the command exits with an error unless `--force` is passed.
+
+### Options
+
+| Flag | Description |
+|------|-------------|
+| `--force` | Overwrite the target directory if it already exists. |
+| `--ref REF` | Git ref (commit SHA, tag, or branch) to download. Defaults to the version pinned at build time. |
+
+### Examples
+
+```bash
+# Download the examples matching your version of ProofFrog into an "examples" directory
+python -m proof_frog download-examples
+
+# Download into a custom directory
+python -m proof_frog download-examples my-examples
+
+# Download the latest main branch instead of the pinned version
+python -m proof_frog download-examples --ref main
+
+# Overwrite an existing examples directory
+python -m proof_frog download-examples --force
+```
+
+---
+
 ## web
 
 ### Synopsis

manual/installation.md

@@ -138,16 +138,13 @@ Do not use `sudo pip install` to work around a `command not found` error. Instal
 
 ## Get the examples
 
-ProofFrog has a companion repository of example proof files. To download it, run:
+ProofFrog has a companion repository of example proof files. The easiest way to get them is with the built-in `download-examples` command:
 
 ```bash
-git clone https://github.com/ProofFrog/examples
+proof_frog download-examples
 ```
 
-This creates an `examples/` directory in your current location containing primitives, schemes, games, and proofs from introductory cryptography.
-
-{: .note }
-If you do not have git installed, you can download the examples as a ZIP file from GitHub: go to [github.com/ProofFrog/examples](https://github.com/ProofFrog/examples), click the green **Code** button, and choose **Download ZIP**.
+This creates an `examples/` directory in your current location containing primitives, schemes, games, and proofs from introductory cryptography. The command downloads the exact version of the examples that matches your installed ProofFrog release.
 
 ## First run
 

manual/tutorial/hello-frog.md

@@ -24,16 +24,13 @@ Make sure you've [installed ProofFrog]({% link manual/installation.md %}).
 
 ## Get the examples
 
-Clone the ProofFrog examples repository:
+Download the ProofFrog examples:
 
 ```bash
-git clone https://github.com/ProofFrog/examples
+proof_frog download-examples
 ```
 
-This creates an `examples/` directory containing primitives, schemes, games, and proofs from introductory cryptography. The rest of this tutorial assumes you cloned it in your current working directory, so that the path `examples/joy/` exists.
-
-{: .note }
-If you do not have git, you can download a zip file containing the examples from the **Code** button on the [examples GitHub page](https://github.com/ProofFrog/examples).
+This creates an `examples/` directory containing primitives, schemes, games, and proofs from introductory cryptography. The rest of this tutorial assumes you ran this command in your current working directory, so that the path `examples/joy/` exists.
 
 ## Launch the web editor