git: 2317424cb609 - main - math/lean: Fix performance problem
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Mon, 05 Sep 2022 17:40:19 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=2317424cb6092aa0430b738cd19199089dfb3bab
commit 2317424cb6092aa0430b738cd19199089dfb3bab
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: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