setting up lean-git-hooks

Stream: general

[Kevin Buzzard]

Is my set-up borked? I don't usually edit mathlib. How do I start again?

git clone git@github.com:leanprover-community/mathlib.git
git fetch --all
git checkout origin/lean-3.4.2
cache-olean --fetch
find src/ -name '*.olean' -exec touch {} +

all work fine. Then

$ setup-lean-git-hooks
This script will copy post-commit and post-checkout scripts to .git/hooks
/home/buzzard/.mathlib/bin/setup-lean-git-hooks: 5: read: Illegal option -n

/home/buzzard/.mathlib/bin/setup-lean-git-hooks: 7: /home/buzzard/.mathlib/bin/setup-lean-git-hooks: [[: not found
Cancelled...
buzzard@bob:~/Lean/lean-projects/mathlib$

[Kevin Buzzard]

$ /bin/sh
$ read -p "Do you want to proceed? " -n 1 -r
/bin/sh: 1: read: Illegal option -n

[Kevin Buzzard]

Editing $HOME/.mathlib/bin/setup-lean-git-hooks so that it starts with /bin/bash works for me on Ubuntu. Is that not an acceptable change in general?

[Kevin Buzzard]

By default I seem to have this:

$ more /home/buzzard/.mathlib/bin/setup-lean-git-hooks
#! /bin/sh
HOOK_DIR=`git rev-parse --git-dir`/hooks
if [ -e $HOOK_DIR ]; then
    echo This script will copy post-commit and post-checkout scripts to $HOOK_DIR
    read -p "Do you want to proceed? " -n 1 -r
...

and this doesn't work for me on Ubuntu 18.04

[Kevin Buzzard]

$ git checkout -b pointwise
Switched to a new branch 'pointwise'
hint: The '.git/hooks/post-checkout' hook was ignored because it's not set as executable.
hint: You can disable this warning with `git config advice.ignoredHook false`.

I need more hints. I have no idea what that means.

[Alex J. Best]

(deleted)

[Reid Barton]

Editing $HOME/.mathlib/bin/setup-lean-git-hooks so that it starts with /bin/bash works for me on Ubuntu. Is that not an acceptable change in general?

This is a good change. On some systems /bin/sh is actually bash; I assume those systems should have /bin/bash as well. Shells that use bash features should not assume /bin/sh is bash.

[Alex J. Best]

https://stackoverflow.com/questions/226703/how-do-i-prompt-for-yes-no-cancel-input-in-a-linux-shell-script gives several posix variants

[Reid Barton]

$ git checkout -b pointwise
Switched to a new branch 'pointwise'
hint: The '.git/hooks/post-checkout' hook was ignored because it's not set as executable.
hint: You can disable this warning with `git config advice.ignoredHook false`.

I need more hints. I have no idea what that means.

.git/hooks/post-checkout is a file

[Kevin Buzzard]

But do I want to disable the warning or do I want to set the executable flag?

[Reid Barton]

I've never used these hooks but presumably if you went to the trouble of setting them up then you want to set the executable flag so that they run.

[Kevin Buzzard]

I went to the trouble of cutting and pasting stuff from here

[Reid Barton]

In that case, I don't understand how you ended up with the file without the executable flag being set, but you want to set it

[Kevin Buzzard]

cache-olean also had x not set

[Reid Barton]

The fact that setup-lean-git-hooks.sh copies the files from ~/.mathlib strikes me as bizarre

[Reid Barton]

The files live in the same repository

[Simon Hudon]

I think that's an oversight. I think I corrected the mistake recently but if your setup is older, you didn't get to take advantage of that fix