diff --git a/lean-toolchain b/lean-toolchain index 025e5954..75def609 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.34.0-rc1 diff --git a/test.sh b/test.sh index be8e1b3f..58c5e3f2 100755 --- a/test.sh +++ b/test.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # Define the paths IN_DIR="test" @@ -42,5 +42,6 @@ for infile in $IN_DIR/*.in; do done # Run the Mathlib tests +rm -f test/Mathlib/lean-toolchain cp lean-toolchain test/Mathlib/ cd test/Mathlib/ && ./test.sh diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index 2b8b5ff4..649b190b 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "99e8adeea3c3cd86b6b79ba01a1383bf2d31d055", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "01bc479e7432594821ba3fb0ca465211941de86d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index 9c3f5c0a..495648cb 100644 --- a/test/Mathlib/lakefile.toml +++ b/test/Mathlib/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "v4.33.0" +rev = "v4.34.0-rc1" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 025e5954..75def609 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.34.0-rc1 diff --git a/test/Mathlib/test.sh b/test/Mathlib/test.sh index 0f9f89fe..76dcaba5 100755 --- a/test/Mathlib/test.sh +++ b/test/Mathlib/test.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # Define the paths IN_DIR="test"