diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 26cae09..abfeede 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -28,7 +28,7 @@ structure Options where -- See `pp.implementationDetailHyps` printImplementationDetailHyps: Bool := false -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption - automaticMode: Bool := false + automaticMode: Bool := true deriving Lean.ToJson abbrev OptionsT := ReaderT Options diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index ed33cbb..2decbc1 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.18" +def version := "0.2.19" end Pantograph diff --git a/README.md b/README.md index 27af323..04213ae 100644 --- a/README.md +++ b/README.md @@ -78,9 +78,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `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 - gym, with no resumption necessary to manage your goals. + One particular option for interest for machine learning researchers is the + automatic mode (flag: `"automaticMode"`). By default it is turned on, with + all goals automatically resuming. This makes Pantograph act like a gym, + with no resumption necessary to manage your goals. * `options.print`: Display the current set of options * `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol @@ -153,7 +154,8 @@ with `Pantograph` which mirrors the REPL commands above. It is recommended to call Pantograph via this FFI since it provides a tremendous speed up. The executable can be used as-is, but linking against the shared library -requires the presence of `lean-all`. +requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence +between executable (REPL) commands and library functions. Inject any project path via the `pantograph_init_search` function.