extract error

Stream: new members

[Ka Wing Li]

Anyone encounter the following? It happens when I run lake build for normal lean project which imports mathlib.

error: Mathlib/Data/Array/Extract.lean:24:40: Unknown constant `extract_empty_of_start_eq_stop`
error: Mathlib/Data/Array/Extract.lean:27:30: Unknown constant `extract_append_of_stop_le_size_left`
error: Mathlib/Data/Array/Extract.lean:30:31: Unknown constant `extract_append_of_size_left_le_start`
error: Mathlib/Data/Array/Extract.lean:33:35: Unknown constant `extract_eq_of_size_le_stop`

[Kevin Buzzard]

Those theorems were added to batteries 5 days ago and mathlib was updated accordingly. Do you have your system set up correctly? Can you post your lakefile.toml? Are you depending on a version of mathlib and also an incompatible version of Batteries, for example? You should just depend on mathlib and nothing else, it will bring in the correct version of its own dependencies

[Ka Wing Li]

Good question. You remind me of checking lakefile. I just realised that I have included cslib for some experimental work. Removing cslib fixes the problem. Thanks!

[Ka Wing Li]

Btw, I want to ask what if later I need to sync mathlib and cslib?