`lake build MyProject.37`: can't build files with numeric names
Open
Nobody has claimed this yet.
bug
Lake
P-medium
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 17h
- Merged PRs (30d)
- 175
Description
To reproduce:
lake new Numeric
cd Numeric
touch Numeric/s37.lean
lake build Numeric.s37
works, printing:
[0/1] Building Numeric.s37
but
touch Numeric/37.lean
lake build Numeric.37
errors with:
PANIC at Lean.modToFilePath.go Lean.Util.Path:38:20: ill-formed import
error: 'Numeric.37': no such file or directory (error code: 2)
file:
And without #2756 it's annoying to work around.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Reproduce the issue with the lake new Numeric project and the Numeric/37.lean module, then inspect the Lean.modToFilePath.go failure reported at Lean.Util.Path:38:20. The work is done when lake build Numeric.37 builds the numeric-named file without the panic or missing-file error.
Written by the indexing model from the issue text.
Assessment
- Domain
- build-system, compilers
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 45/100