Using Mathlib as an import causes leanInk to error

[femtomc]

Description

Attempting to use leanInk with a Lean file which relies on Mathlib, and following the instructions in the README.

My file has the following imports:

import Init.Prelude
import Mathlib.Data.Nat.Basic
import Lean

If I remove these, then leanInk works without failure...

❯ leanInk a ProgrammingLanguageSemantics.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"

But I need these, obviously.

First try, no external deps:

❯ leanInk a ProgrammingLanguageSemantics.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"
ERROR(1): ProgrammingLanguageSemantics.lean:1:0: error: unknown package 'Mathlib'

uncaught exception: Errors during import; aborting

Second try, with external deps, using a lakefile.lean:

❯ leanInk analyze ProgrammingLanguageSemantics.lean --lake lakefile.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"
error: unknown command 'print-paths'
uncaught exception: Using lake failed! Make sure that lake is installed!

Expected behaviour

Expected it to work, as per the README.

Environment information

• Operating System: MacOS 14.0
• Lean version: nightly-2023-08-19
• LeanInk version: 1.0.0
• Alectryon version: 1.5.0-dev

Note that I was able to reproduce on current stable, and by updating the toolchain in leanInk to run on stable.