Unable to build the module

[PoloWlg]

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]

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

[gaetanserre]

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

[PoloWlg]

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]

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