26 Commits

Author	SHA1	Message	Date
Leni Aniva	a281557d0a	Merge branch 'misc/version' into experiments/dsp	2024-10-06 22:06:07 -07:00
Leni Aniva	034fd458e3	chore: Update Pantograph and Lean version to 4.12	2024-10-06 22:04:10 -07:00
Leni Aniva	7770c0fb59	feat: Error feedback in DSP	2024-10-06 19:14:38 -07:00
Leni Aniva	159da09c9d	Merge branch 'main' into experiments/minif2f	2024-10-05 22:31:22 -07:00
Leni Aniva	48f2f2cb5a	feat: Add handling for errors in compilation	2024-10-05 15:38:35 -07:00
Leni Aniva	104d2451b1	feat: Add more automation to `HammerAgent`	2024-10-05 01:26:19 -07:00
Leni Aniva	97f22ed67a	feat: Output experiment result into folder	2024-10-05 01:23:38 -07:00
Leni Aniva	0ab29e11cd	Merge branch 'experiments/dsp' into experiments/minif2f	2024-10-05 01:05:25 -07:00
Leni Aniva	1fde034dce	fix: Remove barrier that halts problem iter	2024-10-05 00:59:28 -07:00
Leni Aniva	3b76080495	feat: Search on minif2f	2024-10-04 21:55:47 -07:00
Leni Aniva	d94e3086c1	fix: Lean source project for DSP	2024-10-04 18:53:00 -07:00
Leni Aniva	82d9f9200e	refactor: Pass in `informal_{stmt,proof}` directly	2024-10-04 18:45:13 -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	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	3221cfb45b	refactor: Prompt debug printing into dsp main	2024-10-02 16:10:52 -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	01ec8fa22a	refactor: Update the experiment repo Lean version, use new load_sorry API	2024-09-13 18:18:53 -07:00