-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Description
Hi,
I was trying to build the project following the README.md instructions, but I encountered a few inconsistencies regarding the file structure:
- Missing
repldirectory: The README instructs tocd repland runmake. However, there is noreplfolder in the repository. TheMakefileandmain.cappear to be located directly in the root directory now. - Missing
lakefile: The README instructs to runlake buildin the root, but there is nolakefile.leanorlakefile.tomlin the root directory.
It seems the project structure has been refactored (moving repl content to root), but the documentation hasn't been updated yet.
Could you please update the build instructions? Thanks!
Environment:
- OS: macOS
- Lean 4
Metadata
Metadata
Assignees
Labels
No labels