From nobody Fri Jun 7 17:01:27 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 4VwnXl1LQzz5LMHN; Fri, 07 Jun 2024 17:01:27 +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 "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4VwnXl15NKz4vdZ; Fri, 7 Jun 2024 17:01:27 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1717779687; 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=Y22oQEgIWMfM1A9Z8zgsgjrq30+taewgyh0kXhnNPGY=; b=Fmbb+GrkfVWnQDER9xVekFgDq5FLbPc/5WJo6DK+boCO2Hc6SI0xWsRW0Ut6JdglFYlM9n bCjyhuXK92TyS0+Dt9ht17SaiPJyBkGvX/6a5H3QtY7peGr/zHG3P4XuTwdD/PJ9uqeLud /7Ne7pEqCx1Gy47TzsOM8MVojA4DkvUwW+zHZgODnn22Wf3wOxzMuuIelotjIiwpKtgbW7 ZLhp5WDiEd+TsOgXjgf1XVT8k3c/7j0U3F92JNO1SwVDYVVdG/5dfxWjCXTkfN8pvv+vbH cmvLRC9R9UF71EcF79jAifa4gvZ1lVlLHbEvNYlid1sZJ0rBRC78lAN5GcEBRQ== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1717779687; a=rsa-sha256; cv=none; b=k3PyEW4qf7DhXAm5YQQ2XALGY5Xl7gSIvM8XW4f7ZvH9i2kOvU1O6W0kQcWRRontGPvSvV am2j9AebW9Wp7X00XkFGZ6qeBPjp9G40WtPDSDLlZBtYRDie5hnqfFdMdXps3k0MQ6co9g xfGg5zKX52z5zp4mMzEGqXzmBw9T64FrMB7TIcJhD0SUEOElirtwaTKqqUyfVTHehkKMYA UoY1PGfSrGaxwnSYyoKWqOc6QWj1YY/jWM7dmJa3J4eQM+CGYvS2PZLzW4gHIoXpzTU/vG w5xQ99Xnd+PRlwmsANefoNJI9Rfdo4W+kffXWmWh80W7Z4JVksA+Cfcy8GaLNA== 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=1717779687; 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=Y22oQEgIWMfM1A9Z8zgsgjrq30+taewgyh0kXhnNPGY=; b=rTeBGG7iTIuc9d9mnoSYF65H59GOK3PZveXVw390skCfYFJWLEk+GM+Tj+UnMtFWz7Wsf4 DlDU32+ifOcGtq700Mufu7kl/cuwQUb8lxRJiijWFDdthtKA6gULXup79XkyJ5sPaFFJM8 Dqs/39nfYUlcy5hsIqkIiJ4p1d8rh0Rftl6l7vbqtscs1OqhZlWqxAyH0jYZilbcWKF9nE T9lfzRF+Dv4LKLN4HPRQVesESvV8PeWEsUqjPEhuZwhqLMBuCTZPklk/D9SSMHuQZ1vCRh xtKFILL2/fXn69EzJqjxlIjjIq1TyNowpJsYmctVL/EkjpJt+zWxbxelylfm7A== 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 4VwnXl0j9kzMGQ; Fri, 7 Jun 2024 17:01:27 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.17.1/8.17.1) with ESMTP id 457H1RmQ004600; Fri, 7 Jun 2024 17:01:27 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.17.1/8.17.1/Submit) id 457H1Rwk004597; Fri, 7 Jun 2024 17:01:27 GMT (envelope-from git) Date: Fri, 7 Jun 2024 17:01:27 GMT Message-Id: <202406071701.457H1Rwk004597@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: 4c7811ea785f - main - math/lean4: update 4.7.0 =?utf-8?Q?=E2=86=92?= 4.8.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: 4c7811ea785fa4c53d83e3991a6f786e09251d0f Auto-Submitted: auto-generated The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=4c7811ea785fa4c53d83e3991a6f786e09251d0f commit 4c7811ea785fa4c53d83e3991a6f786e09251d0f Author: Yuri Victorovich AuthorDate: 2024-06-07 17:01:16 +0000 Commit: Yuri Victorovich CommitDate: 2024-06-07 17:01:24 +0000 math/lean4: update 4.7.0 → 4.8.0 Reported by: portscout --- math/lean4/Makefile | 6 +- math/lean4/distinfo | 6 +- math/lean4/pkg-plist | 214 +++++++++++++++++++++++++++++++++++++++++++++++---- 3 files changed, 206 insertions(+), 20 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index cbc4e5280841..c6a1086693fe 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.7.0 +DISTVERSION= 4.8.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 @@ -39,6 +39,8 @@ post-install: lib/lean/libInit_shared.so \ lib/lean/libleanshared.so -# 6 tests are known to fail due to bugs in the testcase code, see https://github.com/leanprover/lean4/issues/3179 +# 2 test failures: +# https://github.com/leanprover/lean4/issues/4396: The test leanlaketest_old times out +# https://github.com/leanprover/lean4/issues/4397: The test leanlaketest_serve fails: error: unexpected identifier; expected command .include diff --git a/math/lean4/distinfo b/math/lean4/distinfo index d20cb0cc673a..d12208f173cc 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1713025323 -SHA256 (leanprover-lean4-v4.7.0_GH0.tar.gz) = b1f00b5f2431b34aeacba993c4f4675211a3827e96c4b1a06054c58188ae72c8 -SIZE (leanprover-lean4-v4.7.0_GH0.tar.gz) = 19261610 +TIMESTAMP = 1717688258 +SHA256 (leanprover-lean4-v4.8.0_GH0.tar.gz) = 3bb46c24b4f5ad1fee38163bf466d8f60a334bb64a19c9801a42f76162580f9c +SIZE (leanprover-lean4-v4.8.0_GH0.tar.gz) = 20345135 diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 5b2bc5e8899c..75fc4ce6be58 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -30,6 +30,10 @@ lib/lean/Init/Control/Id.ilean lib/lean/Init/Control/Id.olean lib/lean/Init/Control/Lawful.ilean lib/lean/Init/Control/Lawful.olean +lib/lean/Init/Control/Lawful/Basic.ilean +lib/lean/Init/Control/Lawful/Basic.olean +lib/lean/Init/Control/Lawful/Instances.ilean +lib/lean/Init/Control/Lawful/Instances.olean lib/lean/Init/Control/Option.ilean lib/lean/Init/Control/Option.olean lib/lean/Init/Control/Reader.ilean @@ -68,6 +72,8 @@ lib/lean/Init/Data/Array/QSort.ilean lib/lean/Init/Data/Array/QSort.olean 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/Basic.ilean lib/lean/Init/Data/Basic.olean lib/lean/Init/Data/BitVec.ilean @@ -140,6 +146,8 @@ lib/lean/Init/Data/Int/Lemmas.ilean lib/lean/Init/Data/Int/Lemmas.olean lib/lean/Init/Data/Int/Order.ilean lib/lean/Init/Data/Int/Order.olean +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/Basic.ilean @@ -148,6 +156,8 @@ 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/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/Nat.ilean @@ -160,6 +170,8 @@ lib/lean/Init/Data/Nat/Bitwise/Basic.ilean lib/lean/Init/Data/Nat/Bitwise/Basic.olean lib/lean/Init/Data/Nat/Bitwise/Lemmas.ilean lib/lean/Init/Data/Nat/Bitwise/Lemmas.olean +lib/lean/Init/Data/Nat/Compare.ilean +lib/lean/Init/Data/Nat/Compare.olean lib/lean/Init/Data/Nat/Control.ilean lib/lean/Init/Data/Nat/Control.olean lib/lean/Init/Data/Nat/Div.ilean @@ -168,6 +180,8 @@ lib/lean/Init/Data/Nat/Dvd.ilean lib/lean/Init/Data/Nat/Dvd.olean lib/lean/Init/Data/Nat/Gcd.ilean lib/lean/Init/Data/Nat/Gcd.olean +lib/lean/Init/Data/Nat/Lcm.ilean +lib/lean/Init/Data/Nat/Lcm.olean lib/lean/Init/Data/Nat/Lemmas.ilean lib/lean/Init/Data/Nat/Lemmas.olean lib/lean/Init/Data/Nat/Linear.ilean @@ -182,6 +196,8 @@ lib/lean/Init/Data/Nat/Power2.ilean lib/lean/Init/Data/Nat/Power2.olean lib/lean/Init/Data/Nat/SOM.ilean lib/lean/Init/Data/Nat/SOM.olean +lib/lean/Init/Data/Nat/Simproc.ilean +lib/lean/Init/Data/Nat/Simproc.olean lib/lean/Init/Data/OfScientific.ilean lib/lean/Init/Data/OfScientific.olean lib/lean/Init/Data/Option.ilean @@ -232,10 +248,14 @@ lib/lean/Init/Dynamic.ilean lib/lean/Init/Dynamic.olean lib/lean/Init/Ext.ilean lib/lean/Init/Ext.olean +lib/lean/Init/GetElem.ilean +lib/lean/Init/GetElem.olean lib/lean/Init/Guard.ilean lib/lean/Init/Guard.olean lib/lean/Init/Hints.ilean lib/lean/Init/Hints.olean +lib/lean/Init/MacroTrace.ilean +lib/lean/Init/MacroTrace.olean lib/lean/Init/Meta.ilean lib/lean/Init/Meta.olean lib/lean/Init/MetaTypes.ilean @@ -308,16 +328,18 @@ lib/lean/Lake/Build.ilean lib/lean/Lake/Build.olean lib/lean/Lake/Build/Actions.ilean lib/lean/Lake/Build/Actions.olean +lib/lean/Lake/Build/Basic.ilean +lib/lean/Lake/Build/Basic.olean lib/lean/Lake/Build/Common.ilean lib/lean/Lake/Build/Common.olean -lib/lean/Lake/Build/Context.ilean -lib/lean/Lake/Build/Context.olean lib/lean/Lake/Build/Data.ilean lib/lean/Lake/Build/Data.olean lib/lean/Lake/Build/Executable.ilean lib/lean/Lake/Build/Executable.olean lib/lean/Lake/Build/Facets.ilean lib/lean/Lake/Build/Facets.olean +lib/lean/Lake/Build/Fetch.ilean +lib/lean/Lake/Build/Fetch.olean lib/lean/Lake/Build/Imports.ilean lib/lean/Lake/Build/Imports.olean lib/lean/Lake/Build/Index.ilean @@ -332,10 +354,10 @@ lib/lean/Lake/Build/Library.ilean lib/lean/Lake/Build/Library.olean lib/lean/Lake/Build/Module.ilean lib/lean/Lake/Build/Module.olean -lib/lean/Lake/Build/Monad.ilean -lib/lean/Lake/Build/Monad.olean lib/lean/Lake/Build/Package.ilean lib/lean/Lake/Build/Package.olean +lib/lean/Lake/Build/Run.ilean +lib/lean/Lake/Build/Run.olean lib/lean/Lake/Build/Store.ilean lib/lean/Lake/Build/Store.olean lib/lean/Lake/Build/Targets.ilean @@ -360,6 +382,12 @@ lib/lean/Lake/CLI/Main.ilean lib/lean/Lake/CLI/Main.olean lib/lean/Lake/CLI/Serve.ilean lib/lean/Lake/CLI/Serve.olean +lib/lean/Lake/CLI/Translate.ilean +lib/lean/Lake/CLI/Translate.olean +lib/lean/Lake/CLI/Translate/Lean.ilean +lib/lean/Lake/CLI/Translate/Lean.olean +lib/lean/Lake/CLI/Translate/Toml.ilean +lib/lean/Lake/CLI/Translate/Toml.olean lib/lean/Lake/Config.ilean lib/lean/Lake/Config.olean lib/lean/Lake/Config/Context.ilean @@ -380,6 +408,8 @@ lib/lean/Lake/Config/Glob.ilean lib/lean/Lake/Config/Glob.olean lib/lean/Lake/Config/InstallPath.ilean lib/lean/Lake/Config/InstallPath.olean +lib/lean/Lake/Config/Lang.ilean +lib/lean/Lake/Config/Lang.olean lib/lean/Lake/Config/LeanConfig.ilean lib/lean/Lake/Config/LeanConfig.olean lib/lean/Lake/Config/LeanExe.ilean @@ -440,10 +470,36 @@ lib/lean/Lake/Load/Materialize.ilean lib/lean/Lake/Load/Materialize.olean lib/lean/Lake/Load/Package.ilean lib/lean/Lake/Load/Package.olean +lib/lean/Lake/Load/Toml.ilean +lib/lean/Lake/Load/Toml.olean lib/lean/Lake/Main.ilean lib/lean/Lake/Main.olean -lib/lean/Lake/Util/Async.ilean -lib/lean/Lake/Util/Async.olean +lib/lean/Lake/Toml.ilean +lib/lean/Lake/Toml.olean +lib/lean/Lake/Toml/Data.ilean +lib/lean/Lake/Toml/Data.olean +lib/lean/Lake/Toml/Data/DateTime.ilean +lib/lean/Lake/Toml/Data/DateTime.olean +lib/lean/Lake/Toml/Data/Dict.ilean +lib/lean/Lake/Toml/Data/Dict.olean +lib/lean/Lake/Toml/Data/Value.ilean +lib/lean/Lake/Toml/Data/Value.olean +lib/lean/Lake/Toml/Decode.ilean +lib/lean/Lake/Toml/Decode.olean +lib/lean/Lake/Toml/Elab.ilean +lib/lean/Lake/Toml/Elab.olean +lib/lean/Lake/Toml/Elab/Expression.ilean +lib/lean/Lake/Toml/Elab/Expression.olean +lib/lean/Lake/Toml/Elab/Value.ilean +lib/lean/Lake/Toml/Elab/Value.olean +lib/lean/Lake/Toml/Encode.ilean +lib/lean/Lake/Toml/Encode.olean +lib/lean/Lake/Toml/Grammar.ilean +lib/lean/Lake/Toml/Grammar.olean +lib/lean/Lake/Toml/Load.ilean +lib/lean/Lake/Toml/Load.olean +lib/lean/Lake/Toml/ParserUtil.ilean +lib/lean/Lake/Toml/ParserUtil.olean lib/lean/Lake/Util/Binder.ilean lib/lean/Lake/Util/Binder.olean lib/lean/Lake/Util/Casing.ilean @@ -466,24 +522,32 @@ lib/lean/Lake/Util/Exit.ilean lib/lean/Lake/Util/Exit.olean lib/lean/Lake/Util/Family.ilean lib/lean/Lake/Util/Family.olean +lib/lean/Lake/Util/FilePath.ilean +lib/lean/Lake/Util/FilePath.olean lib/lean/Lake/Util/Git.ilean lib/lean/Lake/Util/Git.olean +lib/lean/Lake/Util/IO.ilean +lib/lean/Lake/Util/IO.olean lib/lean/Lake/Util/Lift.ilean lib/lean/Lake/Util/Lift.olean lib/lean/Lake/Util/List.ilean lib/lean/Lake/Util/List.olean +lib/lean/Lake/Util/Lock.ilean +lib/lean/Lake/Util/Lock.olean lib/lean/Lake/Util/Log.ilean lib/lean/Lake/Util/Log.olean lib/lean/Lake/Util/MainM.ilean lib/lean/Lake/Util/MainM.olean +lib/lean/Lake/Util/Message.ilean +lib/lean/Lake/Util/Message.olean lib/lean/Lake/Util/Name.ilean lib/lean/Lake/Util/Name.olean lib/lean/Lake/Util/NativeLib.ilean lib/lean/Lake/Util/NativeLib.olean +lib/lean/Lake/Util/Newline.ilean +lib/lean/Lake/Util/Newline.olean lib/lean/Lake/Util/Opaque.ilean lib/lean/Lake/Util/Opaque.olean -lib/lean/Lake/Util/OptionIO.ilean -lib/lean/Lake/Util/OptionIO.olean lib/lean/Lake/Util/OrdHashSet.ilean lib/lean/Lake/Util/OrdHashSet.olean lib/lean/Lake/Util/OrderedTagAttribute.ilean @@ -508,6 +572,8 @@ lib/lean/Lean/Attributes.ilean lib/lean/Lean/Attributes.olean lib/lean/Lean/AuxRecursor.ilean lib/lean/Lean/AuxRecursor.olean +lib/lean/Lean/BuiltinDocAttr.ilean +lib/lean/Lean/BuiltinDocAttr.olean lib/lean/Lean/Class.ilean lib/lean/Lean/Class.olean lib/lean/Lean/Compiler.ilean @@ -790,6 +856,8 @@ lib/lean/Lean/Data/Lsp/TextSync.ilean lib/lean/Lean/Data/Lsp/TextSync.olean lib/lean/Lean/Data/Lsp/Utf16.ilean lib/lean/Lean/Data/Lsp/Utf16.olean +lib/lean/Lean/Data/Lsp/Window.ilean +lib/lean/Lean/Data/Lsp/Window.olean lib/lean/Lean/Data/Lsp/Workspace.ilean lib/lean/Lean/Data/Lsp/Workspace.olean lib/lean/Lean/Data/Name.ilean @@ -874,6 +942,8 @@ lib/lean/Lean/Elab/Config.ilean lib/lean/Lean/Elab/Config.olean lib/lean/Lean/Elab/DeclModifiers.ilean lib/lean/Lean/Elab/DeclModifiers.olean +lib/lean/Lean/Elab/DeclNameGen.ilean +lib/lean/Lean/Elab/DeclNameGen.olean lib/lean/Lean/Elab/DeclUtil.ilean lib/lean/Lean/Elab/DeclUtil.olean lib/lean/Lean/Elab/Declaration.ilean @@ -1004,14 +1074,14 @@ lib/lean/Lean/Elab/PreDefinition/WF/Ite.ilean lib/lean/Lean/Elab/PreDefinition/WF/Ite.olean lib/lean/Lean/Elab/PreDefinition/WF/Main.ilean lib/lean/Lean/Elab/PreDefinition/WF/Main.olean -lib/lean/Lean/Elab/PreDefinition/WF/PackDomain.ilean -lib/lean/Lean/Elab/PreDefinition/WF/PackDomain.olean lib/lean/Lean/Elab/PreDefinition/WF/PackMutual.ilean lib/lean/Lean/Elab/PreDefinition/WF/PackMutual.olean 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 @@ -1110,6 +1180,10 @@ lib/lean/Lean/Elab/Tactic/Repeat.ilean lib/lean/Lean/Elab/Tactic/Repeat.olean lib/lean/Lean/Elab/Tactic/Rewrite.ilean lib/lean/Lean/Elab/Tactic/Rewrite.olean +lib/lean/Lean/Elab/Tactic/Rewrites.ilean +lib/lean/Lean/Elab/Tactic/Rewrites.olean +lib/lean/Lean/Elab/Tactic/Rfl.ilean +lib/lean/Lean/Elab/Tactic/Rfl.olean lib/lean/Lean/Elab/Tactic/ShowTerm.ilean lib/lean/Lean/Elab/Tactic/ShowTerm.olean lib/lean/Lean/Elab/Tactic/Simp.ilean @@ -1152,6 +1226,10 @@ lib/lean/Lean/KeyedDeclsAttribute.ilean lib/lean/Lean/KeyedDeclsAttribute.olean lib/lean/Lean/LabelAttribute.ilean lib/lean/Lean/LabelAttribute.olean +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/LazyInitExtension.ilean lib/lean/Lean/LazyInitExtension.olean lib/lean/Lean/Level.ilean @@ -1188,10 +1266,18 @@ lib/lean/Lean/Meta/AbstractNestedProofs.ilean lib/lean/Lean/Meta/AbstractNestedProofs.olean lib/lean/Lean/Meta/AppBuilder.ilean lib/lean/Lean/Meta/AppBuilder.olean +lib/lean/Lean/Meta/ArgsPacker.ilean +lib/lean/Lean/Meta/ArgsPacker.olean +lib/lean/Lean/Meta/ArgsPacker/Basic.ilean +lib/lean/Lean/Meta/ArgsPacker/Basic.olean lib/lean/Lean/Meta/Basic.ilean lib/lean/Lean/Meta/Basic.olean +lib/lean/Lean/Meta/Canonicalizer.ilean +lib/lean/Lean/Meta/Canonicalizer.olean lib/lean/Lean/Meta/Check.ilean lib/lean/Lean/Meta/Check.olean +lib/lean/Lean/Meta/CheckTactic.ilean +lib/lean/Lean/Meta/CheckTactic.olean lib/lean/Lean/Meta/Closure.ilean lib/lean/Lean/Meta/Closure.olean lib/lean/Lean/Meta/Coe.ilean @@ -1212,6 +1298,8 @@ lib/lean/Lean/Meta/CtorRecognizer.ilean lib/lean/Lean/Meta/CtorRecognizer.olean lib/lean/Lean/Meta/DecLevel.ilean lib/lean/Lean/Meta/DecLevel.olean +lib/lean/Lean/Meta/Diagnostics.ilean +lib/lean/Lean/Meta/Diagnostics.olean lib/lean/Lean/Meta/DiscrTree.ilean lib/lean/Lean/Meta/DiscrTree.olean lib/lean/Lean/Meta/DiscrTreeTypes.ilean @@ -1290,6 +1378,8 @@ lib/lean/Lean/Meta/Match/Value.ilean lib/lean/Lean/Meta/Match/Value.olean lib/lean/Lean/Meta/MatchUtil.ilean lib/lean/Lean/Meta/MatchUtil.olean +lib/lean/Lean/Meta/NatInstTesters.ilean +lib/lean/Lean/Meta/NatInstTesters.olean lib/lean/Lean/Meta/Offset.ilean lib/lean/Lean/Meta/Offset.olean lib/lean/Lean/Meta/PPGoal.ilean @@ -1342,6 +1432,8 @@ lib/lean/Lean/Meta/Tactic/ElimInfo.ilean lib/lean/Lean/Meta/Tactic/ElimInfo.olean lib/lean/Lean/Meta/Tactic/FVarSubst.ilean lib/lean/Lean/Meta/Tactic/FVarSubst.olean +lib/lean/Lean/Meta/Tactic/FunInd.ilean +lib/lean/Lean/Meta/Tactic/FunInd.olean lib/lean/Lean/Meta/Tactic/Generalize.ilean lib/lean/Lean/Meta/Tactic/Generalize.olean lib/lean/Lean/Meta/Tactic/IndependentOf.ilean @@ -1386,6 +1478,10 @@ lib/lean/Lean/Meta/Tactic/Revert.ilean lib/lean/Lean/Meta/Tactic/Revert.olean lib/lean/Lean/Meta/Tactic/Rewrite.ilean lib/lean/Lean/Meta/Tactic/Rewrite.olean +lib/lean/Lean/Meta/Tactic/Rewrites.ilean +lib/lean/Lean/Meta/Tactic/Rewrites.olean +lib/lean/Lean/Meta/Tactic/Rfl.ilean +lib/lean/Lean/Meta/Tactic/Rfl.olean lib/lean/Lean/Meta/Tactic/Simp.ilean lib/lean/Lean/Meta/Tactic/Simp.olean lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean @@ -1410,6 +1506,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.olean +lib/lean/Lean/Meta/Tactic/Simp/Diagnostics.ilean +lib/lean/Lean/Meta/Tactic/Simp/Diagnostics.olean lib/lean/Lean/Meta/Tactic/Simp/Main.ilean lib/lean/Lean/Meta/Tactic/Simp/Main.olean lib/lean/Lean/Meta/Tactic/Simp/RegisterCommand.ilean @@ -1496,10 +1594,14 @@ lib/lean/Lean/PrettyPrinter/Basic.ilean lib/lean/Lean/PrettyPrinter/Basic.olean lib/lean/Lean/PrettyPrinter/Delaborator.ilean lib/lean/Lean/PrettyPrinter/Delaborator.olean +lib/lean/Lean/PrettyPrinter/Delaborator/Attributes.ilean +lib/lean/Lean/PrettyPrinter/Delaborator/Attributes.olean lib/lean/Lean/PrettyPrinter/Delaborator/Basic.ilean lib/lean/Lean/PrettyPrinter/Delaborator/Basic.olean lib/lean/Lean/PrettyPrinter/Delaborator/Builtins.ilean lib/lean/Lean/PrettyPrinter/Delaborator/Builtins.olean +lib/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.ilean +lib/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.olean lib/lean/Lean/PrettyPrinter/Delaborator/Options.ilean lib/lean/Lean/PrettyPrinter/Delaborator/Options.olean lib/lean/Lean/PrettyPrinter/Delaborator/SubExpr.ilean @@ -1516,6 +1618,8 @@ lib/lean/Lean/ReducibilityAttrs.ilean lib/lean/Lean/ReducibilityAttrs.olean lib/lean/Lean/Replay.ilean lib/lean/Lean/Replay.olean +lib/lean/Lean/ReservedNameAction.ilean +lib/lean/Lean/ReservedNameAction.olean lib/lean/Lean/ResolveName.ilean lib/lean/Lean/ResolveName.olean lib/lean/Lean/Runtime.ilean @@ -1590,6 +1694,8 @@ lib/lean/Lean/Util/CollectLevelParams.ilean lib/lean/Lean/Util/CollectLevelParams.olean lib/lean/Lean/Util/CollectMVars.ilean lib/lean/Lean/Util/CollectMVars.olean +lib/lean/Lean/Util/Diff.ilean +lib/lean/Lean/Util/Diff.olean lib/lean/Lean/Util/FileSetupInfo.ilean lib/lean/Lean/Util/FileSetupInfo.olean lib/lean/Lean/Util/FindExpr.ilean @@ -1628,6 +1734,8 @@ lib/lean/Lean/Util/Paths.ilean lib/lean/Lean/Util/Paths.olean lib/lean/Lean/Util/Profile.ilean lib/lean/Lean/Util/Profile.olean +lib/lean/Lean/Util/Profiler.ilean +lib/lean/Lean/Util/Profiler.olean lib/lean/Lean/Util/PtrSet.ilean lib/lean/Lean/Util/PtrSet.olean lib/lean/Lean/Util/RecDepth.ilean @@ -1686,6 +1794,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Control/ExceptCps.lean %%DATADIR%%/src/lean/Init/Control/Id.lean %%DATADIR%%/src/lean/Init/Control/Lawful.lean +%%DATADIR%%/src/lean/Init/Control/Lawful/Basic.lean +%%DATADIR%%/src/lean/Init/Control/Lawful/Instances.lean %%DATADIR%%/src/lean/Init/Control/Option.lean %%DATADIR%%/src/lean/Init/Control/Reader.lean %%DATADIR%%/src/lean/Init/Control/State.lean @@ -1705,6 +1815,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Array/Mem.lean %%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/Basic.lean %%DATADIR%%/src/lean/Init/Data/BitVec.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean @@ -1741,20 +1852,24 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean %%DATADIR%%/src/lean/Init/Data/Int/Lemmas.lean %%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/Basic.lean %%DATADIR%%/src/lean/Init/Data/List/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/List/Control.lean +%%DATADIR%%/src/lean/Init/Data/List/Impl.lean %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Nat.lean %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Compare.lean %%DATADIR%%/src/lean/Init/Data/Nat/Control.lean %%DATADIR%%/src/lean/Init/Data/Nat/Div.lean %%DATADIR%%/src/lean/Init/Data/Nat/Dvd.lean %%DATADIR%%/src/lean/Init/Data/Nat/Gcd.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Lcm.lean %%DATADIR%%/src/lean/Init/Data/Nat/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Nat/Linear.lean %%DATADIR%%/src/lean/Init/Data/Nat/Log2.lean @@ -1762,6 +1877,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Nat/Mod.lean %%DATADIR%%/src/lean/Init/Data/Nat/Power2.lean %%DATADIR%%/src/lean/Init/Data/Nat/SOM.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Simproc.lean %%DATADIR%%/src/lean/Init/Data/OfScientific.lean %%DATADIR%%/src/lean/Init/Data/Option.lean %%DATADIR%%/src/lean/Init/Data/Option/Basic.lean @@ -1787,8 +1903,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean %%DATADIR%%/src/lean/Init/Dynamic.lean %%DATADIR%%/src/lean/Init/Ext.lean +%%DATADIR%%/src/lean/Init/GetElem.lean %%DATADIR%%/src/lean/Init/Guard.lean %%DATADIR%%/src/lean/Init/Hints.lean +%%DATADIR%%/src/lean/Init/MacroTrace.lean %%DATADIR%%/src/lean/Init/Meta.lean %%DATADIR%%/src/lean/Init/MetaTypes.lean %%DATADIR%%/src/lean/Init/Notation.lean @@ -1825,6 +1943,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean.lean %%DATADIR%%/src/lean/Lean/Attributes.lean %%DATADIR%%/src/lean/Lean/AuxRecursor.lean +%%DATADIR%%/src/lean/Lean/BuiltinDocAttr.lean %%DATADIR%%/src/lean/Lean/Class.lean %%DATADIR%%/src/lean/Lean/Compiler.lean %%DATADIR%%/src/lean/Lean/Compiler/AtMostOnce.lean @@ -1966,6 +2085,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Data/Lsp/LanguageFeatures.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/TextSync.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/Utf16.lean +%%DATADIR%%/src/lean/Lean/Data/Lsp/Window.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/Workspace.lean %%DATADIR%%/src/lean/Lean/Data/Name.lean %%DATADIR%%/src/lean/Lean/Data/NameMap.lean @@ -2008,6 +2128,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/ComputedFields.lean %%DATADIR%%/src/lean/Lean/Elab/Config.lean %%DATADIR%%/src/lean/Lean/Elab/DeclModifiers.lean +%%DATADIR%%/src/lean/Lean/Elab/DeclNameGen.lean %%DATADIR%%/src/lean/Lean/Elab/DeclUtil.lean %%DATADIR%%/src/lean/Lean/Elab/Declaration.lean %%DATADIR%%/src/lean/Lean/Elab/DeclarationRange.lean @@ -2073,10 +2194,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/GuessLex.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Ite.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Main.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackDomain.lean %%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 @@ -2126,6 +2247,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/RCases.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Repeat.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrite.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrites.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Rfl.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ShowTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simp.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/SimpTrace.lean @@ -2147,6 +2270,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/InternalExceptionId.lean %%DATADIR%%/src/lean/Lean/KeyedDeclsAttribute.lean %%DATADIR%%/src/lean/Lean/LabelAttribute.lean +%%DATADIR%%/src/lean/Lean/Language/Basic.lean +%%DATADIR%%/src/lean/Lean/Language/Lean.lean %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean %%DATADIR%%/src/lean/Lean/Level.lean %%DATADIR%%/src/lean/Lean/Linter.lean @@ -2165,8 +2290,12 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/AbstractMVars.lean %%DATADIR%%/src/lean/Lean/Meta/AbstractNestedProofs.lean %%DATADIR%%/src/lean/Lean/Meta/AppBuilder.lean +%%DATADIR%%/src/lean/Lean/Meta/ArgsPacker.lean +%%DATADIR%%/src/lean/Lean/Meta/ArgsPacker/Basic.lean %%DATADIR%%/src/lean/Lean/Meta/Basic.lean +%%DATADIR%%/src/lean/Lean/Meta/Canonicalizer.lean %%DATADIR%%/src/lean/Lean/Meta/Check.lean +%%DATADIR%%/src/lean/Lean/Meta/CheckTactic.lean %%DATADIR%%/src/lean/Lean/Meta/Closure.lean %%DATADIR%%/src/lean/Lean/Meta/Coe.lean %%DATADIR%%/src/lean/Lean/Meta/CoeAttr.lean @@ -2177,6 +2306,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean +%%DATADIR%%/src/lean/Lean/Meta/Diagnostics.lean %%DATADIR%%/src/lean/Lean/Meta/DiscrTree.lean %%DATADIR%%/src/lean/Lean/Meta/DiscrTreeTypes.lean %%DATADIR%%/src/lean/Lean/Meta/Eqns.lean @@ -2216,6 +2346,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Match/MatcherInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Match/Value.lean %%DATADIR%%/src/lean/Lean/Meta/MatchUtil.lean +%%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/RecursorInfo.lean @@ -2242,6 +2373,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Delta.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/ElimInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/FunInd.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/IndependentOf.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Induction.lean @@ -2264,6 +2396,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Replace.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Revert.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rewrite.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Rewrites.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Rfl.lean %%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 @@ -2276,6 +2410,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Diagnostics.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Main.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/RegisterCommand.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -2319,8 +2454,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/PrettyPrinter.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Basic.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator.lean +%%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Attributes.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Basic.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Builtins.lean +%%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Options.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/SubExpr.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -2329,6 +2466,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/ProjFns.lean %%DATADIR%%/src/lean/Lean/ReducibilityAttrs.lean %%DATADIR%%/src/lean/Lean/Replay.lean +%%DATADIR%%/src/lean/Lean/ReservedNameAction.lean %%DATADIR%%/src/lean/Lean/ResolveName.lean %%DATADIR%%/src/lean/Lean/Runtime.lean %%DATADIR%%/src/lean/Lean/ScopedEnvExtension.lean @@ -2367,6 +2505,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean +%%DATADIR%%/src/lean/Lean/Util/Diff.lean %%DATADIR%%/src/lean/Lean/Util/FileSetupInfo.lean %%DATADIR%%/src/lean/Lean/Util/FindExpr.lean %%DATADIR%%/src/lean/Lean/Util/FindLevelMVar.lean @@ -2386,6 +2525,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/Path.lean %%DATADIR%%/src/lean/Lean/Util/Paths.lean %%DATADIR%%/src/lean/Lean/Util/Profile.lean +%%DATADIR%%/src/lean/Lean/Util/Profiler.lean %%DATADIR%%/src/lean/Lean/Util/PtrSet.lean %%DATADIR%%/src/lean/Lean/Util/RecDepth.lean %%DATADIR%%/src/lean/Lean/Util/Recognizers.lean @@ -2409,11 +2549,12 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake.lean %%DATADIR%%/src/lean/lake/Lake/Build.lean %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Basic.lean %%DATADIR%%/src/lean/lake/Lake/Build/Common.lean -%%DATADIR%%/src/lean/lake/Lake/Build/Context.lean %%DATADIR%%/src/lean/lake/Lake/Build/Data.lean %%DATADIR%%/src/lean/lake/Lake/Build/Executable.lean %%DATADIR%%/src/lean/lake/Lake/Build/Facets.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Fetch.lean %%DATADIR%%/src/lean/lake/Lake/Build/Imports.lean %%DATADIR%%/src/lean/lake/Lake/Build/Index.lean %%DATADIR%%/src/lean/lake/Lake/Build/Info.lean @@ -2421,8 +2562,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Build/Key.lean %%DATADIR%%/src/lean/lake/Lake/Build/Library.lean %%DATADIR%%/src/lean/lake/Lake/Build/Module.lean -%%DATADIR%%/src/lean/lake/Lake/Build/Monad.lean %%DATADIR%%/src/lean/lake/Lake/Build/Package.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Run.lean %%DATADIR%%/src/lean/lake/Lake/Build/Store.lean %%DATADIR%%/src/lean/lake/Lake/Build/Targets.lean %%DATADIR%%/src/lean/lake/Lake/Build/Topological.lean @@ -2435,6 +2576,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/CLI/Init.lean %%DATADIR%%/src/lean/lake/Lake/CLI/Main.lean %%DATADIR%%/src/lean/lake/Lake/CLI/Serve.lean +%%DATADIR%%/src/lean/lake/Lake/CLI/Translate.lean +%%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Lean.lean +%%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Toml.lean %%DATADIR%%/src/lean/lake/Lake/Config.lean %%DATADIR%%/src/lean/lake/Lake/Config/Context.lean %%DATADIR%%/src/lean/lake/Lake/Config/Defaults.lean @@ -2445,6 +2589,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Config/FacetConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/Glob.lean %%DATADIR%%/src/lean/lake/Lake/Config/InstallPath.lean +%%DATADIR%%/src/lean/lake/Lake/Config/Lang.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanExe.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanExeConfig.lean @@ -2475,8 +2620,21 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Load/Manifest.lean %%DATADIR%%/src/lean/lake/Lake/Load/Materialize.lean %%DATADIR%%/src/lean/lake/Lake/Load/Package.lean +%%DATADIR%%/src/lean/lake/Lake/Load/Toml.lean %%DATADIR%%/src/lean/lake/Lake/Main.lean -%%DATADIR%%/src/lean/lake/Lake/Util/Async.lean +%%DATADIR%%/src/lean/lake/Lake/Toml.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Data.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Data/DateTime.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Data/Dict.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Data/Value.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Decode.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Elab.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Elab/Expression.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Elab/Value.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Encode.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Grammar.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/Load.lean +%%DATADIR%%/src/lean/lake/Lake/Toml/ParserUtil.lean %%DATADIR%%/src/lean/lake/Lake/Util/Binder.lean %%DATADIR%%/src/lean/lake/Lake/Util/Casing.lean %%DATADIR%%/src/lean/lake/Lake/Util/Cli.lean @@ -2488,15 +2646,19 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/Error.lean %%DATADIR%%/src/lean/lake/Lake/Util/Exit.lean %%DATADIR%%/src/lean/lake/Lake/Util/Family.lean +%%DATADIR%%/src/lean/lake/Lake/Util/FilePath.lean %%DATADIR%%/src/lean/lake/Lake/Util/Git.lean +%%DATADIR%%/src/lean/lake/Lake/Util/IO.lean %%DATADIR%%/src/lean/lake/Lake/Util/Lift.lean %%DATADIR%%/src/lean/lake/Lake/Util/List.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Lock.lean %%DATADIR%%/src/lean/lake/Lake/Util/Log.lean %%DATADIR%%/src/lean/lake/Lake/Util/MainM.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Message.lean %%DATADIR%%/src/lean/lake/Lake/Util/Name.lean %%DATADIR%%/src/lean/lake/Lake/Util/NativeLib.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Newline.lean %%DATADIR%%/src/lean/lake/Lake/Util/Opaque.lean -%%DATADIR%%/src/lean/lake/Lake/Util/OptionIO.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrdHashSet.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean %%DATADIR%%/src/lean/lake/Lake/Util/Proc.lean @@ -2510,6 +2672,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/lakefile.lean %%DATADIR%%/src/lean/lake/tests/badImport/Lib/A.lean %%DATADIR%%/src/lean/lake/tests/badImport/Lib/B.lean +%%DATADIR%%/src/lean/lake/tests/badImport/Lib/C.lean %%DATADIR%%/src/lean/lake/tests/badImport/X.lean %%DATADIR%%/src/lean/lake/tests/badImport/lakefile.lean %%DATADIR%%/src/lean/lake/tests/buildArgs/Hello.lean @@ -2524,6 +2687,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/globs/Test/1.lean %%DATADIR%%/src/lean/lake/tests/globs/Test/Subtest/1.lean %%DATADIR%%/src/lean/lake/tests/globs/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/lean/Lib.lean +%%DATADIR%%/src/lean/lake/tests/lean/Lib/Basic.lean +%%DATADIR%%/src/lean/lake/tests/lean/Test.lean +%%DATADIR%%/src/lean/lake/tests/lean/lakefile.lean %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/Main.lean @@ -2539,6 +2706,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/meta/lakefile.lean %%DATADIR%%/src/lean/lake/tests/noBuild/Test.lean %%DATADIR%%/src/lean/lake/tests/noBuild/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/noRelease/Test.lean +%%DATADIR%%/src/lean/lake/tests/noRelease/dep/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/noRelease/lakefile.lean %%DATADIR%%/src/lean/lake/tests/order/A.lean %%DATADIR%%/src/lean/lake/tests/order/A/B.lean %%DATADIR%%/src/lean/lake/tests/order/A/B/C.lean @@ -2558,3 +2728,17 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/precompileArgs/lakefile.lean %%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean %%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean +%%DATADIR%%/src/lean/lake/tests/reversion/Main.lean +%%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/test/exe.lean +%%DATADIR%%/src/lean/lake/tests/test/none.lean +%%DATADIR%%/src/lean/lake/tests/test/script.lean +%%DATADIR%%/src/lean/lake/tests/test/test.lean +%%DATADIR%%/src/lean/lake/tests/test/two.lean +%%DATADIR%%/src/lean/lake/tests/toml/README.md +%%DATADIR%%/src/lean/lake/tests/toml/Test.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