Zhang Zihao
Zhang Zihao
@nimasteryang do you still have the preprocessed dataset?the preprocessing is too complex for me
@NikolasBielski hi,friend,do you have the preprocessed dataset?
We meet the same error,and I still don't solve it.
@6AlexMan Have you solved it?It is really annoying. :-(
Solved.Just add `supportInterpreter := true` to the next line of ``` [[lean_exe]] name = "declaration_types" root = "scripts.declaration_types" ``` in lakefile.toml.
你们太强了！
Solved. Just add `supportInterpreter = true` after `[[lean_exe]] name = "goal_comments" root = "scripts.goal_comments" ` in lakefile.toml