From nobody Mon Sep 2 07:54:57 2024 X-Original-To: dev-commits-ports-all@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4Wy1J16C48z5Mjwf; Mon, 02 Sep 2024 07:54:57 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R11" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4Wy1J12ft6z3ww7; Mon, 2 Sep 2024 07:54:57 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1725263697; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=pxqubQ69ZRFFNsV7oiv/mA1DXI96YXRsMwtmeIXFYv8=; b=FlISgiVrg57buKyAxu5MTI/BmdM1f0bP9jnUOptwMysCKUdcSz5We9h6OTX7uPl1MfxBOD 6DL4KhZNsZ4hnxJDD/I0f72KC7Ca9AG3QIVTMtwpgvWzBOH1mMvHp1lV8VlBYIn7SnJtRa YJaqtar6Ri7OFjgcu+U6KIOFMELsxgPuezZD7BRkRq+V/Xb+IzNhrVE1l1lQv84T6VHSSc 5PXRTtbb9OmBk0rPvG9X3X2/2I/9obtUycOpi9Z6OrwQolWRi+bYs43efnmNmMpXeQ8dVw YQZXWz3CvAfIjH1OePZgem30RRy7XgtlCOYuDpXHGlqm6PFLPq5sc7UrCi2lUQ== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1725263697; a=rsa-sha256; cv=none; b=aozGiuH1w/OAB55ABs6HB30SlGirCp5UPkOpFN5ux6eRSMVoQyksnZvs9/pkJOZHTlkdqZ He0tBd7lo/7Cw1FdBQAuqGQUGIQ+xT+RGepMwKgpR7q2vbFyOG7lFErTk/OrCNAPPrbTCo CmSo3RSirfxz18iiJTIX6vWfFUpaDFKJG1c0ig6d46FKvXUuSsX1/rx7JW8tsYBR4WTdDw iUKJ68+PUQC8cDC5fqla18VkTUNdARwbaLEWDZZ/xsRsWeblm0xhY12krYXCLRj0XIdG0f dOYxuESJaallKCM0AHuFQwycidkH8hrBmeh9x5WCTgafu60XzogllfWGRCd/CQ== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1725263697; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=pxqubQ69ZRFFNsV7oiv/mA1DXI96YXRsMwtmeIXFYv8=; b=wNvXPOwiBSSaAEDfWBCA+01bfAcphAxdcmw94dmMjgKS6rKAoNvG/YYONxFV8WrLhIPAPU XfXBAcYFqsae64woFbEH7psW0cTND8EGVHGpkf1yKtsSictQflFk66+Fq/wJpHTKHCpJu/ uXh13Tc7V2hVq1VnXnBDKkfxkLkDZ6mvGfJyonF69337wMaN8XoVkcGsdMo2vB0tiRKEZm AqugxiWy9+MyHLzEyx+zdKrnNXKQr9biPWgJwwaG07rX5x7HhSjgFlH5VQs9rv3SdHA53C qW2LVjRrHWN+En3oUViMPh62uFgDPeIbULhUYt4EQMlIbxmqFkrMLmX7KooAkA== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4Wy1J12CMwz13fJ; Mon, 2 Sep 2024 07:54:57 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.18.1/8.18.1) with ESMTP id 4827svw5012018; Mon, 2 Sep 2024 07:54:57 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.18.1/8.18.1/Submit) id 4827svgJ012015; Mon, 2 Sep 2024 07:54:57 GMT (envelope-from git) Date: Mon, 2 Sep 2024 07:54:57 GMT Message-Id: <202409020754.4827svgJ012015@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: 1fde20b526dd - main - math/lean4: update 4.10.0 =?utf-8?Q?=E2=86=92?= 4.11.0 List-Id: Commit messages for all branches of the ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-all List-Help: List-Post: List-Subscribe: List-Unsubscribe: X-BeenThere: dev-commits-ports-all@freebsd.org Sender: owner-dev-commits-ports-all@FreeBSD.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 1fde20b526ddc12811e0af7ee6a71e1f732eaf5b Auto-Submitted: auto-generated The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=1fde20b526ddc12811e0af7ee6a71e1f732eaf5b commit 1fde20b526ddc12811e0af7ee6a71e1f732eaf5b Author: Yuri Victorovich AuthorDate: 2024-09-02 07:54:32 +0000 Commit: Yuri Victorovich CommitDate: 2024-09-02 07:54:45 +0000 math/lean4: update 4.10.0 → 4.11.0 --- math/lean4/Makefile | 2 +- math/lean4/distinfo | 6 +- math/lean4/pkg-plist | 220 ++++++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 215 insertions(+), 13 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 562dad632944..abfc3004d07b 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.10.0 +DISTVERSION= 4.11.0 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org diff --git a/math/lean4/distinfo b/math/lean4/distinfo index 1ca0f069d7a4..fd56f3893df9 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1722411891 -SHA256 (leanprover-lean4-v4.10.0_GH0.tar.gz) = dee5d1dbcea924fa3f4500c1f4854ea5953f471e3600dac71421c742c844b094 -SIZE (leanprover-lean4-v4.10.0_GH0.tar.gz) = 25013155 +TIMESTAMP = 1725254182 +SHA256 (leanprover-lean4-v4.11.0_GH0.tar.gz) = 8b7fc8e71e107250c7bbf911eb1f450379d874857a26236577aaa624dd5962b5 +SIZE (leanprover-lean4-v4.11.0_GH0.tar.gz) = 25790812 diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 65859221ae90..365f371356e4 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -54,6 +54,8 @@ lib/lean/Init/Data/AC.ilean lib/lean/Init/Data/AC.olean lib/lean/Init/Data/Array.ilean lib/lean/Init/Data/Array.olean +lib/lean/Init/Data/Array/Attach.ilean +lib/lean/Init/Data/Array/Attach.olean lib/lean/Init/Data/Array/Basic.ilean lib/lean/Init/Data/Array/Basic.olean lib/lean/Init/Data/Array/BasicAux.ilean @@ -74,6 +76,10 @@ lib/lean/Init/Data/Array/Subarray.ilean lib/lean/Init/Data/Array/Subarray.olean lib/lean/Init/Data/Array/Subarray/Split.ilean lib/lean/Init/Data/Array/Subarray/Split.olean +lib/lean/Init/Data/Array/TakeDrop.ilean +lib/lean/Init/Data/Array/TakeDrop.olean +lib/lean/Init/Data/BEq.ilean +lib/lean/Init/Data/BEq.olean lib/lean/Init/Data/Basic.ilean lib/lean/Init/Data/Basic.olean lib/lean/Init/Data/BitVec.ilean @@ -106,6 +112,8 @@ lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.olean lib/lean/Init/Data/Fin/Basic.ilean lib/lean/Init/Data/Fin/Basic.olean +lib/lean/Init/Data/Fin/Bitwise.ilean +lib/lean/Init/Data/Fin/Bitwise.olean lib/lean/Init/Data/Fin/Fold.ilean lib/lean/Init/Data/Fin/Fold.olean lib/lean/Init/Data/Fin/Iterate.ilean @@ -154,20 +162,48 @@ lib/lean/Init/Data/Int/Pow.ilean lib/lean/Init/Data/Int/Pow.olean lib/lean/Init/Data/List.ilean lib/lean/Init/Data/List.olean +lib/lean/Init/Data/List/Attach.ilean +lib/lean/Init/Data/List/Attach.olean lib/lean/Init/Data/List/Basic.ilean lib/lean/Init/Data/List/Basic.olean lib/lean/Init/Data/List/BasicAux.ilean lib/lean/Init/Data/List/BasicAux.olean lib/lean/Init/Data/List/Control.ilean lib/lean/Init/Data/List/Control.olean +lib/lean/Init/Data/List/Count.ilean +lib/lean/Init/Data/List/Count.olean +lib/lean/Init/Data/List/Erase.ilean +lib/lean/Init/Data/List/Erase.olean +lib/lean/Init/Data/List/Find.ilean +lib/lean/Init/Data/List/Find.olean lib/lean/Init/Data/List/Impl.ilean lib/lean/Init/Data/List/Impl.olean lib/lean/Init/Data/List/Lemmas.ilean lib/lean/Init/Data/List/Lemmas.olean +lib/lean/Init/Data/List/MinMax.ilean +lib/lean/Init/Data/List/MinMax.olean +lib/lean/Init/Data/List/Monadic.ilean +lib/lean/Init/Data/List/Monadic.olean +lib/lean/Init/Data/List/Nat.ilean +lib/lean/Init/Data/List/Nat.olean +lib/lean/Init/Data/List/Nat/Basic.ilean +lib/lean/Init/Data/List/Nat/Basic.olean +lib/lean/Init/Data/List/Nat/Pairwise.ilean +lib/lean/Init/Data/List/Nat/Pairwise.olean +lib/lean/Init/Data/List/Nat/Range.ilean +lib/lean/Init/Data/List/Nat/Range.olean +lib/lean/Init/Data/List/Nat/TakeDrop.ilean +lib/lean/Init/Data/List/Nat/TakeDrop.olean lib/lean/Init/Data/List/Notation.ilean lib/lean/Init/Data/List/Notation.olean +lib/lean/Init/Data/List/Pairwise.ilean +lib/lean/Init/Data/List/Pairwise.olean +lib/lean/Init/Data/List/Sublist.ilean +lib/lean/Init/Data/List/Sublist.olean lib/lean/Init/Data/List/TakeDrop.ilean lib/lean/Init/Data/List/TakeDrop.olean +lib/lean/Init/Data/List/Zip.ilean +lib/lean/Init/Data/List/Zip.olean lib/lean/Init/Data/Nat.ilean lib/lean/Init/Data/Nat.olean lib/lean/Init/Data/Nat/Basic.ilean @@ -240,6 +276,8 @@ lib/lean/Init/Data/String/Extra.ilean lib/lean/Init/Data/String/Extra.olean lib/lean/Init/Data/String/Lemmas.ilean lib/lean/Init/Data/String/Lemmas.olean +lib/lean/Init/Data/Subtype.ilean +lib/lean/Init/Data/Subtype.olean lib/lean/Init/Data/Sum.ilean lib/lean/Init/Data/Sum.olean lib/lean/Init/Data/ToString.ilean @@ -252,6 +290,8 @@ lib/lean/Init/Data/UInt.ilean lib/lean/Init/Data/UInt.olean lib/lean/Init/Data/UInt/Basic.ilean lib/lean/Init/Data/UInt/Basic.olean +lib/lean/Init/Data/UInt/Bitwise.ilean +lib/lean/Init/Data/UInt/Bitwise.olean lib/lean/Init/Data/UInt/Lemmas.ilean lib/lean/Init/Data/UInt/Lemmas.olean lib/lean/Init/Data/UInt/Log2.ilean @@ -1092,14 +1132,22 @@ lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.olean lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.ilean lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.olean +lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.ilean +lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.olean lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.ilean lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.olean lib/lean/Lean/Elab/PreDefinition/Structural/Main.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Main.olean lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.olean +lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.ilean +lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.olean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.ilean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.olean +lib/lean/Lean/Elab/PreDefinition/TerminationArgument.ilean +lib/lean/Lean/Elab/PreDefinition/TerminationArgument.olean +lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean +lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean lib/lean/Lean/Elab/PreDefinition/WF.ilean lib/lean/Lean/Elab/PreDefinition/WF.olean lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean @@ -1118,10 +1166,6 @@ lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.ilean lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.olean lib/lean/Lean/Elab/PreDefinition/WF/Rel.ilean lib/lean/Lean/Elab/PreDefinition/WF/Rel.olean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.ilean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.olean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.ilean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.olean lib/lean/Lean/Elab/Print.ilean lib/lean/Lean/Elab/Print.olean lib/lean/Lean/Elab/Quotation.ilean @@ -1178,6 +1222,8 @@ lib/lean/Lean/Elab/Tactic/Conv/Unfold.ilean lib/lean/Lean/Elab/Tactic/Conv/Unfold.olean lib/lean/Lean/Elab/Tactic/Delta.ilean lib/lean/Lean/Elab/Tactic/Delta.olean +lib/lean/Lean/Elab/Tactic/DiscrTreeKey.ilean +lib/lean/Lean/Elab/Tactic/DiscrTreeKey.olean lib/lean/Lean/Elab/Tactic/Doc.ilean lib/lean/Lean/Elab/Tactic/Doc.olean lib/lean/Lean/Elab/Tactic/ElabTerm.ilean @@ -1270,6 +1316,8 @@ lib/lean/Lean/Language/Basic.ilean lib/lean/Lean/Language/Basic.olean lib/lean/Lean/Language/Lean.ilean lib/lean/Lean/Language/Lean.olean +lib/lean/Lean/Language/Lean/Types.ilean +lib/lean/Lean/Language/Lean/Types.olean lib/lean/Lean/LazyInitExtension.ilean lib/lean/Lean/LazyInitExtension.olean lib/lean/Lean/Level.ilean @@ -1286,6 +1334,8 @@ lib/lean/Lean/Linter/Deprecated.ilean lib/lean/Lean/Linter/Deprecated.olean lib/lean/Lean/Linter/MissingDocs.ilean lib/lean/Lean/Linter/MissingDocs.olean +lib/lean/Lean/Linter/Omit.ilean +lib/lean/Lean/Linter/Omit.olean lib/lean/Lean/Linter/UnusedVariables.ilean lib/lean/Lean/Linter/UnusedVariables.olean lib/lean/Lean/Linter/Util.ilean @@ -1338,6 +1388,10 @@ lib/lean/Lean/Meta/Constructions.ilean lib/lean/Lean/Meta/Constructions.olean lib/lean/Lean/Meta/Constructions/BRecOn.ilean lib/lean/Lean/Meta/Constructions/BRecOn.olean +lib/lean/Lean/Meta/Constructions/CasesOn.ilean +lib/lean/Lean/Meta/Constructions/CasesOn.olean +lib/lean/Lean/Meta/Constructions/NoConfusion.ilean +lib/lean/Lean/Meta/Constructions/NoConfusion.olean lib/lean/Lean/Meta/Constructions/RecOn.ilean lib/lean/Lean/Meta/Constructions/RecOn.olean lib/lean/Lean/Meta/CtorRecognizer.ilean @@ -1430,6 +1484,8 @@ lib/lean/Lean/Meta/Offset.ilean lib/lean/Lean/Meta/Offset.olean lib/lean/Lean/Meta/PPGoal.ilean lib/lean/Lean/Meta/PPGoal.olean +lib/lean/Lean/Meta/PProdN.ilean +lib/lean/Lean/Meta/PProdN.olean lib/lean/Lean/Meta/RecursorInfo.ilean lib/lean/Lean/Meta/RecursorInfo.olean lib/lean/Lean/Meta/Reduce.ilean @@ -1552,6 +1608,8 @@ lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean lib/lean/Lean/Meta/Tactic/Simp/Attr.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.ilean @@ -1562,6 +1620,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.ilean @@ -1754,6 +1814,8 @@ lib/lean/Lean/ToExpr.ilean lib/lean/Lean/ToExpr.olean lib/lean/Lean/Util.ilean lib/lean/Lean/Util.olean +lib/lean/Lean/Util/CollectAxioms.ilean +lib/lean/Lean/Util/CollectAxioms.olean lib/lean/Lean/Util/CollectFVars.ilean lib/lean/Lean/Util/CollectFVars.olean lib/lean/Lean/Util/CollectLevelParams.ilean @@ -1790,6 +1852,8 @@ lib/lean/Lean/Util/MonadBacktrack.ilean lib/lean/Lean/Util/MonadBacktrack.olean lib/lean/Lean/Util/MonadCache.ilean lib/lean/Lean/Util/MonadCache.olean +lib/lean/Lean/Util/NumObjs.ilean +lib/lean/Lean/Util/NumObjs.olean lib/lean/Lean/Util/OccursCheck.ilean lib/lean/Lean/Util/OccursCheck.olean lib/lean/Lean/Util/PPExt.ilean @@ -1814,6 +1878,10 @@ lib/lean/Lean/Util/ReplaceLevel.ilean lib/lean/Lean/Util/ReplaceLevel.olean lib/lean/Lean/Util/SCC.ilean lib/lean/Lean/Util/SCC.olean +lib/lean/Lean/Util/SafeExponentiation.ilean +lib/lean/Lean/Util/SafeExponentiation.olean +lib/lean/Lean/Util/SearchPath.ilean +lib/lean/Lean/Util/SearchPath.olean lib/lean/Lean/Util/ShareCommon.ilean lib/lean/Lean/Util/ShareCommon.olean lib/lean/Lean/Util/Sorry.ilean @@ -1842,6 +1910,72 @@ lib/lean/Lean/Widget/UserWidget.ilean lib/lean/Lean/Widget/UserWidget.olean lib/lean/Std.ilean lib/lean/Std.olean +lib/lean/Std/Data.ilean +lib/lean/Std/Data.olean +lib/lean/Std/Data/DHashMap.ilean +lib/lean/Std/Data/DHashMap.olean +lib/lean/Std/Data/DHashMap/AdditionalOperations.ilean +lib/lean/Std/Data/DHashMap/AdditionalOperations.olean +lib/lean/Std/Data/DHashMap/Basic.ilean +lib/lean/Std/Data/DHashMap/Basic.olean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.ilean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ilean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.olean +lib/lean/Std/Data/DHashMap/Internal/Defs.ilean +lib/lean/Std/Data/DHashMap/Internal/Defs.olean +lib/lean/Std/Data/DHashMap/Internal/Index.ilean +lib/lean/Std/Data/DHashMap/Internal/Index.olean +lib/lean/Std/Data/DHashMap/Internal/List/Associative.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Associative.olean +lib/lean/Std/Data/DHashMap/Internal/List/Defs.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Defs.olean +lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean +lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean +lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean +lib/lean/Std/Data/DHashMap/Internal/List/Perm.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Perm.olean +lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean +lib/lean/Std/Data/DHashMap/Internal/Model.ilean +lib/lean/Std/Data/DHashMap/Internal/Model.olean +lib/lean/Std/Data/DHashMap/Internal/Raw.ilean +lib/lean/Std/Data/DHashMap/Internal/Raw.olean +lib/lean/Std/Data/DHashMap/Internal/RawLemmas.ilean +lib/lean/Std/Data/DHashMap/Internal/RawLemmas.olean +lib/lean/Std/Data/DHashMap/Internal/WF.ilean +lib/lean/Std/Data/DHashMap/Internal/WF.olean +lib/lean/Std/Data/DHashMap/Lemmas.ilean +lib/lean/Std/Data/DHashMap/Lemmas.olean +lib/lean/Std/Data/DHashMap/Raw.ilean +lib/lean/Std/Data/DHashMap/Raw.olean +lib/lean/Std/Data/DHashMap/RawDef.ilean +lib/lean/Std/Data/DHashMap/RawDef.olean +lib/lean/Std/Data/DHashMap/RawLemmas.ilean +lib/lean/Std/Data/DHashMap/RawLemmas.olean +lib/lean/Std/Data/HashMap.ilean +lib/lean/Std/Data/HashMap.olean +lib/lean/Std/Data/HashMap/AdditionalOperations.ilean +lib/lean/Std/Data/HashMap/AdditionalOperations.olean +lib/lean/Std/Data/HashMap/Basic.ilean +lib/lean/Std/Data/HashMap/Basic.olean +lib/lean/Std/Data/HashMap/Lemmas.ilean +lib/lean/Std/Data/HashMap/Lemmas.olean +lib/lean/Std/Data/HashMap/Raw.ilean +lib/lean/Std/Data/HashMap/Raw.olean +lib/lean/Std/Data/HashMap/RawLemmas.ilean +lib/lean/Std/Data/HashMap/RawLemmas.olean +lib/lean/Std/Data/HashSet.ilean +lib/lean/Std/Data/HashSet.olean +lib/lean/Std/Data/HashSet/Basic.ilean +lib/lean/Std/Data/HashSet/Basic.olean +lib/lean/Std/Data/HashSet/Lemmas.ilean +lib/lean/Std/Data/HashSet/Lemmas.olean +lib/lean/Std/Data/HashSet/Raw.ilean +lib/lean/Std/Data/HashSet/Raw.olean +lib/lean/Std/Data/HashSet/RawLemmas.ilean +lib/lean/Std/Data/HashSet/RawLemmas.olean lib/lean/libInit.a lib/lean/libInit_shared.so lib/lean/libLake.a @@ -1875,6 +2009,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data.lean %%DATADIR%%/src/lean/Init/Data/AC.lean %%DATADIR%%/src/lean/Init/Data/Array.lean +%%DATADIR%%/src/lean/Init/Data/Array/Attach.lean %%DATADIR%%/src/lean/Init/Data/Array/Basic.lean %%DATADIR%%/src/lean/Init/Data/Array/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/Array/BinSearch.lean @@ -1885,6 +2020,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Array/QSort.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray/Split.lean +%%DATADIR%%/src/lean/Init/Data/Array/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/BEq.lean %%DATADIR%%/src/lean/Init/Data/Basic.lean %%DATADIR%%/src/lean/Init/Data/BitVec.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean @@ -1901,6 +2038,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Char/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Fin.lean %%DATADIR%%/src/lean/Init/Data/Fin/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Fin/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/Fin/Fold.lean %%DATADIR%%/src/lean/Init/Data/Fin/Iterate.lean %%DATADIR%%/src/lean/Init/Data/Fin/Lemmas.lean @@ -1925,13 +2063,27 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Int/Order.lean %%DATADIR%%/src/lean/Init/Data/Int/Pow.lean %%DATADIR%%/src/lean/Init/Data/List.lean +%%DATADIR%%/src/lean/Init/Data/List/Attach.lean %%DATADIR%%/src/lean/Init/Data/List/Basic.lean %%DATADIR%%/src/lean/Init/Data/List/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/List/Control.lean +%%DATADIR%%/src/lean/Init/Data/List/Count.lean +%%DATADIR%%/src/lean/Init/Data/List/Erase.lean +%%DATADIR%%/src/lean/Init/Data/List/Find.lean %%DATADIR%%/src/lean/Init/Data/List/Impl.lean %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/List/MinMax.lean +%%DATADIR%%/src/lean/Init/Data/List/Monadic.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean %%DATADIR%%/src/lean/Init/Data/List/Notation.lean +%%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean +%%DATADIR%%/src/lean/Init/Data/List/Sublist.lean %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/List/Zip.lean %%DATADIR%%/src/lean/Init/Data/Nat.lean %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean @@ -1968,12 +2120,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/String/Basic.lean %%DATADIR%%/src/lean/Init/Data/String/Extra.lean %%DATADIR%%/src/lean/Init/Data/String/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Subtype.lean %%DATADIR%%/src/lean/Init/Data/Sum.lean %%DATADIR%%/src/lean/Init/Data/ToString.lean %%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean %%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean %%DATADIR%%/src/lean/Init/Data/UInt.lean %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean +%%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean %%DATADIR%%/src/lean/Init/Dynamic.lean @@ -2266,10 +2420,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndPred.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Preprocess.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean @@ -2279,8 +2437,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackMutual.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Preprocess.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Rel.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationHint.lean %%DATADIR%%/src/lean/Lean/Elab/Print.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation/Precheck.lean @@ -2309,6 +2465,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Simp.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Unfold.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Delta.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Ext.lean @@ -2355,6 +2512,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/LabelAttribute.lean %%DATADIR%%/src/lean/Lean/Language/Basic.lean %%DATADIR%%/src/lean/Lean/Language/Lean.lean +%%DATADIR%%/src/lean/Lean/Language/Lean/Types.lean %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean %%DATADIR%%/src/lean/Lean/Level.lean %%DATADIR%%/src/lean/Lean/Linter.lean @@ -2363,6 +2521,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean +%%DATADIR%%/src/lean/Lean/Linter/Omit.lean %%DATADIR%%/src/lean/Lean/Linter/UnusedVariables.lean %%DATADIR%%/src/lean/Lean/Linter/Util.lean %%DATADIR%%/src/lean/Lean/LoadDynlib.lean @@ -2389,6 +2548,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/CongrTheorems.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/BRecOn.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/CasesOn.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/NoConfusion.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/RecOn.lean %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean @@ -2435,6 +2596,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/NatInstTesters.lean %%DATADIR%%/src/lean/Lean/Meta/Offset.lean %%DATADIR%%/src/lean/Lean/Meta/PPGoal.lean +%%DATADIR%%/src/lean/Lean/Meta/PProdN.lean %%DATADIR%%/src/lean/Lean/Meta/RecursorInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Reduce.lean %%DATADIR%%/src/lean/Lean/Meta/ReduceEval.lean @@ -2496,11 +2658,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Attr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -2598,6 +2762,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Syntax.lean %%DATADIR%%/src/lean/Lean/ToExpr.lean %%DATADIR%%/src/lean/Lean/Util.lean +%%DATADIR%%/src/lean/Lean/Util/CollectAxioms.lean %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean @@ -2616,6 +2781,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean %%DATADIR%%/src/lean/Lean/Util/MonadBacktrack.lean %%DATADIR%%/src/lean/Lean/Util/MonadCache.lean +%%DATADIR%%/src/lean/Lean/Util/NumObjs.lean %%DATADIR%%/src/lean/Lean/Util/OccursCheck.lean %%DATADIR%%/src/lean/Lean/Util/PPExt.lean %%DATADIR%%/src/lean/Lean/Util/Path.lean @@ -2628,6 +2794,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/ReplaceExpr.lean %%DATADIR%%/src/lean/Lean/Util/ReplaceLevel.lean %%DATADIR%%/src/lean/Lean/Util/SCC.lean +%%DATADIR%%/src/lean/Lean/Util/SafeExponentiation.lean +%%DATADIR%%/src/lean/Lean/Util/SearchPath.lean %%DATADIR%%/src/lean/Lean/Util/ShareCommon.lean %%DATADIR%%/src/lean/Lean/Util/Sorry.lean %%DATADIR%%/src/lean/Lean/Util/TestExtern.lean @@ -2643,6 +2811,39 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean %%DATADIR%%/src/lean/Leanc.lean %%DATADIR%%/src/lean/Std.lean +%%DATADIR%%/src/lean/Std/Data.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Index.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Perm.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/WF.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/RawDef.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashMap.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashSet.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean %%DATADIR%%/src/lean/lake/Lake.lean %%DATADIR%%/src/lean/lake/Lake/Build.lean %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean @@ -2818,6 +3019,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/lock/Nop.lean %%DATADIR%%/src/lean/lake/tests/lock/Wait.lean %%DATADIR%%/src/lean/lake/tests/lock/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Error.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Info.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Warning.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/bar/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/foo/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/lakefile.lean @@ -2857,6 +3062,3 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/trace/Foo.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean -%%DATADIR%%/src/lean/lake/tests/wfail/Warn.lean -%%DATADIR%%/src/lean/lake/tests/wfail/lakefile.lean -@dir lib/lean/Std