lake update error

Stream: new members

[Carter Schonwald]

carterschonwald@CarterHydra ~/W/p/a/numerical_lean (main)> lake update mathlib: updating repository './.lake/packages/mathlib' to revision '561ab0981d6df710afb3d34423378152195e3440' error: ./.lake/packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig' error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors

I did a lake update on my first lean4 project (where i'm including mathlib as a dep because why not), whats the cause of this error on the mathlib side?

[Alex J. Best]

You probably need to update your lean-toolchain to match the one in .lake/packages/mathlib/ now also

[Carter Schonwald]

so that'd be an elan update?

[Carter Schonwald]

should i be using lean4 stable or something else channel wise?

[Carter Schonwald]

switching to nightly doesn't work, or is that somethink i do in build.lean or the lake file

[Carter Schonwald]

oh i think i see

[Alex J. Best]

You wont need to update elan most likely. The purpose of elan is to automatically download and install whatever lean version is specified in the file lean-toolchain. So if you update that file you hopefully wont need to issue any elan commands directly. Simply typing lean -v in that directory will be enough to trigger elan to do the right thing

[Carter Schonwald]

ok
now i'm trying to update the example lakefile.lean or whatever
how do i change
def moreServerArgs := #[ (pp.unicode.fun, true),
-- pretty-prints fun a ↦ b
⟨pp.proofs.withType, false⟩, ⟨autoImplicit, false⟩,
⟨relaxedAutoImplicit, false⟩] to be a list of LeanOption?

[Carter Schonwald]

thx youre being very helpful