## Stream: general

### Topic: setting up lean-git-hooks

#### Kevin Buzzard (Nov 16 2019 at 21:47):

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 (Nov 16 2019 at 21:48):

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


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 (Nov 16 2019 at 21:51): 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

$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 (Nov 16 2019 at 21:58): (deleted) #### Reid Barton (Nov 16 2019 at 21:59): 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 (Nov 16 2019 at 22:00):

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 (Nov 16 2019 at 22:02):

\$ 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 (Nov 16 2019 at 22:03):

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

#### Reid Barton (Nov 16 2019 at 22:04):

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 (Nov 16 2019 at 22:06):

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

#### Reid Barton (Nov 16 2019 at 22:07):

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 (Nov 16 2019 at 22:08):

cache-olean also had x not set

#### Reid Barton (Nov 16 2019 at 22:10):

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

#### Reid Barton (Nov 16 2019 at 22:10):

The files live in the same repository

#### Simon Hudon (Nov 17 2019 at 00:31):

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

Last updated: May 08 2021 at 10:12 UTC