What does "import runtime" do?

Stream: lean4

[Eric Wieser]

I notice that import runtime Lean is legal syntax, but it doesn't seem to actually do anything in the web editor; is there any documentation on this feature?

[Mario Carneiro]

I think it's vestigial

[Henrik Böving]

Doing some basic grepping it sets the runtimeOnly flag in docs#Lean.Import which has precisely one location where it is used:

partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
  for i in imports do
    if i.runtimeOnly || (← get).moduleNameSet.contains i.module then
      continue
    modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
    let mFile ← findOLean i.module
    let (mod, region) ← readModuleData mFile
    importModulesCore mod.imports
    modify fun s => { s with
      moduleData  := s.moduleData.push mod
      regions     := s.regions.push region
      moduleNames := s.moduleNames.push i.module
    }

so for now it noops the import

[Eric Wieser]

Are the proposed semantics defined? If not, should runtimeOnly be removed entirely?