Updating to Lean v4.4.0-rc1

.github/workflows/build.yml

@@ -54,17 +54,11 @@ jobs:
         if: github.ref_type == 'tag'
         uses: softprops/action-gh-release@v1
 
-      # TODO: replace with just `lake upload $RELEASE_TAG` when lean4#2713 is fixed
-      # References:
-      # https://docs.github.com/en/actions/learn-github-actions/contexts#runner-context
-      # https://stackoverflow.com/questions/8766730/tar-command-in-mac-os-x-adding-hidden-files-why
       - name: Upload release archive
         if: github.ref_type == 'tag'
         # All our runners are 64-bit ¯\_(ツ)_/¯
         run: |
-          export COPYFILE_DISABLE=true
-          tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./build .
-          gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz
+          lake upload ${RELEASE_TAG}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           RELEASE_TAG: ${{ github.ref_name }}

.gitignore

@@ -1,3 +1,5 @@
+.lake
+DuperOnMathlib/.lake
 /build
 /lake-packages
 /lean_packages

Duper/Tests/test_regression.lean

@@ -682,4 +682,4 @@ theorem proj_test (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0) (h2 : 3 >
 def sk (a b : Nat) (c : Nat × Nat) (h1 : c = (a, b)) : c.1 = a := by
   duper [h1]
 
-#print sk.proof_1
+#print sk

DuperOnMathlib/DuperOnMathlib.lean

@@ -1,3 +1,2 @@
 import DuperOnMathlib.Prime
 import DuperOnMathlib.Cantor
-import DuperOnMathlib.PrimesModFour

DuperOnMathlib/lake-manifest.json

@@ -1,61 +1,74 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "4e5518cafc0efd7c7b7d287fa960fce5201908db",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "4e5518cafc0efd7c7b7d287fa960fce5201908db",
-    "inherited": false}},
-  {"path": {"opts": {}, "name": "Duper", "inherited": false, "dir": "./../"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/quote4",
-    "subDir?": null,
-    "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/lean4-cli",
-    "subDir?": null,
-    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/ProofWidgets4",
-    "subDir?": null,
-    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.21",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/lean-auto.git",
-    "subDir?": null,
-    "rev": "c42a69000568fbadd8bc5664ed22b64b7ff96a62",
-    "opts": {},
-    "name": "auto",
-    "inputRev?": "v0.0.2",
-    "inherited": true}}],
- "name": "duperOnMathlib"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.23",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "rev": "75641abe702d35c946b6e59b8dc672c7e6d80b13",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.4.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "b61345f6d42675298f8fa2b0cc5c471c264a6b40",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.4",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "Duper",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../",
+   "configFile": "lakefile.lean"}],
+ "name": "duperOnMathlib",
+ "lakeDir": ".lake"}

DuperOnMathlib/lakefile.lean

@@ -5,7 +5,7 @@ package «duperOnMathlib» {
   -- add any package configuration options here
 }
 
-require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "4e5518cafc0efd7c7b7d287fa960fce5201908db"
+require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "v4.4.0-rc1"
 
 require «Duper» from "../"
 

DuperOnMathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.4.0-rc1

lake-manifest.json

@@ -1,20 +1,23 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/lean-auto.git",
-    "subDir?": null,
-    "rev": "c42a69000568fbadd8bc5664ed22b64b7ff96a62",
-    "opts": {},
-    "name": "auto",
-    "inputRev?": "v0.0.2",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4.git",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}}],
- "name": "Duper"}
+ [{"url": "https://github.com/leanprover/std4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "b61345f6d42675298f8fa2b0cc5c471c264a6b40",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.4",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Duper",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.2"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.4"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.4.0-rc1