Zulip Chat Archive

Stream: general

Topic: setting up lean-git-hooks


view this post on Zulip 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$

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 21:50):

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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 21:55):

$ 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.

view this post on Zulip Alex J. Best (Nov 16 2019 at 21:58):

(deleted)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:06):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:08):

cache-olean also had x not set

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 16 2019 at 22:10):

The files live in the same repository

view this post on Zulip 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