update mathlib-demo

leanprover-community · Jun 5, 2024 · 94048d4 · 94048d4
1 parent f14bfa8
commit 94048d4
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 15 deletions.
diff --git a/Projects/mathlib-demo/MathlibLatest/Rational.lean b/Projects/mathlib-demo/MathlibLatest/Rational.lean
@@ -1,4 +1,3 @@
-import Mathlib.Data.Rat.Order -- import the rationals
 import Mathlib.Data.Rat.Init -- import notation ℚ for rationals
 import Mathlib.Tactic.Linarith -- a linear arithmetic tactic
 import Mathlib.Tactic.Ring -- import the `ring` tactic

diff --git a/Projects/mathlib-demo/lake-manifest.json b/Projects/mathlib-demo/lake-manifest.json
@@ -1,19 +1,19 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
-   "name": "std",
+   "rev": "7110da53bf6da84198dba69ca90221c4798ade35",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,16 +49,16 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "8d0c6e6f821392660468fdce7c5463740d7988be",
+   "rev": "5795dea5a47ba1d4735896548b96dd0bb38cf248",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -67,7 +67,7 @@
   {"url": "https://github.com/hhu-adam/lean4web-tools.git",
    "type": "git",
    "subDir": null,
-   "rev": "0bf7f2dd6861b0be4c7f0e761a50ae03e6fb2d6b",
+   "rev": "8be7734dfa9a686d3a1329651e2a1a690e1123b6",
    "name": "webeditor",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/Projects/mathlib-demo/lean-toolchain b/Projects/mathlib-demo/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.7.0
		leanprover/lean4:v4.8.0-rc2