Pin mathlib4 to port-complete

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:

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`
 

config.json

@@ -69,7 +69,7 @@
     "sorries": [],
     "skipProofs": false,
     "skipDefEq": true,
-    "replacementStyle": "comment",
+    "replacementStyle": "keep",
     "redundantAlign": true,
     "error2warning" : true,
     "dubiousMsg": false,

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,