search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

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

Open mariovagomarzal opened 1 month ago

mariovagomarzal commented 1 month ago

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