From nobody Mon Sep 05 17:40:19 2022 X-Original-To: dev-commits-ports-main@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 4MLwlR3plPz4bCRt; Mon, 5 Sep 2022 17:40:19 +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 4MLwlR3TtHz49Cg; Mon, 5 Sep 2022 17:40:19 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1662399619; 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=bBiPj+rKAPOd7DEAYRzQP+pCp49b3ONhNauqg87CDKk=; b=pmCa6xVyAhPEcigQX5mWa9UWIS2jzdjr4wMRSFymvODTC0fA3zp2BDrt/idy+bR6GWeN59 C7O2FEaPL2TG0u7I8arYe5csZceRC6UQ2mmkaAPll8n/ZrXsikKV79xVzulFaLoV5TYFlU Li7Fmr384RPBheIhY0YA0knU9EMHqrfKYZOQtbIr/9l5iQI6jUSXN8U8nF8JSGc6kQkZjL pM9Akybu0+0UI7TDIF5ez6kqAmf6c7h3Sape+USZr4RXL8bxuef2BM2TucZ7kgg3+m6Rw4 SnKqZHbw8NEbb/c2F8lymDhXxF8qrHnSEEKndkMUA4GdQBfmoAtsQcnvUooRSw== 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 4MLwlR2QkKztlQ; Mon, 5 Sep 2022 17:40:19 +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 285HeJrH006892; Mon, 5 Sep 2022 17:40:19 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.16.1/8.16.1/Submit) id 285HeJGE006886; Mon, 5 Sep 2022 17:40:19 GMT (envelope-from git) Date: Mon, 5 Sep 2022 17:40:19 GMT Message-Id: <202209051740.285HeJGE006886@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: 2317424cb609 - main - math/lean: Fix performance problem List-Id: Commits to the main branch of the FreeBSD ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-main List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-dev-commits-ports-main@freebsd.org X-BeenThere: dev-commits-ports-main@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: 2317424cb6092aa0430b738cd19199089dfb3bab Auto-Submitted: auto-generated ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1662399619; 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=bBiPj+rKAPOd7DEAYRzQP+pCp49b3ONhNauqg87CDKk=; b=bFiMusubKzdnEmDq9ZAQBIZAe76AzcgJkHS3eZpMvGiUFDQ5zeCZ1rZEJk+LBf2MHjoLMw SmnNa2uCz2YyBLKzxC6OutieGsGW34HnFXvkblLRPKjBylDfcny9wF/mnrKMMattxU/yvw Benl+SMx6HR9L2d1FR1RfdAq27eGFcJpvbiiDsZ/J5MPPEdCHobaCB+tuuynlKtOI6pAk+ VursrDHKlvbu9yULJvutdm07G3dQ8SStQePS4KEfnf7+AdSNyLCkb3aykY+U6l9ZcUaI17 WUCKsJklKAGeLhycffjjCRym11tLU+gZCcd86xdGQt4kuqYjvTyWMuowX+ffOg== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1662399619; a=rsa-sha256; cv=none; b=td5XVBLRy4tA7zgc7SyopOl5IJpXLwAe7qUe4UivocEnfwNFfSbrydRDnPl57iktMXD0HT MBRfmBkeL7zSNBkSHVmQSWVQmWLGS3s4xGPCuvOqy6HwTMD0eFFtWUa1QbiF/4YhFEyCjW O6Skhz/Luvj/gxhoEpB538hT05TPB9IZka0qGQyYzQMeDinHoaXBeXY5vKsTFRFpVupkzA 2QPlfB58wU/DWosh4UnwrAKFxJP82UC68vJj4MKFs0XcEqRBCXutvRcJclK2Q9RsqIn6au CZ3bhUatduoVe02EzCX73jk5R78u/12ppSw0lM2n2N9JQixHvW7OJZ4mKnPkfA== ARC-Authentication-Results: i=1; mx1.freebsd.org; none X-ThisMailContainsUnwantedMimeParts: N The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=2317424cb6092aa0430b738cd19199089dfb3bab commit 2317424cb6092aa0430b738cd19199089dfb3bab Author: Yuri Victorovich AuthorDate: 2022-09-05 17:37:43 +0000 Commit: Yuri Victorovich CommitDate: 2022-09-05 17:40:17 +0000 math/lean: Fix performance problem Pre-compiled library files weren't installed due to some bug which made lean very slow. --- 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 055dd155831e..cb05da02342b 100644 --- a/math/lean/Makefile +++ b/math/lean/Makefile @@ -1,6 +1,7 @@ PORTNAME= lean DISTVERSIONPREFIX= v DISTVERSION= 3.48.0 +PORTREVISION= 1 CATEGORIES= math PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/ @@ -33,6 +34,9 @@ TCMALLOC_LIB_DEPENDS= libtcmalloc.so:devel/google-perftools THREADS_CMAKE_BOOL= MULTI_THREAD +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