search

wellecks / llmstep

llmstep: [L]LM proofstep suggestions in Lean 4.
MIT License
118 stars 15 forks source link

Can not evalate #22

Open Car-pe opened 1 month ago

Car-pe commented 1 month ago

Hello, when I tried to reproduce your results by running bash proofsearch.sh, I encountered the following error while initializing Lean-Dojo. My Lean-Dojo version is 1.1.2. Is there anything wrong?

"ExtractData.lean:375:10: error: invalid field 'mergeIntoOuter?', the environment does not contain 'Lean.Elab.ContextInfo.mergeIntoOuter?' ctx' has type ContextInfo ExtractData.lean:388:10: error: invalid field 'mergeIntoOuter?', the environment does not contain 'Lean.Elab.ContextInfo.mergeIntoOuter?' ctx has type ContextInfo "

yangky11 commented 1 month ago

The issue is likely caused by incompatible versions between LeanDojo, mathlib, or Lean. LeanDojo is not always backward compatible since we try to keep up with the latest version of Lean, and Lean itself is not backward compatible. You could re-try with the latest LeanDojo, but you may also have to use the latest version of mathlib (instead of 5a919533f110b7d76410134a237ee374f24eaaad used by this repo).