basic_string::substr: __pos > this->size()

Stream: general

[Eric Wieser]

This is a type of error I haven't seem before:

-- basic_string::substr: __pos (which is 2) > this->size() (which is 1)
run_cmd (lean.parser.with_input lean.parser.command_like ".").run

(context: I'm trying to fix open_all_locales to work again in doc-gen)

[Eric Wieser]

A similar error:

import system.io

meta def main : io unit :=
do
  io.run_tactic (lean.parser.with_input lean.parser.command_like "#where").run,
  pure ()

in i_am_not_a_dummy.lean gives

$ lean --run i_am_not_a_dummy.lean
dummy file:1:1: error: invalid import: init
module importing disabled