Updating `mathlib3port`

Stream: mathlib4

[Scott Morrison]

@Gabriel Ebner, would you be able to give me a quick update on how to update mathlib3port? I see you've changed some things since I last did it (almost a year ago!) and in particular the lakefile no longer tried to download the synported Lean files by itself. What is your process for updating these?

The README.md still talks about it downloading those files itself.

I just found myself porting something that was out of sync with current mathlib and it was too confusing to cope with. :-)

[Gabriel Ebner]

There's now an update.sh script in both lean3port and mathlib3port. Run the lean3port one first then mathlib3port.

[Gabriel Ebner]

It automatically modifies the lake file updates the tool chain version and makes a commit.

[Scott Morrison]

Urghh...

% ./update.sh nightly-2022-10-02
+ tag=nightly-2022-10-02
+ curl -qsSL https://raw.githubusercontent.com/leanprover-community/mathport/nightly-2022-10-02/lean-toolchain -olean-toolchain
++ curl -qsSL https://raw.githubusercontent.com/leanprover-community/mathport/nightly-2022-10-02/lean_packages/manifest.json
++ jq -r '.packages[] | select(.name=="mathlib") | .rev'
+ mathlib4_rev=56b19bdec560037016e326795d0feaa23b402c20
+ sed -i '
  /^def tag / s/"\(.*\)"$/"nightly-2022-10-02"/;
  /^require mathlib / s/@"\([^"]*\)"$/@"56b19bdec560037016e326795d0feaa23b402c20"/
' lakefile.lean
sed: 1: "lakefile.lean": extra characters at the end of l command

[Gabriel Ebner]

I think this may be one of the differences between Linux and Mac... From what I remember sed requires an extra argument on Mac.

[Alex J. Best]

Iirc there is a brew installable gsed (gnu-sed) that can be used in place of sed on Mac and is more compatible. Of course long term the script should be portable. But just for hacking around i recommend installing the package and changing sed to gsed

[Patrick Stevens]

(Similarly gnused is in nixpkgs.)

[Gabriel Ebner]

Now update.sh only works on mac, and not on linux.

[Alex J. Best]

Does sed -i.bak work on both, I think that is the only syntax I found compatible with both seds

[Scott Morrison]

Sorry, I've fixed both update.shs now to be macos/linux compatible.

[Scott Morrison]

I've just bumped mathport to leanprover/lean4:nightly-2022-10-03 --- not because I needed a new Lean4/Std/mathlib4 version, but because I wanted it to process mathlib again.

[Scott Morrison]

I wonder if in the build script for mathport we should change the naming scheme for nightly releases, so it uses the date in lean-toolchain, rather than the date at which CI runs. This might be easier to understand which releases are which.

[Moritz Doll]

Yesterday I've wanted to port another file, but the files in the mathlib3port repo were outdated. Am I supposed to run mathlib3port myself or will we have a automatic nightly builds at some point?

[Mario Carneiro]

cc: @Gabriel Ebner , any chance you could look into automating mathlib3port commits from mathport builds?

[Mario Carneiro]

Until then, you don't have to run mathlib3port yourself @Moritz Doll , you can also download the builds from https://github.com/leanprover-community/mathport/tags, just look for mathlib3-synport.tar.gz

[Scott Morrison]

I think there are two issues here:

[Scott Morrison]

1. mathport doesn't actually generate "nightly" releases nightly, but only after commits to master (of mathport not mathlib).

[Scott Morrison]

2. someone needs to run the update scripts in lean3port and mathlib3port by hand

[Gabriel Ebner]

https://github.com/leanprover-community/mathport/commit/4a13f4185fa85bf9ce518a07bfabf1c2b0aebe10 :fingers_crossed:

[Gabriel Ebner]

It took a couple of tries to get it working, but leanprover-community-bot has just pushed its first update of mathlib3port. From now on, there will be automatic daily updates.

[Gabriel Ebner]

There was another CI issue today, keeping fingers crossed for tomorrow.

[Gabriel Ebner]

Another day, another CI failure. "Keeping fingers crossed for tomorrow."