[m-rev.] for review: git hook improvements

[Peter Wang]

On Sat, 09 Mar 2024 18:34:58 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter.
> 
> I am not 100% sure that I understand correctly how
> the hook should be used, so I would appreciate it
> if you checked my slightly more detailed documentation
> of the script.
> 
> Zoltan.

> Improve git_hooks.

Change it to:

    Improve pre-commit git hook.

> 
> git_hooks/update_copyright.pre-commit:
>     Document the operation of this script in more detail.
> 
>     Document the use of the new Makefile, and of the new environment
>     variable that can be used to avoid redundant copies of the update_copyright
>     program's executable.
> 
> git_hooks/Makefile:
>     Add a trivial makefile to shorten the build and clean commands.

You didn't add the Makefile.

> 
> git_hooks/update_copyright.m:
>     Merge contiguous year ranges in copyright lines.


> diff --git a/git_hooks/update_copyright.m b/git_hooks/update_copyright.m
> index 229076c23..0c246356b 100644
> --- a/git_hooks/update_copyright.m
> +++ b/git_hooks/update_copyright.m
> @@ -305,11 +312,27 @@ parse_range(Str, Range) :-
>          Range = years(N1, N2)
>      ).
>  
> -:- pred is_whitespace_or_comma(char::in) is semidet.
> +:- pred merge_adjancent_ranges_if_possible(
> +    list(year_range)::in, list(year_range)::out) is det.
>  

adjacent

> diff --git a/git_hooks/update_copyright.pre-commit b/git_hooks/update_copyright.pre-commit
> index 5b6bcf161..240834870 100755
> --- a/git_hooks/update_copyright.pre-commit
> +++ b/git_hooks/update_copyright.pre-commit
> @@ -1,19 +1,44 @@
>  #!/usr/bin/env bash
>  #
> -# You can copy/symlink this script to .git/hooks/pre-commit.
> -# It will update the Copyright lines of all files that are going to be
> -# modified in the commit, before the commit is made.
> +# This script is designed to the Copyright lines of all files

to update

> +# that are going to be modified in the commit in a workspace,
> +# before the commit is made.
> +#
> +# If ${ws} is the pathname of a workspace, then you enable this script
> +# for that workspace by
> +#
> +# - compiling update_copyright.m to an executable, and
> +# - copying or symlinking this script to ${ws}/.git/hooks/pre-commit.
> +#
> +# The first step can be done by either of the commands
>  #
> -# You need to compile the update_copyright.m program:
>  #   mmc --mercury-linkage static update_copyright.m
> +#   make update_copyright
> +#
> +# The unneeded intermediate files from the first step can cleaned up by either
> +# of the commands
>  #
> -# You can clean the intermediate files with:
>  #   git clean -fx 'update_copyright.*' 'update_copyright_init.*'
> +#   make clean
>  #

We only need to describe the make commands.

> +# By default, this script requires the executable git_hooks/update_copyright
> +# to be present in the workspace. You can avoid having a duplicate copy
> +# of that executable in every workspace by
> +#
> +# - putting that executable in some central location, and
> +# - setting up the environment variable UPDATE_MERCURY_COPYRIGHT
> +#   to point to that central location.

I suggest:

- setting the environment variable UPDATE_MERCURY_COPYRIGHT
  to invoke that executable.

> +#
> +
>  set -e
>  
>  rootdir=$( git rev-parse --show-toplevel )
> -update_copyright="$rootdir/git_hooks/update_copyright"
> +if test "${UPDATE_MERCURY_COPYRIGHT}" != ""
> +then
> +    update_copyright="${UPDATE_MERCURY_COPYRIGHT}"
> +else
> +    update_copyright="$rootdir/git_hooks/update_copyright"
> +fi

Obviously that could also be:

    update_copyright=${UPDATE_MERCURY_COPYRIGHT-"$rootdir/git_hooks/update_copyright"}

>  # Only continue if the update_copyright program has been compiled.
>  if test ! -x "$update_copyright"

I suggest:

    # Only continue if the update_copyright program is available.
    command -v "$update_copyright" >/dev/null || exit 0

Then UPDATE_MERCURY_COPYRIGHT does not necessarily have to point to an
executable file, but can also be a command on the PATH.

Peter