aesop not building?

Stream: general

[Alex Meiburg]

I tried running lake update just now, and it's complaining about aesop:

alex@laptop % lake update
mathlib: updating repository './.lake/packages/mathlib' to revision 'a5eb48ce9eb3a014115cc27e69f022a7d2edd44e'
Qq: updating repository './.lake/packages/Qq' to revision '53156671405fbbd5402ed17a79bd129b961bd8d6'
aesop: updating repository './.lake/packages/aesop' to revision '093226b2a8c0cdeac12f1b4786827c67c673b4fb'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5'
Cli: updating repository './.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
importGraph: updating repository './.lake/packages/importGraph' to revision 'e9fb4ecc5d718eb36faae5308880cd3f243788df'
error: ./.lake/packages/aesop/lakefile.toml:1:0: error: unexpected identifier; expected command
error: ./.lake/packages/aesop/lakefile.toml: package configuration has errors

Is it broken at the moment? Is there something I have wrong?

[Alex Meiburg]

Fixed this by updating to lean 4.8.0-rc1. It seems like anything lower than that doesn't understand the toml formatting. It feels a bit strange that, just to use mathlib, I need to be an rc version of lean. :/

[Richard Copley]

Not just that, but the specific toolchain Mathlib was built on. One gets used to it!
The recommendation (for a project that depends directly only on mathlib, at the mathlib repo's default branch) used to be to run

curl -L -O https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain
lake update

And that still works just fine, for that specific case.

[Alex Meiburg]

I see, alright, thanks. :)

[Shreyas Srinivas]

Alex Meiburg said:

Fixed this by updating to lean 4.8.0-rc1. It seems like anything lower than that doesn't understand the toml formatting. It feels a bit strange that, just to use mathlib, I need to be an rc version of lean. :/

the toml support is new

[Shreyas Srinivas]

4.8.0 will be the first stable release in which it lands

[Shreyas Srinivas]

See the announcement

[Patrick Massot]

Alex Meiburg said:

Fixed this by updating to lean 4.8.0-rc1. It seems like anything lower than that doesn't understand the toml formatting. It feels a bit strange that, just to use mathlib, I need to be an rc version of lean. :/

You need an rc version of Lean only if you want to use bleeding edge Mathlib. You can also use the v4.7.0 tag for instance. https://github.com/leanprover-community/mathlib4/releases/tag/v4.7.0

[Alex Meiburg]

Is it silly if I say, I feel like I continually need to use the bleeding edge, because otherwise Loogle becomes useless?

In this most recent case the recent disappearance of eigenvectorMatrix made a lot of lemmas un-loogleable, so if I was to find things reasonably fast I need to upgrade

[Notification Bot]

8 messages were moved from this topic to #general > loogle for other versions of mathlib by Joachim Breitner.