fix: Shield tactics from the environment generated by frontend.process #199

aniva · 2025-05-01T08:59:15-07:00

aniva commented

2025-05-01 08:59:15 -07:00

exact? should fail when applied to 1 + 2 = 2 + 3, so this is correct:

goal.start {"expr": "1 + 2 = 2 + 3"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "exact?"}

but this is not

frontend.process {"file": "theorem lenislemma : 1 + 2 = 2 + 3 := by sorry", "readHeader": false, "inheritEnv": false, "invocations": false, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "exact?"}

same incorrect behaviour shows up when we replace by sorry with sorry.

feat: Add message log even in the successful case of tactic execution
fix: Prevent tactics from using constants when they're in the constants definitions

`exact?` should fail when applied to `1 + 2 = 2 + 3`, so this is correct: ```jsonl goal.start {"expr": "1 + 2 = 2 + 3"} goal.tactic {"stateId": 0, "goalId": 0, "tactic": "exact?"} ``` but this is not ```jsonl frontend.process {"file": "theorem lenislemma : 1 + 2 = 2 + 3 := by sorry", "readHeader": false, "inheritEnv": false, "invocations": false, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false} goal.tactic {"stateId": 0, "goalId": 0, "tactic": "exact?"} ``` same incorrect behaviour shows up when we replace `by sorry` with `sorry`. - feat: Add message log even in the successful case of tactic execution - fix: Prevent tactics from using constants when they're in the constants definitions

aniva added the

part/Frontend

category

bug

labels 2025-05-01 08:59:16 -07:00

aniva self-assigned this 2025-05-01 08:59:16 -07:00

aniva added 1 commit 2025-05-01 08:59:16 -07:00

170099525c

test: Add tactic edge cases test

aniva added 1 commit 2025-05-01 09:21:53 -07:00

49d06e8c05

fix: Shield tactics from newly created environment