importing binported oleans

Stream: mathlib4

[David Renshaw]

The blog post from December says:

binport constructs Lean 4 .olean files, from Lean 3 .olean files. It largely works, and means that you can import mathlib3 content into Lean 4 (as long as you don't expect to have source files!) This is what lets us do things like:

import Mathbin

#lookup3 algebraic_geometry.Scheme
#check AlgebraicGeometry.Scheme

Should this still be possible? I haven't been able to get it to work.