import diff bot

Stream: mathlib4

[Kim Morrison]

@Damiano Testa, a bug report. When I try to follow the advice of the import diffs bot:

You can run scripts/import_trans_difference.sh all locally to see the whole output.

on a macos system, I get

awk: calling undefined function asort
 input record number 5612, file transImports2.txt
 source line number 24


<details><summary>Import changes for all files</summary>

|Files|Import difference|
|-|-|

</details>

[Damiano Testa]

Let me try: I only used it on Linux and it has only run on CI, as far as I know, so no MacOS testing.

[Damiano Testa]

Ah, I think that asort is an internal of awk that is not part of the MacOS distribution of awk...

[Kim Morrison]

I guess we better rewrite it in Lean, then. :-)

[Damiano Testa]

Let me look at the script: the shell functions are very convenient, but maybe I can do the final processing of the data in Lean, and use sorting in Lean.

[Damiano Testa]

(Running that command switches branch back and forth and calls the python script that computes import differences: rewriting those in Lean would be lengthier.)

[Kim Morrison]

Mostly joking. Dog fooding is great, and we would probably learn useful things from it, but it takes a lot of time.

[Damiano Testa]

In the meantime, is there a way to emulate a bash shell in MacOS? I think that asort should be available very widely in non-MacOS Unix-like terminals.

[Damiano Testa]

According to this, the awk call should really be a gawk call: maybe simply changing awk to gawk works for you?

[Damiano Testa]

Locally, the change awk --> gawk shows no difference in output.

[Damiano Testa]

This discussion suggests that gawk is not available, but can be installed with the instructions there.

[Kim Morrison]

Yes, I've installed gawk already.

[Damiano Testa]

Ok, and does changing the unique awk to gawk in the script make it work?

[Kim Morrison]

Yes, looks good. Thanks!

[Damiano Testa]

Ok, I can PR the addition of a g to the script!

[Damiano Testa]

#20909