From nobody Mon Sep 05 17:52:22 2022 X-Original-To: dev-commits-ports-branches@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 4MLx1L6lq0z4bDtl; Mon, 5 Sep 2022 17:52:22 +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 4MLx1L6Zlbz4BmM; Mon, 5 Sep 2022 17:52:22 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1662400342; 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=8juc6xufUg/5aMy1tf71uaVIzSwcUkEctGIb4KZgGzA=; b=aEK7jfaUyCD8+DXq/0ZjR05BuOM+vialdlRIiT2i2EvjwNvbPF7e+Lq76da5L02J/K3+dd E6M91aemuiRCHRD1rcvaUFaFU0qg8JAQqjBo9a5v9ZPmlzwfvaD4isCOsxf/KK2D55YXql 3dXFRuTdeeSG11CGAlW1MXSLuSB9EYYJ7/dJboICuccg1n30F2vjDG/JYWxQer7ZQ0bPka Kv7WcRV6qrZSZEdI9H/HfTRFpWLA6015tlYgSAO8EpFzQdFWvswxp5z17AGnpzFdD/Ji1Q 25unkpp5beRP9BrQuEUkeFouaUK9LfvqrgYs8A7wFk/xshEHXBBIgk/iMxtooQ== 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 4MLx1L5KPkztk3; Mon, 5 Sep 2022 17:52:22 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.16.1/8.16.1) with ESMTP id 285HqMKG024098; Mon, 5 Sep 2022 17:52:22 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.16.1/8.16.1/Submit) id 285HqM4I024097; Mon, 5 Sep 2022 17:52:22 GMT (envelope-from git) Date: Mon, 5 Sep 2022 17:52:22 GMT Message-Id: <202209051752.285HqM4I024097@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-branches@FreeBSD.org From: Yuri Victorovich Subject: git: 56e03a4e58bc - 2022Q3 - math/lean: Fix performance problem List-Id: Commits to the quarterly branches of the FreeBSD ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-branches List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-dev-commits-ports-branches@freebsd.org X-BeenThere: dev-commits-ports-branches@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/2022Q3 X-Git-Reftype: branch X-Git-Commit: 56e03a4e58bc9d9380a8e0cd94274bfcde1a89c3 Auto-Submitted: auto-generated ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1662400342; 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=8juc6xufUg/5aMy1tf71uaVIzSwcUkEctGIb4KZgGzA=; b=MgVfS/cGWnS39bld1Dw4vYWkHvf6e5401NNO3YOd9f4W7LjAgCFfK4uZ+Wfo3WZ7Nu0dyQ /splzIUtLiuwar4rBHtbXAu5x2eBh8a52YVijCPDdHON+HB+LjaOqAErGucr8ViYy6KV50 9LszBDfg8qyK2CA2rGO5KJIPnmR4bgLcqAm9ZRuURsQKZNDKEfIgMfwT7zDgChxVUHi9JP 8/delQg+f3pUvNTryN8aR8jyYQbNPiK1ybIOlXYnpQPkSmxJcIxwbSMw2A3bWGGUAlBJz/ h3R5Yfw2h8o8yPPcCtQ/BjCpyqLkBNv+xD/EMMfWpzQMSmkTrq0XyEcr5AQ7yQ== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1662400342; a=rsa-sha256; cv=none; b=UdJ9WCw5s3OvXgrhe2EccHuB6GiAq1tATGZmKdc0i69f5iMxOA8VN4BwfGZ7yAJU9sqFuF 9h9WejTblNdzPC4eED0La7c1z1uSbILC9Nda39dmVHSp+xE8SoLKy6d61GfvGunBojEy3h zdbxO73lSLoClwQiSQgOGPcu9lBiP3l0tt/pH4wMpUCggnY0UNvXkemr4JtZ1nChpowDJV L1wlmttPuIU6r+cwQbiZgqxtSaCN6BQjPEfeSECDH8es4ZWEzPNdW9xOWyKdtuf0m6ekpL 8bkTUh2Ovy+Mw+Yv9h+JazP38qfQ+X4u6YdA9+61nUK5KOtzR9QhrEJ7EIdV2Q== ARC-Authentication-Results: i=1; mx1.freebsd.org; none X-ThisMailContainsUnwantedMimeParts: N The branch 2022Q3 has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=56e03a4e58bc9d9380a8e0cd94274bfcde1a89c3 commit 56e03a4e58bc9d9380a8e0cd94274bfcde1a89c3 Author: Yuri Victorovich AuthorDate: 2022-09-05 17:37:43 +0000 Commit: Yuri Victorovich CommitDate: 2022-09-05 17:52:20 +0000 math/lean: Fix performance problem Pre-compiled library files weren't installed due to some bug which made lean very slow. (cherry picked from commit 2317424cb6092aa0430b738cd19199089dfb3bab) --- math/lean/Makefile | 4 ++ math/lean/pkg-plist | 174 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 178 insertions(+) diff --git a/math/lean/Makefile b/math/lean/Makefile index 444b6372fd33..2cee6bd5ebe8 100644 --- a/math/lean/Makefile +++ b/math/lean/Makefile @@ -1,6 +1,7 @@ PORTNAME= lean DISTVERSIONPREFIX= v DISTVERSION= 3.44.1 +PORTREVISION= 1 CATEGORIES= math MAINTAINER= yuri@FreeBSD.org @@ -21,6 +22,9 @@ WRKSRC_SUBDIR= src CMAKE_OFF= BUILD_TESTING CMAKE_TESTING_ON= BUILD_TESTING +post-build: # workaround for https://github.com/leanprover-community/lean/issues/765 + @cd ${WRKSRC}/../library && ${BUILD_WRKSRC}/shell/lean --make + post-install: @${FIND} ${STAGEDIR}${PREFIX} -type d -empty -delete diff --git a/math/lean/pkg-plist b/math/lean/pkg-plist index 170a58fed99e..ade817a020e2 100644 --- a/math/lean/pkg-plist +++ b/math/lean/pkg-plist @@ -401,178 +401,352 @@ lib/lean/leanpkg/leanpkg/proc.lean lib/lean/leanpkg/leanpkg/resolve.lean lib/lean/leanpkg/leanpkg/toml.lean lib/lean/library/data/buffer.lean +lib/lean/library/data/buffer.olean lib/lean/library/data/buffer/parser.lean +lib/lean/library/data/buffer/parser.olean lib/lean/library/data/dlist.lean +lib/lean/library/data/dlist.olean lib/lean/library/data/vector.lean +lib/lean/library/data/vector.olean lib/lean/library/init/algebra/classes.lean +lib/lean/library/init/algebra/classes.olean lib/lean/library/init/algebra/default.lean +lib/lean/library/init/algebra/default.olean lib/lean/library/init/algebra/functions.lean +lib/lean/library/init/algebra/functions.olean lib/lean/library/init/algebra/order.lean +lib/lean/library/init/algebra/order.olean lib/lean/library/init/cc_lemmas.lean +lib/lean/library/init/cc_lemmas.olean lib/lean/library/init/classical.lean +lib/lean/library/init/classical.olean lib/lean/library/init/coe.lean +lib/lean/library/init/coe.olean lib/lean/library/init/control/alternative.lean +lib/lean/library/init/control/alternative.olean lib/lean/library/init/control/applicative.lean +lib/lean/library/init/control/applicative.olean lib/lean/library/init/control/combinators.lean +lib/lean/library/init/control/combinators.olean lib/lean/library/init/control/default.lean +lib/lean/library/init/control/default.olean lib/lean/library/init/control/except.lean +lib/lean/library/init/control/except.olean lib/lean/library/init/control/functor.lean +lib/lean/library/init/control/functor.olean lib/lean/library/init/control/id.lean +lib/lean/library/init/control/id.olean lib/lean/library/init/control/lawful.lean +lib/lean/library/init/control/lawful.olean lib/lean/library/init/control/lift.lean +lib/lean/library/init/control/lift.olean lib/lean/library/init/control/monad.lean +lib/lean/library/init/control/monad.olean lib/lean/library/init/control/monad_fail.lean +lib/lean/library/init/control/monad_fail.olean lib/lean/library/init/control/option.lean +lib/lean/library/init/control/option.olean lib/lean/library/init/control/reader.lean +lib/lean/library/init/control/reader.olean lib/lean/library/init/control/state.lean +lib/lean/library/init/control/state.olean lib/lean/library/init/core.lean +lib/lean/library/init/core.olean lib/lean/library/init/data/array/basic.lean +lib/lean/library/init/data/array/basic.olean lib/lean/library/init/data/array/default.lean +lib/lean/library/init/data/array/default.olean lib/lean/library/init/data/array/slice.lean +lib/lean/library/init/data/array/slice.olean lib/lean/library/init/data/basic.lean +lib/lean/library/init/data/basic.olean lib/lean/library/init/data/bool/basic.lean +lib/lean/library/init/data/bool/basic.olean lib/lean/library/init/data/bool/default.lean +lib/lean/library/init/data/bool/default.olean lib/lean/library/init/data/bool/lemmas.lean +lib/lean/library/init/data/bool/lemmas.olean lib/lean/library/init/data/char/basic.lean +lib/lean/library/init/data/char/basic.olean lib/lean/library/init/data/char/classes.lean +lib/lean/library/init/data/char/classes.olean lib/lean/library/init/data/char/default.lean +lib/lean/library/init/data/char/default.olean lib/lean/library/init/data/char/lemmas.lean +lib/lean/library/init/data/char/lemmas.olean lib/lean/library/init/data/default.lean +lib/lean/library/init/data/default.olean lib/lean/library/init/data/fin/basic.lean +lib/lean/library/init/data/fin/basic.olean lib/lean/library/init/data/fin/default.lean +lib/lean/library/init/data/fin/default.olean lib/lean/library/init/data/fin/ops.lean +lib/lean/library/init/data/fin/ops.olean lib/lean/library/init/data/int/basic.lean +lib/lean/library/init/data/int/basic.olean lib/lean/library/init/data/int/bitwise.lean +lib/lean/library/init/data/int/bitwise.olean lib/lean/library/init/data/int/comp_lemmas.lean +lib/lean/library/init/data/int/comp_lemmas.olean lib/lean/library/init/data/int/default.lean +lib/lean/library/init/data/int/default.olean lib/lean/library/init/data/int/order.lean +lib/lean/library/init/data/int/order.olean lib/lean/library/init/data/list/basic.lean +lib/lean/library/init/data/list/basic.olean lib/lean/library/init/data/list/default.lean +lib/lean/library/init/data/list/default.olean lib/lean/library/init/data/list/instances.lean +lib/lean/library/init/data/list/instances.olean lib/lean/library/init/data/list/lemmas.lean +lib/lean/library/init/data/list/lemmas.olean lib/lean/library/init/data/list/qsort.lean +lib/lean/library/init/data/list/qsort.olean lib/lean/library/init/data/nat/basic.lean +lib/lean/library/init/data/nat/basic.olean lib/lean/library/init/data/nat/bitwise.lean +lib/lean/library/init/data/nat/bitwise.olean lib/lean/library/init/data/nat/default.lean +lib/lean/library/init/data/nat/default.olean lib/lean/library/init/data/nat/div.lean +lib/lean/library/init/data/nat/div.olean lib/lean/library/init/data/nat/gcd.lean +lib/lean/library/init/data/nat/gcd.olean lib/lean/library/init/data/nat/lemmas.lean +lib/lean/library/init/data/nat/lemmas.olean lib/lean/library/init/data/option/basic.lean +lib/lean/library/init/data/option/basic.olean lib/lean/library/init/data/option/instances.lean +lib/lean/library/init/data/option/instances.olean lib/lean/library/init/data/ordering/basic.lean +lib/lean/library/init/data/ordering/basic.olean lib/lean/library/init/data/ordering/default.lean +lib/lean/library/init/data/ordering/default.olean lib/lean/library/init/data/ordering/lemmas.lean +lib/lean/library/init/data/ordering/lemmas.olean lib/lean/library/init/data/prod.lean +lib/lean/library/init/data/prod.olean lib/lean/library/init/data/punit.lean +lib/lean/library/init/data/punit.olean lib/lean/library/init/data/quot.lean +lib/lean/library/init/data/quot.olean lib/lean/library/init/data/repr.lean +lib/lean/library/init/data/repr.olean lib/lean/library/init/data/set.lean +lib/lean/library/init/data/set.olean lib/lean/library/init/data/setoid.lean +lib/lean/library/init/data/setoid.olean lib/lean/library/init/data/sigma/basic.lean +lib/lean/library/init/data/sigma/basic.olean lib/lean/library/init/data/sigma/default.lean +lib/lean/library/init/data/sigma/default.olean lib/lean/library/init/data/sigma/lex.lean +lib/lean/library/init/data/sigma/lex.olean lib/lean/library/init/data/string/basic.lean +lib/lean/library/init/data/string/basic.olean lib/lean/library/init/data/string/default.lean +lib/lean/library/init/data/string/default.olean lib/lean/library/init/data/string/ops.lean +lib/lean/library/init/data/string/ops.olean lib/lean/library/init/data/subtype/basic.lean +lib/lean/library/init/data/subtype/basic.olean lib/lean/library/init/data/subtype/default.lean +lib/lean/library/init/data/subtype/default.olean lib/lean/library/init/data/subtype/instances.lean +lib/lean/library/init/data/subtype/instances.olean lib/lean/library/init/data/sum/basic.lean +lib/lean/library/init/data/sum/basic.olean lib/lean/library/init/data/sum/default.lean +lib/lean/library/init/data/sum/default.olean lib/lean/library/init/data/sum/instances.lean +lib/lean/library/init/data/sum/instances.olean lib/lean/library/init/data/to_string.lean +lib/lean/library/init/data/to_string.olean lib/lean/library/init/data/unsigned/basic.lean +lib/lean/library/init/data/unsigned/basic.olean lib/lean/library/init/data/unsigned/default.lean +lib/lean/library/init/data/unsigned/default.olean lib/lean/library/init/data/unsigned/ops.lean +lib/lean/library/init/data/unsigned/ops.olean lib/lean/library/init/default.lean +lib/lean/library/init/default.olean lib/lean/library/init/function.lean +lib/lean/library/init/function.olean lib/lean/library/init/funext.lean +lib/lean/library/init/funext.olean lib/lean/library/init/init.md lib/lean/library/init/ite_simp.lean +lib/lean/library/init/ite_simp.olean lib/lean/library/init/logic.lean +lib/lean/library/init/logic.olean lib/lean/library/init/meta/ac_tactics.lean +lib/lean/library/init/meta/ac_tactics.olean lib/lean/library/init/meta/async_tactic.lean +lib/lean/library/init/meta/async_tactic.olean lib/lean/library/init/meta/attribute.lean +lib/lean/library/init/meta/attribute.olean lib/lean/library/init/meta/backward.lean +lib/lean/library/init/meta/backward.olean lib/lean/library/init/meta/case_tag.lean +lib/lean/library/init/meta/case_tag.olean lib/lean/library/init/meta/comp_value_tactics.lean +lib/lean/library/init/meta/comp_value_tactics.olean lib/lean/library/init/meta/congr_lemma.lean +lib/lean/library/init/meta/congr_lemma.olean lib/lean/library/init/meta/congr_tactic.lean +lib/lean/library/init/meta/congr_tactic.olean lib/lean/library/init/meta/constructor_tactic.lean +lib/lean/library/init/meta/constructor_tactic.olean lib/lean/library/init/meta/contradiction_tactic.lean +lib/lean/library/init/meta/contradiction_tactic.olean lib/lean/library/init/meta/converter/conv.lean +lib/lean/library/init/meta/converter/conv.olean lib/lean/library/init/meta/converter/default.lean +lib/lean/library/init/meta/converter/default.olean lib/lean/library/init/meta/converter/interactive.lean +lib/lean/library/init/meta/converter/interactive.olean lib/lean/library/init/meta/decl_cmds.lean +lib/lean/library/init/meta/decl_cmds.olean lib/lean/library/init/meta/declaration.lean +lib/lean/library/init/meta/declaration.olean lib/lean/library/init/meta/default.lean +lib/lean/library/init/meta/default.olean lib/lean/library/init/meta/derive.lean +lib/lean/library/init/meta/derive.olean lib/lean/library/init/meta/environment.lean +lib/lean/library/init/meta/environment.olean lib/lean/library/init/meta/exceptional.lean +lib/lean/library/init/meta/exceptional.olean lib/lean/library/init/meta/expr.lean +lib/lean/library/init/meta/expr.olean lib/lean/library/init/meta/expr_address.lean +lib/lean/library/init/meta/expr_address.olean lib/lean/library/init/meta/feature_search.lean +lib/lean/library/init/meta/feature_search.olean lib/lean/library/init/meta/float.lean +lib/lean/library/init/meta/float.olean lib/lean/library/init/meta/format.lean +lib/lean/library/init/meta/format.olean lib/lean/library/init/meta/fun_info.lean +lib/lean/library/init/meta/fun_info.olean lib/lean/library/init/meta/has_reflect.lean +lib/lean/library/init/meta/has_reflect.olean lib/lean/library/init/meta/hole_command.lean +lib/lean/library/init/meta/hole_command.olean lib/lean/library/init/meta/injection_tactic.lean +lib/lean/library/init/meta/injection_tactic.olean lib/lean/library/init/meta/instance_cache.lean +lib/lean/library/init/meta/instance_cache.olean lib/lean/library/init/meta/interaction_monad.lean +lib/lean/library/init/meta/interaction_monad.olean lib/lean/library/init/meta/interactive.lean +lib/lean/library/init/meta/interactive.olean lib/lean/library/init/meta/interactive_base.lean +lib/lean/library/init/meta/interactive_base.olean lib/lean/library/init/meta/json.lean +lib/lean/library/init/meta/json.olean lib/lean/library/init/meta/lean/parser.lean +lib/lean/library/init/meta/lean/parser.olean lib/lean/library/init/meta/level.lean +lib/lean/library/init/meta/level.olean lib/lean/library/init/meta/local_context.lean +lib/lean/library/init/meta/local_context.olean lib/lean/library/init/meta/match_tactic.lean +lib/lean/library/init/meta/match_tactic.olean lib/lean/library/init/meta/mk_dec_eq_instance.lean +lib/lean/library/init/meta/mk_dec_eq_instance.olean lib/lean/library/init/meta/mk_has_reflect_instance.lean +lib/lean/library/init/meta/mk_has_reflect_instance.olean lib/lean/library/init/meta/mk_has_sizeof_instance.lean +lib/lean/library/init/meta/mk_has_sizeof_instance.olean lib/lean/library/init/meta/mk_inhabited_instance.lean +lib/lean/library/init/meta/mk_inhabited_instance.olean lib/lean/library/init/meta/module_info.lean +lib/lean/library/init/meta/module_info.olean lib/lean/library/init/meta/name.lean +lib/lean/library/init/meta/name.olean lib/lean/library/init/meta/occurrences.lean +lib/lean/library/init/meta/occurrences.olean lib/lean/library/init/meta/options.lean +lib/lean/library/init/meta/options.olean lib/lean/library/init/meta/pexpr.lean +lib/lean/library/init/meta/pexpr.olean lib/lean/library/init/meta/rb_map.lean +lib/lean/library/init/meta/rb_map.olean lib/lean/library/init/meta/rec_util.lean +lib/lean/library/init/meta/rec_util.olean lib/lean/library/init/meta/ref.lean +lib/lean/library/init/meta/ref.olean lib/lean/library/init/meta/relation_tactics.lean +lib/lean/library/init/meta/relation_tactics.olean lib/lean/library/init/meta/rewrite_tactic.lean +lib/lean/library/init/meta/rewrite_tactic.olean lib/lean/library/init/meta/set_get_option_tactics.lean +lib/lean/library/init/meta/set_get_option_tactics.olean lib/lean/library/init/meta/simp_tactic.lean +lib/lean/library/init/meta/simp_tactic.olean lib/lean/library/init/meta/smt/congruence_closure.lean +lib/lean/library/init/meta/smt/congruence_closure.olean lib/lean/library/init/meta/smt/default.lean +lib/lean/library/init/meta/smt/default.olean lib/lean/library/init/meta/smt/ematch.lean +lib/lean/library/init/meta/smt/ematch.olean lib/lean/library/init/meta/smt/interactive.lean +lib/lean/library/init/meta/smt/interactive.olean lib/lean/library/init/meta/smt/rsimp.lean +lib/lean/library/init/meta/smt/rsimp.olean lib/lean/library/init/meta/smt/smt_tactic.lean +lib/lean/library/init/meta/smt/smt_tactic.olean lib/lean/library/init/meta/tactic.lean +lib/lean/library/init/meta/tactic.olean lib/lean/library/init/meta/tagged_format.lean +lib/lean/library/init/meta/tagged_format.olean lib/lean/library/init/meta/task.lean +lib/lean/library/init/meta/task.olean lib/lean/library/init/meta/type_context.lean +lib/lean/library/init/meta/type_context.olean lib/lean/library/init/meta/vm.lean +lib/lean/library/init/meta/vm.olean lib/lean/library/init/meta/well_founded_tactics.lean +lib/lean/library/init/meta/well_founded_tactics.olean lib/lean/library/init/meta/widget/basic.lean +lib/lean/library/init/meta/widget/basic.olean lib/lean/library/init/meta/widget/default.lean +lib/lean/library/init/meta/widget/default.olean lib/lean/library/init/meta/widget/html_cmd.lean +lib/lean/library/init/meta/widget/html_cmd.olean lib/lean/library/init/meta/widget/interactive_expr.lean +lib/lean/library/init/meta/widget/interactive_expr.olean lib/lean/library/init/meta/widget/replace_save_info.lean +lib/lean/library/init/meta/widget/replace_save_info.olean lib/lean/library/init/meta/widget/tactic_component.lean +lib/lean/library/init/meta/widget/tactic_component.olean lib/lean/library/init/propext.lean +lib/lean/library/init/propext.olean lib/lean/library/init/util.lean +lib/lean/library/init/util.olean lib/lean/library/init/version.lean +lib/lean/library/init/version.olean lib/lean/library/init/wf.lean +lib/lean/library/init/wf.olean lib/lean/library/library.md lib/lean/library/smt/arith.lean +lib/lean/library/smt/arith.olean lib/lean/library/smt/array.lean +lib/lean/library/smt/array.olean lib/lean/library/smt/default.lean +lib/lean/library/smt/default.olean lib/lean/library/smt/prove.lean +lib/lean/library/smt/prove.olean lib/lean/library/system/io.lean +lib/lean/library/system/io.olean lib/lean/library/system/io_interface.lean +lib/lean/library/system/io_interface.olean lib/lean/library/system/random.lean +lib/lean/library/system/random.olean lib/lean/library/tools/debugger/cli.lean +lib/lean/library/tools/debugger/cli.olean lib/lean/library/tools/debugger/default.lean +lib/lean/library/tools/debugger/default.olean lib/lean/library/tools/debugger/util.lean +lib/lean/library/tools/debugger/util.olean