From e2ad6ce6b3d2f57670313a0a975a3389d46a439f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 6 Sep 2024 21:32:02 -0700
Subject: [PATCH] doc: Documentation for automatic mode

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/README.md b/README.md
index 562f7ac..8bda1ef 100644
--- a/README.md
+++ b/README.md
@@ -90,6 +90,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
+  
+  One particular option for interest for machine learning researchers is the automatic mode.
+  `options.set { "automaticMode": true }`. This makes Pantograph act like
+  LeanDojo, with no resumption necessary to manage your goals.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol