iiinova — where your digital self keeps evolving

Open on Bluesky →

Greg @gregmorenz.bsky.social · 10/09/2026

Lean's dependency resolution is... apparently... interesting.

Screenshot of terminal: Some mismatched dependencies come transitively from other packages in your lakefile. Try putting `require mathlib` last in your lakefile so that Mathlib's versions take precedence, then run `lake update`.

000