Skip to content

Better errors when the lean4export version is incorrect #33

@robsimmons

Description

@robsimmons

Lean4export includes a header with the version and this version (must? usually needs to?) exactly match the precise version of Lean being used. I got stuck for awhile because I had lean4export for 4.29.0-rc7 on my PATH, unbeknownst to me and with higher priority than the 4.30.0-rc2 lean4export I'd added to the PATH as well, so comparator 4.30.0-rc2 was failing unhelpfully.

Building Challenge
⚠ [2/3] Built Challenge
warning: Challenge.lean:1:8: declaration uses `sorry`
Build completed successfully (3 jobs).
Exporting #[amazing, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Challenge
uncaught exception: process 'landrun' exited with code 1
stderr:
uncaught exception: process 'lean' exited with code 255
stderr:
could not execute external process 'lean'

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions