Error when analyzing a simple file with LeankInk: failed to read file ..., invalid header

[mariovagomarzal]

Description

I'm attempting to analyze a simple file with a sample theorem with leanInk a sample.lean and I get the following error:

Starting Analysis for: "sample.lean"
ERROR(1): sample.lean:1:0: error: failed to read file '/Users/user/.elan/toolchains/4.6.0/lib/lean/Init.olean', invalid header

uncaught exception: Errors during import; aborting

Expected behaviour

Expected to work without the error.

Reproducing the issue

I have built the program from source and added the bin directory to the path. I have created a sample.lean file with the following content:

theorem sample (p : Prop) (hp : p) : p :=
  p

Then, leanInk a sample.lean.

Environment information

• Operating System: macOS Sonoma 14.4.1 (M1 chip)
• Lean version: 4.6.0
• LeanInk version: 1.0.0
• Alectryon version: None