git: 56e03a4e58bc - 2022Q3 - math/lean: Fix performance problem

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Mon, 05 Sep 2022 17:52:22 UTC
The branch 2022Q3 has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=56e03a4e58bc9d9380a8e0cd94274bfcde1a89c3

commit 56e03a4e58bc9d9380a8e0cd94274bfcde1a89c3
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2022-09-05 17:37:43 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
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