Cannot build .olean file on NFS

[Longhao-Chen]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I store mathlib on an NFS server. When I use leanpkg build to build it, there are not have .olean files, but have many files *.olean. lock files with size 0.

Steps to Reproduce

1. Store some package or source files on an NFS server.
2. Build it.

Versions

Lean (version 3.43.0, commit bfce34363b0e, Release)

[ge9]

I experienced the same issue. I also had .tlean.lock and .ast.json.lock files. Their permission was set as -rwsrwsr-t. Using tmpfs (create a temporary directory in /tmp and make a symbolic link) worked.

[PatrickMassot]

@ge9 you are commenting on an issue about a completely obsolete piece of software. Are you sure you really want to use Lean 3?

[ge9]

Actually not, I was just trying to port https://github.com/openai/miniF2F to Lean 4 (since many theorems are missing from https://github.com/yangky11/miniF2F-lean4), with https://github.com/leanprover-community/mathport. I don't think this (possible) bug should be fixed, but posted the message just for someone's help. Sorry

[PatrickMassot]

There is nothing to be sorry about, don’t worry. I was only trying to help you not wasting time on a badly outdated version of Lean.

[PatrickMassot]

And I’m afraid I can confirm nobody will work on this issue. Support for Lean 3 ended almost one year ago.

[ge9]

Okay, that's fine. Thank you for your help!