Zulip Chat Archive

import subprocess
import re
comment_git_re = r'\`(' + r'|'.join([
    re.escape("> THIS FILE IS SYNCHRONIZED WITH MATHLIB4."),
    re.escape("> https://github.com/leanprover-community/mathlib4/pull/") + r"[0-9]*",
    re.escape("> Any changes to this file require a corresponding PR to mathlib4."),
    r"",
]) + r")" + "\n"

git_command = ['git', 'diff', '--quiet', f'--ignore-matching-lines={comment_git_re}', 'HEAD^..HEAD']
subprocess.run(git_command, check=True)

and slowly chip away at comment_git_re to work out which part is causing the error

Eric Wieser (Dec 22 2022 at 10:01):

Once we know which part it is, we have a mwe to file a bug against git

Eric Wieser (Dec 22 2022 at 10:01):

But I can't do any of this without access to macOS

Eric Rodriguez (Dec 22 2022 at 11:51):

comment_git_re = r'\`(' + r")" still fails

Eric Wieser (Dec 22 2022 at 11:57):

Does r'\`'?

Eric Rodriguez (Dec 22 2022 at 12:00):

nope

Eric Rodriguez (Dec 22 2022 at 12:00):

as in it doesn't work

Eric Rodriguez (Dec 22 2022 at 12:00):

english is confusing sorry

Eric Wieser (Dec 22 2022 at 12:00):

Does the original work if you replace \` with \A?

Eric Rodriguez (Dec 22 2022 at 12:01):

no - I don't know what either of those does, sadly!

Eric Wieser (Dec 22 2022 at 12:02):

They both mean "start of input"

Eric Wieser (Dec 22 2022 at 12:02):

But in different regex dialects

Eric Wieser (Dec 22 2022 at 12:02):

Shreyas Srinivas said:

http://www.greenend.org.uk/rjk/tech/regexp.html

See here

Eric Rodriguez (Dec 22 2022 at 12:02):

Oh I'm always used to ^ for start of input

Eric Wieser (Dec 22 2022 at 12:03):

That means start of line

Eric Rodriguez (Dec 22 2022 at 12:03):

oh is this multiline?

Eric Wieser (Dec 22 2022 at 12:03):

Its matching against some_line\n

Eric Wieser (Dec 22 2022 at 12:03):

Which has two lines, one before the \n and one empty one after the \n

Eric Wieser (Dec 22 2022 at 12:04):

Having said that, maybe the \` can be safely replaced with ^ since we're explicitly matching the \n

Eric Wieser (Dec 22 2022 at 12:04):

Does that work for you?

Eric Wieser (Dec 22 2022 at 12:04):

Either way, this is worthy of a git bug report since \` works on linux but not macOS

Eric Rodriguez (Dec 22 2022 at 12:05):

mailing lists are such a pain urgh

Eric Rodriguez (Dec 22 2022 at 12:05):

give me a couple minutes though and let me see if I can get a fully-working regex

Eric Rodriguez (Dec 22 2022 at 12:05):

because even removing it I think there's other issues

Eric Rodriguez (Dec 22 2022 at 12:15):

I can't quite track down a fully working regex without basically nuking all of the interesting stuff

Eric Rodriguez (Dec 22 2022 at 12:15):

my hunch is that it's using "old" regexes on mac instead of some PCRE stuff

Eric Rodriguez (Dec 22 2022 at 12:15):

but I'm not too sure what's going on because someone wanted to turn _back_ the support on:
https://www.spinellis.gr/blog/20221012/

Eric Rodriguez (Dec 22 2022 at 12:16):

I think the same guy is the one who put their fix in git itself:
https://github.com/git/git/commit/410a0e520dcc91d13f77fd812f068161859883fc

Eric Rodriguez (Dec 23 2022 at 20:58):

for now, what's a reasonable workaround? wasn't there a server somewhere that kept the output of that script posted somewhere (+ "reasonably" up to date?)

Reid Barton (Dec 23 2022 at 22:09):

https://math.commelin.net/files/port_status.html ?

Eric Rodriguez (Dec 24 2022 at 00:17):

oh sick, the git commands are a bit broken in that file but everything else is great. many thanks johan!

Last updated: Dec 20 2023 at 11:08 UTC