TACAS '25

New Issue

Features that must be ready for TACAS '25

feat: Automatic mode
feat: Reading tactic steps from file
feat: Collecting holes from file
feat: REPL Tactics: have, let, conv, calc

2024-10-14

100% Completed

feat: Let tactic in REPL

#111 by aniva was merged 2024-10-12 16:54:13 -07:00

repl/tactic-let

fix: Delayed MVars in MetaTranslate

#110 by aniva was merged 2024-10-09 18:08:10 -07:00

bug/frontend-translate-delayed-mvar

feat: Catch and print IO errors in REPL

#109 by aniva was merged 2024-10-08 23:50:37 -07:00

repl/io-exception

feat: Error reporting in frontend

#107 by aniva was merged 2024-10-05 22:39:24 -07:00

Report error when frontend parsing fails

#106 by aniva was closed 2024-10-05 22:40:54 -07:00

Metavariable not found bug with sorry collection

#103 by aniva was closed 2024-10-03 11:51:44 -07:00 frontend/collect-holes

feat: Set automaticMode to true by default

#101 by aniva was merged 2024-09-09 17:33:42 -07:00

goal/automatic-mode

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

#99 by aniva was merged 2024-10-03 15:43:01 -07:00

frontend/collect-holes

Parse and enter environment at arbitrary points of the input

#97 by aniva was closed 2024-10-03 15:43:31 -07:00

feat: Automatic Mode

#92 by aniva was merged 2024-09-08 12:25:07 -07:00

feat: Extraction of tactics from compiler

part/Environment

#76 by aniva was merged 2024-05-31 20:23:51 -07:00