withImportModules causes error

Stream: lean4

[Adam Topaz]

Here is a MWE illustrating the error I am experiencing:

First, here is Main.lean

import Mathlib.Lean.CoreM
import Lean

open Lean

def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  CoreM.withImportModules #[`Mathlib] do
    println! "success!"

and the associated lakefile:

import Lake
open Lake DSL

package «foobar» where

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

lean_exe foobar where
  root := `Main
  supportInterpreter := true

Using lake exe foobar results in the following (unhelpful) error:

uncaught exception: parser 'subscript' was not found

Anyone have any clue about what's causing this error?

[Adam Topaz]

I should say that this is with the most recent mathlib as of now, and the following toolchain: leanprover/lean4:v4.15.0-rc1.

[Adam Topaz]

I should also add that this is not an issue with CoreM.withImportModules. The following Main.lean causes the same error:

import Lean

open Lean

unsafe
def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  withImportModules #[Import.mk `Mathlib false] {} 0 fun _ => do
    println! "success!"

so it seems that there may be a bug in core?

[Patrick Massot]

This issue was reported a lot. If I understand correctly, https://github.com/leanprover/lean4/pull/6325 is related.

[Patrick Massot]

You can search for this error message on Zulip.

[Adam Topaz]

Thanks Patrick. The PR comment gave me a sufficient hint to solve the issue:

import Lean

open Lean

unsafe
def main : IO Unit := do
  searchPathRef.set compile_time_search_path%
  enableInitializersExecution
  withImportModules #[Import.mk `Mathlib false] {} 0 fun _ => do
    println! "success!"

works