[codex] Improve new user install and scheduling docs

README.md

@@ -9,6 +9,27 @@ Please see the [documentation](https://egglog-python.readthedocs.io/) for more i
 
 Come say hello [on the e-graphs Zulip](https://egraphs.zulipchat.com/#narrow/stream/375765-egglog/) or [open an issue](https://github.com/egraphs-good/egglog-python/issues/new/choose)!
 
+## Install
+
+With pip:
+
+```shell
+python -m pip install egglog
+```
+
+With uv in a project:
+
+```shell
+uv add egglog
+```
+
+For array examples, install the optional array dependencies:
+
+```shell
+python -m pip install "egglog[array]"
+uv add "egglog[array]"
+```
+
 ## How to cite
 
 If you use **egglog-python** in academic work, please cite the paper:

docs/reference/egglog-translation.md

@@ -395,12 +395,38 @@ After a run, you get a run report, with some timing information as well as wheth
 
 ### Schedules
 
-The `egraph.run` function also takes a `schedule` argument, which corresponds to the `(run-schedule ...)` command in egglog. A schedule can be either:
+`EGraph.run` can run either a bounded number of iterations or a full schedule.
+The bounded form:
 
-- A run configuration, created with `run(limit=..., ruleset=..., *until)`, corresponding to `(run ...)` in egglog
-- Saturating an existing schedule, by calling the `schedule.saturate()` method, corresponding to `(saturate ...)` in egglog
-- A sequence of sequences run one after the other, created with `seq(*schedules)`, corresponding to `(seq ...)` in egglog
-- Repeating a schedule some number of times, created with `schedule * n`, corresponding to `(repeat ...)` in egglog
+```python
+egraph.run(5)
+```
+
+is shorthand for running the default ruleset five times. You can also pass a
+ruleset and optional stop facts:
+
+```python
+egraph.run(10, ruleset=path_ruleset)
+egraph.run(10000, fib(7))
+```
+
+For more control, pass a `Schedule` object. Schedules correspond to egglog's
+`(run-schedule ...)` command and are composed from these Python forms:
+
+| Python | egglog | Meaning |
+| --- | --- | --- |
+| `run()` | `(run)` | Run the default ruleset once. |
+| `run(ruleset)` | `(run ruleset)` | Run one named ruleset once. |
+| `run(ruleset, fact)` | `(run ruleset :until fact)` | Run until the fact is reached. |
+| `schedule.saturate()` | `(saturate schedule)` | Repeat until the schedule stops changing the e-graph. |
+| `schedule * n` | `(repeat n schedule)` | Repeat a schedule exactly `n` times. |
+| `left + right` | `(seq left right)` | Run two schedules in order. |
+| `seq(a, b, c)` | `(seq a b c)` | Run any number of schedules in order. |
+
+Rulesets are schedules, so `egraph.run(path_ruleset)` runs `path_ruleset` once.
+For readability, prefer `run(path_ruleset)` when you are composing a larger
+schedule and `egraph.run(10, ruleset=path_ruleset)` when all you need is a
+bounded run.
 
 We can show an example of this by translating the `schedule-demo.egg` to Python:
 
@@ -470,15 +496,19 @@ step_egraph.check(left(i64(10)), right(i64(9)))
 step_egraph.check_fail(left(i64(11)), right(i64(10)))
 ```
 
-#### Custom Schedulers
+#### Backoff Scheduler
 
-Custom backoff scheduler from egglog-experimental is supported. Create a custom backoff scheduler with `bo = BackOff(match_limit: None | int=None, ban_length: None | int=None)`, then run using `run(ruleset, *facts, scheduler=bo)`:
+The custom backoff scheduler can delay rules that produce too many matches in a
+single scheduler iteration. Create one with
+`bo = back_off(match_limit=None, ban_length=None)`, then pass it to
+`run(ruleset, *facts, scheduler=bo)`.
 
 - `match_limit`: per-rule threshold of matches allowed in a single scheduler iteration. If a rule produces more matches than the threshold, that rule is temporarily banned.
 - `ban_length`: initial ban duration (in scheduler iterations). While banned, that rule is skipped.
-- Exponential backoff: each time a rule is banned, both the threshold and ban length double for that rule (threshold = match_limit << times_banned; ban = ban_length << times_banned).
+- Exponential backoff: each time a rule is banned, both the threshold and ban length double for that rule. After `times_banned` bans, the effective threshold is `match_limit << times_banned` and the ban duration is `ban_length << times_banned`.
 - Fast-forwarding: when any rule is banned, the scheduler fast-forwards by the minimum remaining ban to unban at least one rule before checking for termination again.
 - Defaults: match_limit defaults to 1000; ban_length defaults to 5.
+- `:until` support: custom scheduler runs can use at most one non-equality fact as the stop condition. Equality stop facts and multiple stop facts raise `ValueError`.
 
 For example, this egglog code:
 
@@ -497,7 +527,7 @@ step_egraph.run(
 ```
 
 By default the scheduler will be created before any other schedules are run.
-To control where is instantiated explicitly, use `bo.scope(<schedule>)`, where it will be created before everything in `<schedule>`.
+To control where it is instantiated explicitly, use `bo.scope(<schedule>)`, where it will be created before everything in `<schedule>`.
 
 So the previous is equivalent to:
 
@@ -526,6 +556,11 @@ This would be equivalent to this egglog:
         (run-with bo step_right)))
 ```
 
+That distinction matters because a scheduler carries state. Hoisting one
+scheduler outside `* 10` lets its `times_banned` counters accumulate across all
+ten runs. Placing `bo.scope(...)` inside `* 10` creates a fresh scheduler each
+time, so every iteration starts with the initial `match_limit` and `ban_length`.
+
 ## Check
 
 The `(check ...)` command to verify that some facts are true, can be translated to Python with the `egraph.check` function:

docs/reference/usage.md

@@ -2,22 +2,55 @@
 
 ## Installation
 
-You can install this package with `pip`:
+`egglog` supports Python 3.11 and newer. The examples below create an isolated
+environment first so that new installs do not depend on packages already present
+on your machine.
+
+With `pip`:
+
+```shell
+python3.13 -m venv .venv  # or any supported Python 3.11+
+source .venv/bin/activate
+python -m pip install --upgrade pip
+python -m pip install egglog
+python -c "from egglog import EGraph; EGraph(); print('egglog ok')"
+```
+
+With `uv` in a project:
+
+```shell
+uv init egglog-demo
+cd egglog-demo
+uv add egglog
+uv run python -c "from egglog import EGraph; EGraph(); print('egglog ok')"
+```
+
+With `uv` in a standalone virtual environment:
+
+```shell
+uv venv --python 3.13 .venv  # or any supported Python 3.11+
+uv pip install --python .venv/bin/python egglog
+.venv/bin/python -c "from egglog import EGraph; EGraph(); print('egglog ok')"
+```
+
+If you already have an active environment, the install command is simply:
 
 ```shell
-pip install egglog
+python -m pip install egglog
 ```
 
-To be able to run the array demos:
+To run the array demos, install the optional array dependencies:
 
 ```shell
-pip install egglog[array]
+python -m pip install "egglog[array]"
+uv add "egglog[array]"
 ```
 
-To see interactive widgets:
+From a source checkout for development, use the repo's uv workflow:
 
 ```shell
-pip install anywidget
+uv sync --all-extras
+uv run python -c "from egglog import EGraph; EGraph(); print('egglog ok')"
 ```
 
 It follows [SPEC 0](https://scientific-python.org/specs/spec-0000/) in terms of what Python versions are supported.

docs/tutorials/getting-started.ipynb

@@ -18,30 +18,47 @@
     "\n",
     "## Install egglog Python\n",
     "\n",
-    "First, you will need to have a working Python interpreter. In this tutorial, we will [use `miniconda`](https://docs.conda.io/en/latest/miniconda.html) to create a new Python environment and activate it:\n",
+    "First, you will need a working Python 3.11 or newer interpreter. The safest setup is to create a new environment before installing `egglog`.\n",
+    "\n",
+    "With `pip`:\n",
     "\n",
     "```bash\n",
-    "$ brew install miniconda\n",
-    "$ conda create -n egglog-python python=3.11\n",
-    "$ conda activate egglog-python\n",
+    "$ python3.13 -m venv .venv  # or any supported Python 3.11+\n",
+    "$ source .venv/bin/activate\n",
+    "$ python -m pip install --upgrade pip\n",
+    "$ python -m pip install egglog\n",
     "```\n",
     "\n",
-    "Then we want to install `egglog` Python. `egglog` Python can run on any recent Python version, and is tested on 3.8 - 3.11. To install it, run:\n",
+    "With `uv`:\n",
     "\n",
     "```bash\n",
-    "$ pip install egglog\n",
+    "$ uv init egglog-python-start\n",
+    "$ cd egglog-python-start\n",
+    "$ uv add egglog\n",
     "```\n",
     "\n",
     "To test you have installed it correctly, run:\n",
     "\n",
     "```bash\n",
-    "$ python -m 'import egglog'\n",
+    "$ python -c \"from egglog import EGraph; EGraph(); print('egglog ok')\"\n",
+    "```\n",
+    "\n",
+    "If you used `uv`, run the same check through uv:\n",
+    "\n",
+    "```bash\n",
+    "$ uv run python -c \"from egglog import EGraph; EGraph(); print('egglog ok')\"\n",
+    "```\n",
+    "\n",
+    "We also want to install `mypy` for static type checking. This is not required, but it will help us write correct representations. With pip, run:\n",
+    "\n",
+    "```bash\n",
+    "$ python -m pip install mypy\n",
     "```\n",
     "\n",
-    "We also want to install `mypy` for static type checking. This is not required, but it will help us write correct representations. To install it, run:\n",
+    "With uv, run:\n",
     "\n",
     "```bash\n",
-    "$ pip install mypy\n",
+    "$ uv add --dev mypy\n",
     "```\n",
     "\n",
     "## Creating an E-Graph\n",
@@ -1246,4 +1263,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}

docs/tutorials/tut_4_scheduling.py

@@ -228,7 +228,7 @@ def _(x: Num) -> Iterable[RewriteOrRule]:
 egraph.function_size(Num.__mul__)
 
 
-# Note that any scheudler which doesn't have an explicit scope is bound to the outer loop like:
+# Note that any scheduler which doesn't have an explicit scope is bound to the outer loop like:
 #
 # ```python
 # bo = back_off()

python/egglog/egraph.py

@@ -1560,7 +1560,11 @@ def ruleset(
 @dataclass
 class Schedule(DelayedDeclarations):
     """
-    A composition of some rulesets, either composing them sequentially, running them repeatedly, running them till saturation, or running until some facts are met
+    A composable e-graph schedule.
+
+    Use ``left + right`` to run schedules in sequence, ``schedule * n`` to
+    repeat a schedule a fixed number of times, and ``schedule.saturate()`` to
+    repeat until the schedule stops changing the e-graph.
     """
 
     # Defer declerations so that we can have rule generators that used not yet defined yet
@@ -2065,7 +2069,11 @@ def to_runtime_expr(expr: BaseExpr) -> RuntimeExpr:
 
 def run(ruleset: Ruleset | None = None, *until: FactLike, scheduler: BackOff | None = None) -> Schedule:
     """
-    Create a run configuration.
+    Create a one-step run schedule.
+
+    ``run()`` runs the default ruleset once. ``run(ruleset)`` runs one named
+    ruleset once. Additional facts become ``:until`` stop conditions. A custom
+    ``scheduler`` currently supports at most one non-equality stop fact.
     """
     facts = _fact_likes(until)
     return Schedule(
@@ -2086,6 +2094,9 @@ def back_off(match_limit: None | int = None, ban_length: None | int = None) -> B
     schedule = run(analysis_ruleset).saturate() + run(ruleset, scheduler=back_off(match_limit=1000, ban_length=5)) * 10
     ```
     This will run the `analysis_ruleset` until saturation, then run `ruleset` 10 times, using a backoff scheduler.
+
+    The backend defaults are ``match_limit=1000`` and ``ban_length=5``. Each time
+    a rule is banned, both effective values double for that rule.
     """
     return BackOff(BackOffDecl(id=uuid4(), match_limit=match_limit, ban_length=ban_length))
 
@@ -2110,7 +2121,9 @@ def __repr__(self) -> str:
 
 def seq(*schedules: Schedule) -> Schedule:
     """
-    Run a sequence of schedules.
+    Run any number of schedules in order.
+
+    For two schedules, ``left + right`` is equivalent to ``seq(left, right)``.
     """
     return Schedule(partial(Declarations.create, *schedules), SequenceDecl(tuple(s.schedule for s in schedules)))