search

lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
309 stars 25 forks source link

Mechanics.olean not building? #1

Closed omrischwarz closed 2 years ago

omrischwarz commented 2 years ago

I'm on a MacBook Air, just installed lean 4 to try to look at Scilean, and I am getting this:

omri@OmriSchwarzsAir SciLean % lake env lean --run examples/HarmonicOscilator.lean

info: mathlib: trying to update ./lean_packages/mathlib to revision 977e6e1ddb5306b83460b3c1c86ca43cac969326 examples/HarmonicOscilator.lean:1:0: error: object file './build/lib/SciLean/Mechanics.olean' of module SciLean.Mechanics does not exist examples/HarmonicOscilator.lean:6:0: error: unknown namespace 'SciLean' examples/HarmonicOscilator.lean:8:12: error: unknown identifier 'ℝ' examples/HarmonicOscilator.lean:8:12: error: unknown constant 'sorryAx' examples/HarmonicOscilator.lean:8:14: error: expected token examples/HarmonicOscilator.lean:10:31: error: expected token examples/HarmonicOscilator.lean:16:3: error: unknown tactic examples/HarmonicOscilator.lean:14:0: error: unsolved goals ℝ : Sort ?u.60 Nat : Sort ?u.64 x✝ : Sort ?u.57 Impl : x✝ m k : ℝ steps : Nat ⊢ ?m.74 m k steps examples/HarmonicOscilator.lean:38:13: error: expected ']'

The build directory does have a lot of code compiled, but it looks like running "lake build" did not compile the Mechanics file.

lecopivo commented 2 years ago

Sorry for such a late reply. Yes indeed SciLean.lean or SciLean/Basic.lean is missing import SciLean.Mechanics. Oddly enough, on my machine this is not necessary and running lake env lean --run examples/HarmonicOscilator.lean somehow builds Mechanics file.

omrischwarz commented 2 years ago

git pull, lake build, lake env lean --run, and it all worked, and is fascinating.

lecopivo commented 2 years ago

Yay! And now your are officially the first person, I'm aware of, that tried and got it running :)