lean-training-data icon indicating copy to clipboard operation
lean-training-data copied to clipboard
verified publisher icon semorrison

`goal_comments`has no effect

Open zzhisthebest opened this issue 1 year ago • 1 comments

I tried lake exe goal_comments Mathlib.Logic.Hydra and lake exe goal_comments Mathlib.Logic.Hydra --edit, but the -- ⊢ x = y aren't inserted at all.

zzhisthebest avatar Mar 28 '25 03:03 zzhisthebest

Solved. Just add supportInterpreter = true after
[[lean_exe]] name = "goal_comments" root = "scripts.goal_comments" in lakefile.toml

zzhisthebest avatar Jun 13 '25 12:06 zzhisthebest