180 Commits

Author	SHA1	Message	Date
Leni Aniva	2f732a7f20	feat: Print goals in `goal.print`	2024-12-11 16:49:52 -08:00
Leni Aniva	7cba8efd54	Merge branch 'dev' into frontend/infotree	2024-12-11 01:14:15 -08:00
Leni Aniva	1527743900	refactor: Optionalize CompilationUnit	2024-12-09 21:00:33 -08:00
Leni Aniva	eb0374dfb3	feat: Collect new constants in repl	2024-12-09 20:57:25 -08:00
Leni Aniva	9a69c48cb2	fix: Integration test failure	2024-12-09 20:42:05 -08:00
Leni Aniva	dd00d803d1	feat: Collect sorry/elab failure boundaries	2024-12-09 20:38:27 -08:00
Leni Aniva	0b4ded1049	fix: Collect sorrys and type mismatches	2024-12-09 20:15:53 -08:00
Leni Aniva	5ef2b5c118	feat: Collect newly defined constants	2024-12-09 19:40:00 -08:00
Leni Aniva	d040d2006c	fix: Do not guard mvar errors in other tactics	2024-12-09 17:58:08 -08:00
Leni Aniva	47d26badc8	feat: Capture mvar errors	2024-12-09 17:30:33 -08:00
Leni Aniva	7fc2bd0d0f	test: Tactic failure on synthesizing placeholder	2024-12-09 08:15:01 -08:00
Leni Aniva	17ab2eafd8	fix: Halt on match guard	2024-12-09 00:03:53 -08:00
Leni Aniva	ea813e5bc5	feat: Monadic info collection	2024-12-08 23:21:36 -08:00
Leni Aniva	0415baaaff	chore: Cleanup old `TestM`	2024-12-05 22:16:20 -08:00
Leni Aniva	a62ac51c37	chore: Remove all redundant filenames	2024-12-05 22:11:37 -08:00
Leni Aniva	7aafd6956f	fix: Capture composite tactic failure	2024-12-05 22:07:21 -08:00
Leni Aniva	2e2658bde7	test: Add test case for composite tactic	2024-12-05 21:35:37 -08:00
Leni Aniva	ebf9ab24f7	Merge pull request 'feat: Pickling goal states' (#129) from serial/pickle into dev ... Reviewed-on: #129	2024-12-05 16:02:25 -08:00
Leni Aniva	105fb7af4b	feat: Goal state pickling	2024-12-05 14:23:55 -08:00
Leni Aniva	0f946880ae	test: Environment pickling	2024-12-04 10:44:33 -08:00
Leni Aniva	7c9b092200	test: Dual monad testing stub	2024-11-30 23:21:16 -08:00
Leni Aniva	a8e7a1a726	feat: Erase macro scopes in sexp	2024-11-26 12:34:52 -08:00
Leni Aniva	4bfd606e2a	Merge branch 'dev' into serial/pickle	2024-11-15 23:09:08 -08:00
Leni Aniva	ee8063e1f5	refactor: Merge all Delation functions	2024-11-08 14:41:24 -08:00
Leni Aniva	0d57027681	refactor: Merge Condensed into Delate	2024-11-08 13:05:48 -08:00
Leni Aniva	1c4f38e5eb	refactor: Rename {Serial,Delate}.lean	2024-11-08 13:04:00 -08:00
Leni Aniva	d7c9590780	feat: Extract used constants from invocation	2024-11-05 14:37:06 -08:00
Leni Aniva	946e688dec	test(frontend): Environment capture	2024-10-12 16:52:36 -07:00
Leni Aniva	8d774d3281	feat: Remove most filters on catalog	2024-10-06 16:12:22 -07:00
Leni Aniva	d0321e72dd	feat: Add message diagnostics to frontend.process	2024-10-05 14:49:17 -07:00
Leni Aniva	10cb32e03f	Merge branch 'dev' into frontend/collect-holes	2024-10-03 11:47:38 -07:00
Leni Aniva	a03eeddc9b	fix: Variable duplication in nested translation	2024-10-03 11:46:09 -07:00
Leni Aniva	530a1a1a97	fix: Extracting `sorry`s from coupled goals	2024-10-03 11:35:54 -07:00
Leni Aniva	143cd289bb	fix: Extraction of sorry's from nested tactics	2024-10-03 01:29:46 -07:00
Leni Aniva	18cd1d0388	fix: Extracting sorrys from sketches	2024-10-02 22:22:20 -07:00
Leni Aniva	4f5950ed78	feat: Convert holes to goals	2024-09-09 12:26:46 -07:00
Leni Aniva	08fb53c020	test: Frontend process testing	2024-09-09 10:18:20 -07:00
Leni Aniva	8e3241c02a	refactor: Move all frontend functions to `Frontend`	2024-09-08 15:02:43 -07:00
Leni Aniva	5e99237e09	fix: Tactics should produce `.syntheticOpaque` goals	2024-09-08 14:13:39 -07:00
Leni Aniva	25bb964604	test: Automatic mode testing ... refactor: Simplified integration test structure	2024-09-08 11:57:39 -07:00
Leni Aniva	a7b30af36b	refactor: Refactor REPL out of main library ... fix: Calc previous rhs not found bug	2024-09-06 22:01:36 -07:00
Leni Aniva	82d99ccf9b	refactor: Use `MVarId` across the board	2024-09-06 21:07:12 -07:00
Leni Aniva	8d2cd6dfc7	fix: Bindings in prograde tactics	2024-09-03 14:15:52 -07:00
Leni Aniva	43e11f1ba3	refactor: Always display isInaccessible	2024-08-17 00:53:38 -07:00
Leni Aniva	e1b7eaab12	fix: Let tactic not bringing binder into scope	2024-08-17 00:47:12 -07:00
Leni Aniva	5b4f8a37eb	refactor: All Tactic/ tactics into MetaM form	2024-08-15 23:41:17 -07:00
Leni Aniva	1e7a186bb1	refactor: MetaM form of define (evaluate)	2024-08-15 23:23:17 -07:00
Leni Aniva	e07f9d9b3f	Merge branch 'dev' into tactic/eval	2024-08-15 22:45:43 -07:00
Leni Aniva	e943a4b065	refactor: Assign into its own tactic	2024-08-15 22:39:40 -07:00
Leni Aniva	431ca4e481	fix: Move elab context to condensed	2024-07-22 17:57:01 -07:00