make source gives Invalid argument

[EdAyers]

I followed the instructions in the readme, downloading nightly-2022-03-09 which is the latest at time of writing. However I get an error in git clean -xfd in the make source script.

ayers@gentzen:~/mathport$ ./download-release.sh nightly-2022-03-09
[...]
ayers@gentzen:~/mathport$ make build
[...]
ayers@gentzen:~/mathport$ make source
mkdir -p sources
if [ ! -d "sources/mathlib" ]; then \
    cd sources && git clone https://github.com/leanprover-community/mathlib.git; \
fi
cd sources/mathlib && git clean -xfd && git checkout master
warning: failed to remove ./: Invalid argument
make: *** [Makefile:46: mathbin-source] Error 1

I had a look on stack overflow but I couldn't find anything obvious that I have missed.

[gebner]

This is surprising. Can you try running cd sources/mathlib and git clean -xfd and git checkout master manually. I wonder which of these fails.

BTW, you don't need to do make source if you've already done ./download-release.sh. The download release scripts fetches lean 3 sources, ast + tlean files, binported oleans, and synported lean files. To try out mathport, these three steps should be enough:

./download-release.sh nightly-2022-03-09
lake build
./build/bin/mathport config.json Leanbin::data.dlist

[gebner]

This is presumably no longer an issue since the issue hasn't been updated since March. Feel free to reopen if you run into any other issues.

[EdAyers]

oops sorry I forgot about this

[EdAyers]

git clean -xfd fails

[gebner]

Oh, that is unexpected.. I'm not sure if we can do anything about that.

My recommendation is still the same though: don't use make source, just do ./download-release.sh nightly-2022-06-14

[EdAyers]

roger that