search

gaetanserre / LeanCal

This is a simple calendar manager written in Lean that sends notification using `notify-send` whenever an event is due. Compatible with Waybar.
GNU General Public License v3.0
0 stars 0 forks source link

Unable to build the module #1

Open PoloWlg opened 2 weeks ago

PoloWlg commented 2 weeks ago

While running ./compile.sh, got this error: 

 [6/13] Building Main
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/paulwaligora/.elan/toolchains/leanprover--lean4---v4.9.0/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --json
error: ././././Main.lean:10:5: unexpected token '/'; expected '_', 'rec', identifier or term
error: Lean exited with code 1
Some builds logged failures:
- Main
error: build failed
cp: .lake/build/bin/leancal: No such file or directory
gaetanserre commented 2 weeks ago

I did not try on macOS yet. Could you provide the content of the Main.lean file?

gaetanserre commented 2 weeks ago

Nevermind, it should work now (see #6ab883c).

PoloWlg commented 2 weeks ago

Thanks for your responsiveness, the build is working, however I got a new error: 

Build completed successfully.
cp: cannot overwrite directory ./leancal with non-directory .lake/build/bin/leancal
gaetanserre commented 2 weeks ago

That's weird. Could you provide the output of ls -la in the root directory of the repo?