Errors caused by breaking changes in `lean4:v4.3.0-rc2`

[lean-dojo]

Errors caused by breaking changes in `lean4:v4.3.0-rc2`

[yangky11]

adapting to the most recent versions is currently still considered the standard approach

That makes sense!

better FFI support in the future that would elide the need to hard code the build directory at all

Looking forward to it. Thanks!

[yangky11]

leanprover/lean4#2749

[tydeu]

@yangky11

Is there a way to make the project work for both lean4:v4.3.0-rc2 and older versions of Lean? Thanks!

One somewhat hacky way to do this is to condition the paths based on the Lean version definitions (e.g., Lean.version.minor / Lean.version.specialDescr). However, it should probably be noted that Lean is currently still at the point where different versions of Lean are not presumed to be compatible, so adapting to the most recent versions is currently still considered the standard approach.

Also, hopefully, Lake will have better FFI support in the future that would elide the need to hard code the build directory at all in the configuration file.