Trouble setting up a Lean project with SciLean

Stream: lean4

[DSB]

Friends, I'm trying to start a project using SciLean, but I keep getting errors once I try to build it (which can take quite some time... I wonder if there is a way to make such process faster).
Here is my lakefile.toml:

name = "LeanViz"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["LeanViz"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[require]]
name = "proofwidgets"
git = "https://github.com/leanprover-community/ProofWidgets4"
rev = "v0.0.46"

[[require]]
name = "scilean"
git = "https://github.com/lecopivo/SciLean"

[[lean_lib]]
name = "LeanViz"

This worked previously. But I'm guessing the error might be in the Lean version? The documentation in Lean seems to suggest that once a project is created, we should run lake update. Once I do this, I get the newest Lean version in my lean-toolchain (leanprover/lean4:v4.15.0-rc3).
Is this the "proper" way of coding a project? Or should I fix the Lean version somehow to some stable version?

BTW, here is the error:

Some required builds logged failures:
- SciLean.Tactic.CompiledTactics
- Mathlib.Tactic.NormNum.Basic
error: build failed

I have also tried to manually fix the Lean version to "leanprover/lean4:v4.14.0-rc3", but I still get the error.

[Tomas Skrivan]

Just require scilean, you will get mathlib and proofwidgets automatically and correct versions. Set your toolchain to match SciLean's.

If you are on Windows or Mac make sure to update SciLean as a few weeks ago the build was broken and the issue was in SciLean.Tactic.CompiledTactics

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

(In particular, do _not_ explicitly [[require]] mathlib and proofwidgets. Requiring SicLean will pull them in.)