From 143f2ed7d5d3a8b7cd1004fba9996278f6a1b599 Mon Sep 17 00:00:00 2001
From: Leni Aniva <107011294+lenianiva@users.noreply.github.com>
Date: Thu, 17 Oct 2024 08:44:48 -0700
Subject: [PATCH] doc: Remove stale documentation (#28)

* fix: Remove stale documentation

* doc: Fix git command

* fix: Submodule origin
---
 .gitmodules |  3 +--
 README.md   | 19 ++++++-------------
 2 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/.gitmodules b/.gitmodules
index 6b49ada..56a53a9 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,4 +1,3 @@
 [submodule "src"]
 	path = src
-	url = https://git.leni.sh/aniva/Pantograph.git
-	
\ No newline at end of file
+	url = https://github.com/lenianiva/Pantograph.git
diff --git a/README.md b/README.md
index 96829fc..4246ccf 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@ A Machine-to-Machine Interaction System for Lean 4.
 1. Install `poetry`
 2. Clone this repository with submodules:
 ```sh
-git clone --recursive-submodules <repo-path>
+git clone --recurse-submodules <repo-path>
 ```
 3. Install `elan` and `lake`: See [Lean Manual](https://docs.lean-lang.org/lean4/doc/setup.html)
 4. Execute
@@ -18,24 +18,17 @@ poetry install
 
 ## Examples
 
-For API interaction examples, see `examples/README.md`
-
-An agent based on the `sglang` library is provided in
-`pantograph/search_llm.py`. To use this agent, set the environment variable
-`OPENAI_API_KEY`, and run
-```bash
-python3 -m pantograph.search_llm
-```
+For API interaction examples, see `examples/README.md`. The examples directory
+also contains a comprehensive Jupyter notebook.
 
 ## Experiments
 
 In `experiments/`, there are some experiments:
-1. `minif2f/` is an example of executing a SGLANG based prover on the miniF2F dataset
+1. `minif2f` is an example of executing a `sglang` based prover on the miniF2F dataset
 2. `dsp` is an Lean implementation of Draft-Sketch-Prove
 
-If the experiments don't work, run them in `poetry shell`. The environment
-variable `OPENAI_API_KEY` must be set when running experiments calling the
-OpenAI API.
+The experiments should be run in `poetry shell`. The environment variable
+`OPENAI_API_KEY` must be set when running experiments calling the OpenAI API.
 
 ## Referencing