math/lean: Fix performance problem
Pre-compiled library files weren't installed due to some bug which made lean very slow.
This commit is contained in:
Yuri Victorovich
parent
b8913b6c0c
commit
2317424cb6
@ -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
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user