aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Collect holes in Lean file and put them into a GoalState #99

Merged
aniva merged 14 commits from frontend/collect-holes into dev 2024-10-03 15:43:01 -07:00
Conversation 5 Commits 14 Files Changed 20 +8 -6
3 changed files with 8 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit f729a357b9 - Show all commits

2
Pantograph/Protocol.lean
View File

@ -28,7 +28,7 @@ structure Options where
-- See `pp.implementationDetailHyps` -- See `pp.implementationDetailHyps`
printImplementationDetailHyps: Bool := false printImplementationDetailHyps: Bool := false
-- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption -- 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 deriving Lean.ToJson
abbrev OptionsT := ReaderT Options abbrev OptionsT := ReaderT Options

2
Pantograph/Version.lean
View File

@ -1,6 +1,6 @@
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def version := "0.2.18" def version := "0.2.19"
end Pantograph end Pantograph

10
README.md
View File

@ -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 * `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` 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. One particular option for interest for machine learning researchers is the
`options.set { "automaticMode": true }`. This makes Pantograph act like automatic mode (flag: `"automaticMode"`). By default it is turned on, with
gym, with no resumption necessary to manage your goals. 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 * `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`: * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
Start a new proof from a given expression or symbol 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. 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 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. Inject any project path via the `pantograph_init_search` function.