aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity
226 Commits 10 Branches 21 Tags 50 MiB
Commit Graph

226 Commits

Author SHA1 Message Date
Leni Aniva d94e3086c1
fix: Lean source project for DSP 2024-10-04 18:53:00 -07:00
Leni Aniva 02167afa30
Merge branch 'feat/search' into experiments/dsp 2024-10-04 18:45:30 -07:00
Leni Aniva 82d9f9200e
refactor: Pass in `informal_{stmt,proof}` directly 2024-10-04 18:45:13 -07:00
Leni Aniva 6156f6a297
Merge branch 'feat/search' into experiments/minif2f 2024-10-04 18:43:14 -07:00
Leni Aniva 9d9c7063cd
feat: Remove the goal count restriction on initial state 2024-10-04 18:42:33 -07:00
Leni Aniva cfa9d103b9
feat: Improve feedback and provide default options 2024-10-04 18:41:33 -07:00
Leni Aniva 91c8de2ca0
Merge branch 'main' into experiments/minif2f 2024-10-04 18:39:12 -07:00
Leni Aniva 9fd930380d
feat: Hammer agent for DSP, diagnostics 2024-10-04 18:36:52 -07:00
Leni Aniva 5b176795b2
doc: Diagnostics info at result 2024-10-04 18:04:10 -07:00
Leni Aniva 542784caa2
fix: Trailing comma in reply, remove simp fallback 2024-10-04 18:01:48 -07:00
Leni Aniva 2fae5e97f1
feat: Concise prompts and unhygienic mode 2024-10-04 17:55:32 -07:00
Leni Aniva 20f3011eb4
doc: Improve error message 2024-10-03 15:45:14 -07:00
Leni Aniva b440363105
fix: Skip the commented out test cases 2024-10-03 12:58:39 -07:00
Leni Aniva a30225069a
refactor: All MiniF2F into its own directory 2024-10-03 12:53:07 -07:00
Leni Aniva b3bd3cdde8 feat: Add binder name option in `TacticHave` 2024-10-03 12:31:13 -07:00
Leni Aniva 80a356c75c
feat: Extract Lean code sections from sketches 2024-10-03 12:26:42 -07:00
Leni Aniva f1e996baae
fix: Argument passing in dsp 2024-10-03 12:03:33 -07:00
Leni Aniva c91024f201
chore: Remove dangling link from brando's machine 2024-10-03 01:37:18 -07:00
Leni Aniva 1bbf14ff32
chore: Update to upstream version 2024-10-03 01:33:25 -07:00
Leni Aniva 850fd89e37
fix: `sorry` extraction from sketch 2024-10-03 01:32:43 -07:00
Leni Aniva 3221cfb45b
refactor: Prompt debug printing into dsp main 2024-10-02 16:10:52 -07:00
Leni Aniva 2e8cff0647
Merge branch 'feat/binder_name' into experiments/dsp 2024-10-02 11:11:34 -07:00
Leni Aniva 8ce8e9d389
feat: Add binder name option in `TacticHave` 2024-10-02 11:09:58 -07:00
Leni Aniva ce2d689b03
refactor: Clarify code in dsp 2024-10-02 11:03:00 -07:00
Leni Aniva e942359666
fix: Absolute directories in experiments 
doc: Add documentation about API key
 2024-10-01 11:34:30 -07:00
Leni Aniva 95e90cc026
refactor: Experiments into their own folders 2024-10-01 11:06:01 -07:00
Leni Aniva 22bba57b99
doc: Move SNAP instructions into its own file 2024-10-01 10:57:21 -07:00
Brando Miranda 89a3f5a97d removed confusing file 2024-09-30 10:57:23 -07:00
Brando Miranda d2f53ccc80 examples with leni 2024-09-26 20:20:32 -07:00
Brando Miranda 0d278e1343 Merge branch 'main' into brando 2024-09-26 19:26:59 -07:00
Brando Miranda 5df50a2c60
Update readme.md 2024-09-24 19:03:04 -07:00
Leni Aniva 5effc63d9e
Merge pull request #10 from lenianiva/search 
feat: Add experiment on miniF2F
 2024-09-16 09:49:01 -05:00
Leni Aniva 8d43507901
Merge pull request #13 from lenianiva/frontend/collect-holes 
feat: Collect sorrys command in the server
 2024-09-13 18:22:51 -07:00
Leni Aniva 01ec8fa22a
refactor: Update the experiment repo Lean version, use new load_sorry API 2024-09-13 18:18:53 -07:00
Leni Aniva 8abe689a0a
fix: Make search work with automatic mode 2024-09-13 17:54:11 -07:00
Leni Aniva 6f4c26ecee
Merge branch 'frontend/collect-holes' into search 2024-09-13 17:14:20 -07:00
Leni Aniva 2f70e6d918
Merge branch 'main' into frontend/collect-holes 2024-09-09 19:35:54 -07:00
Leni Aniva d99104cf0e
doc: Update jupyter notebook 2024-09-09 19:28:35 -07:00
Leni Aniva f2de062d11
fix: Versioning in the examples, tactic invocation 2024-09-09 19:04:56 -07:00
Leni Aniva d85cff5264
chore: Library update 2024-09-09 18:49:35 -07:00
Leni Aniva 180f1b1313
Merge pull request #12 from lenianiva/doc/cite 
doc: Add citation format
 2024-09-09 12:41:31 -07:00
Leni Aniva 889aa79c18
Merge pull request #11 from lenianiva/dev 
feat: Automatic mode (for the gym experience)
 2024-09-09 11:38:38 -07:00
Leni Aniva 75ada0b5ad
doc: Add citation format 2024-09-06 22:53:14 -07:00
Leni Aniva 69b01d3879
Merge branch 'main' into dev 2024-09-06 22:34:48 -07:00
Leni Aniva a79fe979fd
feat: Automatic mode (for the gym experience) 2024-09-06 22:26:37 -07:00
Leni Aniva 6d990601c1
Merge pull request #7 from lenianiva/compile/units 
feat: Compilation unit extraction
 2024-09-06 20:51:57 -04:00
Brando Miranda e533bcc088
[self-contained `install.sh` script](https://github.com/brando90/learning_lean/blob/main/install.sh) 
[self-contained `install.sh` script](https://github.com/brando90/learning_lean/blob/main/install.sh)
 2024-07-15 15:06:08 -07:00
Brando Miranda 65dcaa2ea5 pushing dsp to my branch 2024-07-11 15:49:37 -07:00
Leni Aniva 695374a3e4
feat: Example Jupyter notebook 2024-07-01 12:18:00 -07:00
Leni Aniva 27599f7fad
feat: Set lower parameters for search 2024-06-05 15:23:18 -07:00