Skip to content

Better errors when the lean4export version is incorrect #33

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
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions