start_port.sh fails

Stream: mathlib4

[Xavier Roblot]

The script start_port.sh fails midway on my macOS Ventura 13.1 (M1). Here is the full transcript:

Algorithmi:mathlib4 roblot$ ./scripts/start_port.sh Mathlib/Algebra/Regular/Pow.lean
+ set -o pipefail
+ MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
+ PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ TMP_FILE=start_port_tmp.lean
+ mathlib4_path=Mathlib/Algebra/Regular/Pow.lean
+++ echo Mathlib/Algebra/Regular/Pow.lean
+++ tr / .
++ basename Mathlib.Algebra.Regular.Pow.lean .lean
+ mathlib4_mod=Mathlib.Algebra.Regular.Pow
+ mathlib3port_url=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Algebra/Regular/Pow.lean
+ curl --silent --show-error -o start_port_tmp.lean https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Algebra/Regular/Pow.lean
++ grep '^! .*source module '
++ sed 's/.*source module \(.*\)$/\1/'
+ mathlib3_module=algebra.regular.pow
+ curl --silent --show-error https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ grep -F 'algebra.regular.pow: '
+ grep mathlib4#
++ dirname Mathlib/Algebra/Regular/Pow.lean
+ mkdir -p Mathlib/Algebra/Regular
+ mv start_port_tmp.lean Mathlib/Algebra/Regular/Pow.lean
+ git fetch
remote: Enumerating objects: 6, done.
remote: Counting objects: 100% (6/6), done.
remote: Total 6 (delta 5), reused 6 (delta 5), pack-reused 0
Unpacking objects: 100% (6/6), 496 bytes | 70.00 KiB/s, done.
From https://github.com/leanprover-community/mathlib4
   fa20385e..796b4ed7  AD_PORT_Logic_Equiv_Nat -> origin/AD_PORT_Logic_Equiv_Nat
+ branch_name=port/Algebra.Regular.Pow
+ git checkout --no-track -b port/Algebra.Regular.Pow origin/master
Switched to a new branch 'port/Algebra.Regular.Pow'
+ git add Mathlib/Algebra/Regular/Pow.lean
+ git commit -m 'Initial file copy from mathport'
[port/Algebra.Regular.Pow 4c97e99c] Initial file copy from mathport
 1 file changed, 72 insertions(+)
 create mode 100644 Mathlib/Algebra/Regular/Pow.lean
+ sed -i 's/Mathbin\./Mathlib\./g' Mathlib/Algebra/Regular/Pow.lean
sed: 1: "Mathlib/Algebra/Regular ...": invalid command code M

[Xavier Roblot]

The sed on my computer is the standard version included in macOS, as far as I can tell, it doesn't come with a version number...

[Johan Commelin]

https://stackoverflow.com/a/21470675 suggests that we should pass an argument to -i.

[Johan Commelin]

Could you please try editing the script and changing -i into -ibak?

[Xavier Roblot]

It seems that it works. The script terminates without any error

Algorithmi:mathlib4 roblot$ ./scripts/start_port.sh Mathlib/Algebra/Hom/Centroid.lean
+ set -o pipefail
+ MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
+ PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ TMP_FILE=start_port_tmp.lean
+ mathlib4_path=Mathlib/Algebra/Hom/Centroid.lean
+++ echo Mathlib/Algebra/Hom/Centroid.lean
+++ tr / .
++ basename Mathlib.Algebra.Hom.Centroid.lean .lean
+ mathlib4_mod=Mathlib.Algebra.Hom.Centroid
+ mathlib3port_url=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Algebra/Hom/Centroid.lean
+ curl --silent --show-error -o start_port_tmp.lean https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Algebra/Hom/Centroid.lean
++ grep '^! .*source module '
++ sed 's/.*source module \(.*\)$/\1/'
+ mathlib3_module=algebra.hom.centroid
+ curl --silent --show-error https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ grep -F 'algebra.hom.centroid: '
+ grep mathlib4#
++ dirname Mathlib/Algebra/Hom/Centroid.lean
+ mkdir -p Mathlib/Algebra/Hom
+ mv start_port_tmp.lean Mathlib/Algebra/Hom/Centroid.lean
+ git fetch
+ branch_name=port/Algebra.Hom.Centroid
+ git checkout --no-track -b port/Algebra.Hom.Centroid origin/master
M   lake-manifest.json
M   scripts/start_port.sh
Switched to a new branch 'port/Algebra.Hom.Centroid'
+ git add Mathlib/Algebra/Hom/Centroid.lean
+ git commit -m 'Initial file copy from mathport'
[port/Algebra.Hom.Centroid 5f6153dc] Initial file copy from mathport
 1 file changed, 516 insertions(+)
 create mode 100644 Mathlib/Algebra/Hom/Centroid.lean
+ sed -ibak 's/Mathbin\./Mathlib\./g' Mathlib/Algebra/Hom/Centroid.lean
+ echo 'import Mathlib.Algebra.Hom.Centroid'
+ cat Mathlib.lean
+ LC_ALL=C
+ sort
+ mv -f Mathlib.lean.tmp Mathlib.lean
+ git add Mathlib.lean Mathlib/Algebra/Hom/Centroid.lean
+ git commit -m 'Mathbin -> Mathlib; add import to Mathlib.lean'
[port/Algebra.Hom.Centroid 00146657] Mathbin -> Mathlib; add import to Mathlib.lean
 2 files changed, 3 insertions(+), 2 deletions(-)

[Xavier Roblot]

Thanks!

[Reid Barton]

Also see https://stackoverflow.com/questions/4247068/sed-command-with-i-option-failing-on-mac-but-works-on-linux

[Reid Barton]

We assumed when we were writing this script that it would fail somehow on Macs, but we didn't have any way to find out specifically how--thanks for the report.

[Arien Malec]

I installed gnu-sed and aliased to sed ffwiw

[Reid Barton]

It looks like sed -ibak (or better, sed -i.bak) will leave behind a .bak file, that we maybe then want to delete

[Henrik Böving]

Reid Barton said:

We assumed when we were writing this script that it would fail somehow on Macs, but we didn't have any way to find out specifically how--thanks for the report.

In general BSD sed and GNU sed don't exactly like each other, however BSD sed is a strict subset of GNU sed (at least in the way it accepts -i arguments) you can also to the -ibak in GNU sed what you can also do is pass an empty backup file ending! sed -i '' 's/foo/bar/g' file

[Henrik Böving]

I guess if you wanted to test next time you could install some FreeBSD or OpenBSD in a VM and give it a shot :D

[Reid Barton]

Henrik Böving said:

what you can also do is pass an empty backup file ending! sed -i '' 's/foo/bar/g' file

This doesn't work on my (Ubuntu Linux) system

[Henrik Böving]

:(

[Henrik Böving]

I do remember some trick like this working out though, hmmmm

[Henrik Böving]

Ah of course a whitespace mistake: sed -i'' 's/foo/bar/g' file

[Henrik Böving]

Can't make this type of stuff too easy

[Reid Barton]

Isn't sed -i'' the same as sed -i?

[Henrik Böving]

Hmmm, my OpenBSD seems to like it, but that might already have been infected by a GNU sed lets see

[Henrik Böving]

Indeed a GNU sed /o\

[Reid Barton]

I tried on my Haiku VM but it also has GNU sed

[Eric Rodriguez]

fwiw, I ran into this in my Mac as well and just made gnu-sed be the default sed

[Eric Rodriguez]

after brew install gnu-sed there should be a link in /opt/homebrew/opt/gnu-sed/libexec/gnubin (or /usr/local/opt/gnu-sed/libexec/gnubin if Intel mac) so just prepend that to your path and it should work

[Eric Rodriguez]

but it's annoying that this sort of incomaptibility exists :/

[Eric Wieser]

Bash is a terrible language to write cross-platform code

[Reid Barton]

Unfortunately, so are all the others.

[Arthur Paulino]

It's safer to write it in Lean, if possible. Because that would trigger a self-contained run, always using the same executor for everyone, at any point, modulo eventual differences in the execution of binaries generated for each OS (which should always be reported and are in the scope of the core devs)

[Trebor Huang]

Lean OS on the way.

[Reid Barton]

A Lean reimplementation is of course welcome, if someone would like to contribute one.

[Arien Malec]

IIRC, the dependency for Lean implementation is a safe HTTP & TLS client

[Arthur Paulino]

The script already calls curl anyway, so you might as well call it in Lean

[Eric Wieser]

Or we could just bundle it into mathlibtools, since pretty much everyone involved in the port had a working installation of that

[Reid Barton]

I don't have an installation of mathlibtools

[Kevin Buzzard]

You don't use leanproject?

[Reid Barton]

Nope

[Eric Wieser]

How do you get your caches for lean3?

[Reid Barton]

My what?

[Kevin Buzzard]

He already upgraded

[Arien Malec]

Arien Malec said:

I installed gnu-sed and aliased to sed ffwiw

As an update, brew'dgsed still fails

[Eric Rodriguez]

how do you do the alias?

[Arien Malec]

alias sed=gsed

% which sed
sed: aliased to gsed
% sed --version
gsed (GNU sed) 4.9

[Eric Rodriguez]

do you export that?

[Reid Barton]

Judging from your prompt, you might be using a non-sh shell. Then I'm not sure if whatever customization you have set up will apply to start_port.sh.

[Arien Malec]

I'm using zsh which is standard for OS X; I elided the computer name, etc from the prompt. But yeah, it's possible my alias only takes effect for zsh...

[Arien Malec]

and that the shell script defaults to bash -- sigh.

[Eric Rodriguez]

Eric Rodriguez said:

after brew install gnu-sed there should be a link in /opt/homebrew/opt/gnu-sed/libexec/gnubin (or /usr/local/opt/gnu-sed/libexec/gnubin if Intel mac) so just prepend that to your path and it should work

have you tried adding this to your path @Arien Malec ?

[Arien Malec]

the issue is where -- I think I can update this so deeply that /bin/sh picks it up as well.

[Reid Barton]

Try adding the alias line to .bashrc? or put a gnu sed on the path, yeah

[Eric Rodriguez]

no, it's on zshrc

[Eric Rodriguez]

bash doesn't run bashrc when it runs only a script, just for interactive sessions

[Reid Barton]

Oh whoops you're right

[Eric Rodriguez]

i've dealt with this fiasco already so I know the rundown :b

[Arien Malec]

added to /etc/paths :fingers_crossed:

[Eric Rodriguez]

note that now you'll need gnu awk too (brew install gawk) and also similar extra steps

[Kevin Buzzard]

I'm on Ubuntu 20.04 and the script doesn't work for me:

...
+ sed -i '/^import/{s/[.]Gcd/.GCD/g; s/[.]Modeq/.ModEq/g; s/[.]Nary/.NAry/g; s/[.]Peq/.PEq/g; s/[.]Pfun/.PFun/g; s/[.]Pnat/.PNat/g; s/[.]Smul/.SMul/g; s/[.]Zmod/.ZMod/g}' Mathlib/CategoryTheory/Bicategory/Functor.lean
+ awk '{do {{if (match($0, "^  by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' Mathlib/CategoryTheory/Bicategory/Functor.lean
awk: line 1: syntax error at or near if
awk: line 1: syntax error at or near }

I have

buzzard@buster:~/lean-projects/mathlib4$ awk -W version
mawk 1.3.4 20200120
Copyright 2008-2019,2020, Thomas E. Dickey
Copyright 1991-1996,2014, Michael D. Brennan

random-funcs:       srandom/random
regex-funcs:        internal
compiled limits:
sprintf buffer      8192
maximum-integer     2147483647

What's the recommended way to proceed? (mildly reluctant to upgrade to Ubuntu 22)

[Matthew Ballard]

Do you have gawk?

[Kevin Buzzard]

I just installed it and my guess is that this will fix the probem -- awk -W version is now telling me gawk. But I can't run the script to check because it says "this file already exists" and I have now already looked at the script and manually done the other stuff which it was supposed to do.

[Matthew Ballard]

I was running the script on macos where awk is not gawk. Add the file to Mathlib.lean and change Mathbin to Mathlibto get into a reasonable state.

[Matthew Ballard]

Otherwise I didn't miss much.

[Johan Commelin]

The biggest benefit for reviewers is that the first three commits are very predictable. I always review commits [4..n] in the github ui, which shows the "actual changes" compared to mathport output. I think it's important to have a clear distinction between mathport output and user changes. The predictability of the commits that the script makes helps with this.

[Matthew Ballard]

I think that still exists if awk does not fire

[Matthew Ballard]

There is no restart_port.sh correct?

[Jireh Loreaux]

There is a flag for that, --restart

[Jireh Loreaux]

(I think)

[Matthew Ballard]

Disregard me!

[Matthew Ballard]

It does add the initial file copy from mathport commit.

[Matthew Ballard]

Hmm. I can't find a restart flag

[Johan Commelin]

I think there is a PR that adds --restart but it hasn't been merged yet.

[Eric Wieser]

awk is also a bad version on gitpod

[Yury G. Kudryashov]

@Eric Wieser , after !4#2598, start_port.sh fails for me. More precisely,

• It doesn't add the new file to Mathlib.lean in the "automated fixes" commit.
• It leaves the working tree with staged changes that revert new commits.
• This :up: looks especially strange if HEAD ≠ origin/master.

[Eric Wieser]

The first point has an open PR

[Eric Wieser]

I think I know how to fix the second

[Eric Wieser]

The checkout needs to happen without the env vars

[Johan Commelin]

Eric Wieser said:

The first point has an open PR

Which one?

[Eric Wieser]

The one I PMed you this morning

[Johan Commelin]

Ooops, I missed that PM somehow :see_no_evil:

[Johan Commelin]

It's on the queue

[Eric Wieser]

!4#2639 is the fix to the other half

[Jon Eugster]

With a wrong awk version start_port.sh fails currently:

Jeremy Tan said:

awk: line 1: syntax error at or near if
awk: line 1: syntax error at or near }

As far as I can tell awk is only used to remove the newlines in := by. Since this isn't essential to start porting and can easily be done manually (or even later like in !4#1532) could we make this part of the script optional:

Here's a suggestion PR: !4#2777

(@Eric Wieser who made the last few improvements to the script)

[Eric Wieser]

I don't think we should make any of the porting script optional

[Eric Wieser]

We could rewrite it to not use awk

[Calvin Lee]

Hi, experienced awk user here
if I'm understanding the script correctly, there appears to be a semicolon missing after the while.
I'm going to test this with gawk and mawk for regressions, but I think it should work: !4#2794

[Calvin Lee]

let me know if this is a desired solution (e.g. making awk invocations posix compatible) and I'll test
otherwise if y'all want to get rid of awk alltogether I'll just abandon this PR

[Thomas Murrills]

This looks great! Btw, I tested your posix-compliant awk program with MacOS's default awk (which is neither mawk nor gawk, I believe?) and it now works there too. (The earlier version fails.) I'll mention this on the PR as well.

(Also, maybe the PR title should say "posix-compliant" or something instead of just mawk? It seems like it's a more general fix!)

[Thomas Murrills]

Imo you may as well turn it into a real PR, test it with gawk and mawk as mentioned to confirm it behaves the same as the earlier script, and put it out for review; then someone with merge powers might see it and just hit merge. If it works as advertised, I can't think of any reason we wouldn't want it asap, even if we plan to move away from awk! :)

[Thomas Murrills]

(In that case you should probably explain why it fixes things in the PR description in case they haven't seen zulip, though.)

[Calvin Lee]

good grief. we're going to have issues with mawk for other reasons. In particular, it doesn't support unicode:
image.png
if this much of a deviation (too-conservative line-length calculation in a weird unsupported awk) the PR might not make sense
let me test it in macOS awk and see what happens

[Thomas Murrills]

Oops, I didn’t consider that that might be an issue! (Tested it locally on macOS with a couple Unicode characters and it seemed okay, but your tests will probably be more thorough!)

[Calvin Lee]

I picked a long file, and ended up with two definitions that were calculated differently. I have a solution but it's not pretty image.png

[Thomas Murrills]

Hmmm…maybe a rewrite is in order after all :/ What’s the solution you’re thinking of?

[Thomas Murrills]

Or: why does this happen? I thought posix-compliance meant things were cross-platform; is there a --posix flag or something?

[Calvin Lee]

unicode-compliance in awk is... fairly undefined. Kerningham himself just (last year) added unicode support to upstream AWK

[Thomas Murrills]

Ah, wow

[Thomas Murrills]

I keep thinking “if only there were a cross-platform way to run awk!” but…I guess that’s just gawk…? 😅

[Thomas Murrills]

If we can’t get different versions of awk to agree and can’t immediately find a cross-platform way to rewrite it in something else, maybe the best we can hope for is something at the top of the file which checks that you have gawk and exits with a message like “Please install gawk. See [section] of the porting wiki for details” if you don’t.

[Thomas Murrills]

(Also, is gawk always accessible as gawk if you have it? It might be good to replace awk with gawk if we can, so that people don’t have to actually change their default awk.)

[Jeremy Tan]

Thomas Murrills said:

If we can’t get different versions of awk to agree and can’t immediately find a cross-platform way to rewrite it in something else

Just accept the PR first – the line length issue, if it ever pops up, is for humans to resolve, not awk

[Calvin Lee]

tried to test on macOS but ran into sed issues as well (before reaching the awk)

[Thomas Murrills]

Jeremy Tan said:

Thomas Murrills said:

If we can’t get different versions of awk to agree and can’t immediately find a cross-platform way to rewrite it in something else

Just accept the PR first – the line length issue, if it ever pops up, is for humans to resolve, not awk

If line length is a problem for humans but by positioning isn’t, then we should just remove the line length check from the awk program.

(My understanding is that currently some systems might think that some lines with < 98 characters actually have more than 98 characters, and therefore refrain from repositioning the by, right? Worst that happens is some lines are long.)

[Jeremy Tan]

yeah, we can do that too

[Thomas Murrills]

Calvin Lee said:

tried to test on macOS but ran into sed issues as well (before reaching the awk)

Oh, yeesh, I just tested the awk program in isolation. Does sed rely on awk under the hood? What’s the deal there?

[Jeremy Tan]

The whole script works on my Ubuntu laptop though

[Calvin Lee]

ok as expected, macOS awk result is same as mawk due to unicode issues.
Also I fixed sed on macOS, would these changes be appreciated too?

[Calvin Lee]

ok nevermind it's impossible lol https://stackoverflow.com/questions/5694228/sed-in-place-flag-that-works-both-on-mac-bsd-and-linux

[Thomas Murrills]

Lol I was just looking at that same question

[Thomas Murrills]

Could it be rewritten in gawk somehow? (Since we’re making people install it anyway?)

[Jeremy Tan]

If that's the case, just write another Python scriptoid to handle the by formatting

[Thomas Murrills]

I’m talking about the sed issues

[Calvin Lee]

awk isn't any better at "in-place editing" as sed (this also isn't one of sed's strong-suits, as a "stream editor")
you'd have to awk <SCRIPT> -f file > file which is also possible with sed

[Thomas Murrills]

Hmm, ok!

my sense is that we should balance being robustly cross-platform with being easy to review—if such a modification of the sed script is probably fine for Linux, mac, and windows, and is close to the original, I think that’s a good short-term fix.

[Moritz Doll]

The script now fails on my machine with

  File "/home/moritz/coding/lean/mathlib4/scripts/fix-line-breaks.py", line 6
    with (open(sys.argv[1], "r", encoding="utf-8", newline="\n") as f,
                                                                 ^
SyntaxError: invalid syntax

Python version is 3.8.10

[Eric Wieser]

Oops, looks like we committed 3.10 syntax

[Eric Wieser]

Removing the outermost parentheses and adding a \ on the end of the line should fix it

[Moritz Doll]

yes, that works

[Moritz Doll]

!4#2982

[Eric Wieser]

Heh, it was actually @Julian Berman who requested this feature long ago: https://github.com/python/cpython/issues/56991

[Julian Berman]

Pfft oh man yeah that... was an ordeal.

[Eric Wieser]

I know the feeling, two of my PRs took 5 years to be merged (mostly spent waiting for an expert in something everyone had forgotten about)

[Julian Berman]

So, the decimal module? Though that nonsense applies to lots of things so my silly guess might not be good for much. Working on CPython is a bit like slow torture though :)

[Eric Wieser]

Nope, ctypes

[Peter Nelson]

I'm not sure if this is the same issue, but I'm having trouble with start_port.sh in a way that looks similar (M1 Mac).

peternelson@v1040-wn-rt-a-74-248 mathlib4 % ./scripts/start_port.sh Mathlib/Data/Set/Ncard.lean
remote: Enumerating objects: 37, done.
remote: Counting objects: 100% (37/37), done.
remote: Compressing objects: 100% (28/28), done.
remote: Total 37 (delta 23), reused 12 (delta 9), pack-reused 0
Unpacking objects: 100% (37/37), 25.73 KiB | 731.00 KiB/s, done.
From https://github.com/leanprover-community/mathlib4
   151c25bc..329fc545  master     -> origin/master
   5fdf5610..707a3952  port/Analysis.Analytic.Composition -> origin/port/Analysis.Analytic.Composition
   ffaf90da..39a5d650  port/MeasureTheory.Integral.Bochner -> origin/port/MeasureTheory.Integral.Bochner
   329fc545..593b929e  staging    -> origin/staging
Checking out a new branch in a temporary working tree
Downloading latest version from mathlib3port
Applying automated fixes
sed: 1: "Mathlib/Data/Set/Ncard. ...": invalid command code M

Am I doing something wrong?

[Ruben Van de Velde]

That looks like a case of an incompatible sed - there's been previous discussion here you might be able to find

[Peter Nelson]

Ok thanks - a little more googling helped me figure out exactly what to do. For posterity, I first did
brew install sed, then did PATH="/usr/local/opt/gnu-sed/libexec/gnubin:$PATH". After that, it was ok.

[Oliver Nash]

As another Mac user, I had the same issue and used (essentially) the same solution. The problem seems to be that Mac OS provides BSD sed whereas the script relies on GNU sed. What a time to be alive!