From 3c5df1827558f55ed4be703c2f48af366bd787c5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 22 Jul 2023 11:31:08 +0100
Subject: [PATCH 1/4] Pin mathlib4 to port-complete

---
 lake-manifest.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index fb52690a4..c859ee367 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -18,7 +18,7 @@
     "subDir?": null,
     "rev": "46f71c61691f26accd73c5ee411801d2d696bf0c",
     "name": "mathlib",
-    "inputRev?": "master"}},
+    "inputRev?": "port-complete"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

From f4c7c4765bdb95a591cc075ac4552b7e24ea4d10 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 24 Jul 2023 21:24:27 +0100
Subject: [PATCH 2/4] Update Makefile

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index e37800845..503b9c548 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ build:
 	lake build
 
 # Select which commit of mathlib3 to use.
-MATHBIN_COMMIT=origin/master
+MATHBIN_COMMIT=origin/port-complete
 
 # Clone mathlib3 and create `all.lean`.
 mathbin-source:

From 2810a077ce4cd5d6bbeabc4ede47f5029dfad6ab Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 24 Jul 2023 21:25:43 +0100
Subject: [PATCH 3/4] Update config.json

---
 config.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/config.json b/config.json
index 1263fd69b..1e3ccbdc6 100644
--- a/config.json
+++ b/config.json
@@ -69,7 +69,7 @@
     "sorries": [],
     "skipProofs": false,
     "skipDefEq": true,
-    "replacementStyle": "comment",
+    "replacementStyle": "keep",
     "redundantAlign": true,
     "error2warning" : true,
     "dubiousMsg": false,

From 429bd0a4dd8ce52cdb55d03907b7b8f8f30dd74d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 11 Oct 2023 14:45:37 +0000
Subject: [PATCH 4/4] fix readme

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index a5409f3f1..86ab46c8d 100644
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@ In the mathport folder:
   all of the dependencies of tactics.
 - `make source`
 - `./download-release.sh`
-  (Or `./download-release.sh [relevant-release]`
+  (Or `./download-release.sh nightly-2023-07-22-09`
   if you need to run against an old mathlib;
   see [mathport releases](https://github.com/leanprover-community/mathport/releases),
   and find the nearest `nightly`.)
@@ -46,7 +46,7 @@ Similarly bump your mathlib dependency to the lastest mathlib3 if possible.
 
 If you really want to run against an older mathlib3 (good luck!):
 
-- In `sources/mathlib` run `git --fetch unshallow`
+- In `sources/mathlib` run `git fetch --unshallow`
 - `git checkout SHA` for the mathlib3 SHA you need.
 - `leanproject get-cache`