Skip to content

comparator doesn't work when repo contains filenames starting with numbers #17

@mo271

Description

@mo271

While lake etc supports having filename/modules start with numbers, it seems that comparator doens't.

Te recreate the bug, clone https://github.com/mo271/FilesStartingWithNumbers and run

~/FilesStartingWithNumbers (main)> lake env ~/comparator/.lake/build/bin/comparator config_with_problematic_names.json 
Building FilesStartingWithNumbers.«1»
⣾ [0/0] Running job computationPANIC at Lean.modToFilePath.go Lean.Util.Path:46:20: ill-formed import
backtrace:
/home/firsching/.elan/toolchains/leanprover--lean4---v4.27.0/bin/../lib/lean/libleanshared.so(+0x9b23bfe) [0x7f62fe923bfe]
[...rest of stacktrace...]

When changing the escape := false in ./Main.lean to escape := true (suggested by Eric Wieser) one gets a different error:

lake env ~/comparator/.lake/build/bin/comparator config_with_problematic_names.json
Building FilesStartingWithNumbers.«1»
⚠ [2/2] Replayed FilesStartingWithNumbers.«1»
warning: FilesStartingWithNumbers/1.lean:1:8: declaration uses 'sorry'
Build completed successfully (2 jobs).
Exporting #[foo, 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 FilesStartingWithNumbers.«1»
uncaught exception: process 'landrun' exited with code 134
stderr:
PANIC at Lean.modToFilePath.go Lean.Util.Path:46:20: ill-formed import
backtrace:
lean4export(+0x9ba2f9e) [0x55a336c9cf9e]
[rest of the 

but with a further fix to lean4export it seems to work, see leanprover/lean4export#19

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions