Date: Wed, 30 Oct 2024 19:55:33 GMT From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: b71b1b7da088 - main - math/lean: Remove Message-ID: <202410301955.49UJtXvr021037@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=b71b1b7da088dd6ec88cc38436d8c6dec8cd336b commit b71b1b7da088dd6ec88cc38436d8c6dec8cd336b Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2024-10-30 19:55:11 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2024-10-30 19:55:11 +0000 math/lean: Remove --- MOVED | 1 + math/Makefile | 1 - math/lean/Makefile | 45 --- math/lean/distinfo | 5 - math/lean/pkg-descr | 6 - math/lean/pkg-message | 22 -- math/lean/pkg-plist | 752 -------------------------------------------------- 7 files changed, 1 insertion(+), 831 deletions(-) diff --git a/MOVED b/MOVED index abcab74d9138..be941ca7d71b 100644 --- a/MOVED +++ b/MOVED @@ -3557,3 +3557,4 @@ security/rubygem-devise_pam_authenticatable2-rails61||2024-10-24|Has expired: Ru security/rubygem-doorkeeper-rails61||2024-10-24|Has expired: Ruby on Rails 6.1.x reaches EOL on 2024-10-01 devel/rubygem-better_html-rails61||2024-10-27|Has expired: Ruby on Rails 6.1.x reaches EOL on 2024-10-01 x11-wm/sway-devel|x11-wm/sway|2024-10-27|Out of date: use x11-wm/sway for now +math/lean|math/lean4|2024-10-30|lean has been superseded by lean4, new generation diff --git a/math/Makefile b/math/Makefile index a29fbc746cd7..04d118dcd1e7 100644 --- a/math/Makefile +++ b/math/Makefile @@ -444,7 +444,6 @@ SUBDIR += latte-integrale SUBDIR += lcalc SUBDIR += ldouble - SUBDIR += lean SUBDIR += lean4 SUBDIR += leangz SUBDIR += lemon diff --git a/math/lean/Makefile b/math/lean/Makefile deleted file mode 100644 index e9dfbd1c0a00..000000000000 --- a/math/lean/Makefile +++ /dev/null @@ -1,45 +0,0 @@ -PORTNAME= lean -DISTVERSIONPREFIX= v -DISTVERSION= 3.51.1 -CATEGORIES= math - -PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/ -PATCHFILES= 5eecaa0b9c860858372a22ab242566671907c913.patch:-p2 - -MAINTAINER= yuri@FreeBSD.org -COMMENT= Theorem prover -WWW= https://leanprover-community.github.io/ - -LICENSE= APACHE20 -LICENSE_FILE= ${WRKSRC}/../LICENSE - -BROKEN_aarch64= c++ crashes during link on arm64 on math/lean, see https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=266777 - -LIB_DEPENDS= libgmp.so:math/gmp - -USES= cmake:testing compiler:c++11-lang - -USE_GITHUB= yes -GH_ACCOUNT= leanprover-community - -WRKSRC_SUBDIR= src - -CMAKE_OFF= BUILD_TESTING -CMAKE_TESTING_ON= BUILD_TESTING - -OPTIONS_DEFINE= TCMALLOC THREADS -OPTIONS_DEFAULT= TCMALLOC THREADS -OPTIONS_EXCLUDE_powerpc= TCMALLOC - -TCMALLOC_CMAKE_BOOL= TCMALLOC -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 - -.include <bsd.port.mk> diff --git a/math/lean/distinfo b/math/lean/distinfo deleted file mode 100644 index af11216dec38..000000000000 --- a/math/lean/distinfo +++ /dev/null @@ -1,5 +0,0 @@ -TIMESTAMP = 1685072378 -SHA256 (leanprover-community-lean-v3.51.1_GH0.tar.gz) = 5a4734bf345d6c5ba6eacd2d33d86d9540eea7d008b4ebf8dde126e729fcbcaf -SIZE (leanprover-community-lean-v3.51.1_GH0.tar.gz) = 1918894 -SHA256 (5eecaa0b9c860858372a22ab242566671907c913.patch) = 971765311b28bfc850803f355e9607dee5aa537565d24ffdc52562b6d874e99a -SIZE (5eecaa0b9c860858372a22ab242566671907c913.patch) = 3218 diff --git a/math/lean/pkg-descr b/math/lean/pkg-descr deleted file mode 100644 index d549a156950f..000000000000 --- a/math/lean/pkg-descr +++ /dev/null @@ -1,6 +0,0 @@ -Lean is an open source theorem prover and programming language being developed -at Microsoft Research. Lean aims to bridge the gap between interactive and -automated theorem proving, by situating automated tools and methods in a -framework that supports user interaction and the construction of fully specified -axiomatic proofs. The mathematical components library mathlib for Lean is being -developed at Carnegie Mellon University. diff --git a/math/lean/pkg-message b/math/lean/pkg-message deleted file mode 100644 index e0c1a26dc720..000000000000 --- a/math/lean/pkg-message +++ /dev/null @@ -1,22 +0,0 @@ -[ -{ type: install - message: <<EOM -================================================================================ -You installed Lean: The Theorem Prover. - -(1) Please note that Lean requires /proc to be mounted. - - The usual way to do this is to add this line to /etc/fstab: - proc /proc procfs rw 0 0 - - and then run this command as root: - # mount /proc - -(2) You might also want to install mathlibtools (math/mathlibtools) in case - you need to use the mathematical library of Lean. - mathlibtools download this library to user's home directory for further - use by Lean. -================================================================================ -EOM -} -] diff --git a/math/lean/pkg-plist b/math/lean/pkg-plist deleted file mode 100644 index ade817a020e2..000000000000 --- a/math/lean/pkg-plist +++ /dev/null @@ -1,752 +0,0 @@ -bin/lean -bin/leanchecker -bin/leanpkg -include/lean_ext/checker/simple_pp.h -include/lean_ext/checker/text_import.h -include/lean_ext/frontends/lean/brackets.h -include/lean_ext/frontends/lean/builtin_cmds.h -include/lean_ext/frontends/lean/builtin_exprs.h -include/lean_ext/frontends/lean/calc.h -include/lean_ext/frontends/lean/cmd_table.h -include/lean_ext/frontends/lean/completion.h -include/lean_ext/frontends/lean/decl_attributes.h -include/lean_ext/frontends/lean/decl_cmds.h -include/lean_ext/frontends/lean/decl_util.h -include/lean_ext/frontends/lean/definition_cmds.h -include/lean_ext/frontends/lean/dependencies.h -include/lean_ext/frontends/lean/elaborator.h -include/lean_ext/frontends/lean/inductive_cmds.h -include/lean_ext/frontends/lean/info_manager.h -include/lean_ext/frontends/lean/init_module.h -include/lean_ext/frontends/lean/interactive.h -include/lean_ext/frontends/lean/json.h -include/lean_ext/frontends/lean/local_context_adapter.h -include/lean_ext/frontends/lean/local_decls.h -include/lean_ext/frontends/lean/local_level_decls.h -include/lean_ext/frontends/lean/match_expr.h -include/lean_ext/frontends/lean/module_parser.h -include/lean_ext/frontends/lean/notation_cmd.h -include/lean_ext/frontends/lean/parse_table.h -include/lean_ext/frontends/lean/parser.h -include/lean_ext/frontends/lean/parser_config.h -include/lean_ext/frontends/lean/parser_pos_provider.h -include/lean_ext/frontends/lean/parser_state.h -include/lean_ext/frontends/lean/pp.h -include/lean_ext/frontends/lean/prenum.h -include/lean_ext/frontends/lean/print_cmd.h -include/lean_ext/frontends/lean/scanner.h -include/lean_ext/frontends/lean/structure_cmd.h -include/lean_ext/frontends/lean/structure_instance.h -include/lean_ext/frontends/lean/tactic_notation.h -include/lean_ext/frontends/lean/token_table.h -include/lean_ext/frontends/lean/tokens.h -include/lean_ext/frontends/lean/type_util.h -include/lean_ext/frontends/lean/user_command.h -include/lean_ext/frontends/lean/user_notation.h -include/lean_ext/frontends/lean/util.h -include/lean_ext/frontends/lean/widget.h -include/lean_ext/init/init.h -include/lean_ext/kernel/abstract.h -include/lean_ext/kernel/abstract_type_context.h -include/lean_ext/kernel/cache_stack.h -include/lean_ext/kernel/declaration.h -include/lean_ext/kernel/environment.h -include/lean_ext/kernel/equiv_manager.h -include/lean_ext/kernel/error_msgs.h -include/lean_ext/kernel/expr.h -include/lean_ext/kernel/expr_cache.h -include/lean_ext/kernel/expr_eq_fn.h -include/lean_ext/kernel/expr_maps.h -include/lean_ext/kernel/expr_pair.h -include/lean_ext/kernel/expr_sets.h -include/lean_ext/kernel/ext_exception.h -include/lean_ext/kernel/find_fn.h -include/lean_ext/kernel/for_each_fn.h -include/lean_ext/kernel/formatter.h -include/lean_ext/kernel/free_vars.h -include/lean_ext/kernel/inductive/inductive.h -include/lean_ext/kernel/init_module.h -include/lean_ext/kernel/instantiate.h -include/lean_ext/kernel/kernel_exception.h -include/lean_ext/kernel/level.h -include/lean_ext/kernel/normalizer_extension.h -include/lean_ext/kernel/pos_info_provider.h -include/lean_ext/kernel/quotient/quotient.h -include/lean_ext/kernel/replace_fn.h -include/lean_ext/kernel/scope_pos_info_provider.h -include/lean_ext/kernel/standard_kernel.h -include/lean_ext/kernel/type_checker.h -include/lean_ext/library/abstract_context_cache.h -include/lean_ext/library/abstract_parser.h -include/lean_ext/library/ac_match.h -include/lean_ext/library/aliases.h -include/lean_ext/library/annotation.h -include/lean_ext/library/app_builder.h -include/lean_ext/library/ast_exporter.h -include/lean_ext/library/attribute_manager.h -include/lean_ext/library/aux_definition.h -include/lean_ext/library/aux_recursors.h -include/lean_ext/library/bin_app.h -include/lean_ext/library/cache_helper.h -include/lean_ext/library/check.h -include/lean_ext/library/choice.h -include/lean_ext/library/class.h -include/lean_ext/library/comp_val.h -include/lean_ext/library/compiler/comp_irrelevant.h -include/lean_ext/library/compiler/compiler_step_visitor.h -include/lean_ext/library/compiler/cse.h -include/lean_ext/library/compiler/elim_recursors.h -include/lean_ext/library/compiler/elim_unused_lets.h -include/lean_ext/library/compiler/erase_irrelevant.h -include/lean_ext/library/compiler/eta_expansion.h -include/lean_ext/library/compiler/extract_values.h -include/lean_ext/library/compiler/init_module.h -include/lean_ext/library/compiler/inliner.h -include/lean_ext/library/compiler/lambda_lifting.h -include/lean_ext/library/compiler/nat_value.h -include/lean_ext/library/compiler/preprocess.h -include/lean_ext/library/compiler/procedure.h -include/lean_ext/library/compiler/rec_fn_macro.h -include/lean_ext/library/compiler/reduce_arity.h -include/lean_ext/library/compiler/simp_inductive.h -include/lean_ext/library/compiler/util.h -include/lean_ext/library/compiler/vm_compiler.h -include/lean_ext/library/congr_lemma.h -include/lean_ext/library/constants.h -include/lean_ext/library/constructions/brec_on.h -include/lean_ext/library/constructions/cases_on.h -include/lean_ext/library/constructions/constructor.h -include/lean_ext/library/constructions/drec.h -include/lean_ext/library/constructions/has_sizeof.h -include/lean_ext/library/constructions/init_module.h -include/lean_ext/library/constructions/injective.h -include/lean_ext/library/constructions/no_confusion.h -include/lean_ext/library/constructions/projection.h -include/lean_ext/library/constructions/rec_on.h -include/lean_ext/library/constructions/util.h -include/lean_ext/library/context_cache.h -include/lean_ext/library/deep_copy.h -include/lean_ext/library/defeq_canonizer.h -include/lean_ext/library/delayed_abstraction.h -include/lean_ext/library/discr_tree.h -include/lean_ext/library/documentation.h -include/lean_ext/library/elab_context.h -include/lean_ext/library/equations_compiler/compiler.h -include/lean_ext/library/equations_compiler/elim_match.h -include/lean_ext/library/equations_compiler/equations.h -include/lean_ext/library/equations_compiler/init_module.h -include/lean_ext/library/equations_compiler/pack_domain.h -include/lean_ext/library/equations_compiler/pack_mutual.h -include/lean_ext/library/equations_compiler/structural_rec.h -include/lean_ext/library/equations_compiler/unbounded_rec.h -include/lean_ext/library/equations_compiler/util.h -include/lean_ext/library/equations_compiler/wf_rec.h -include/lean_ext/library/eval_helper.h -include/lean_ext/library/exception.h -include/lean_ext/library/explicit.h -include/lean_ext/library/export.h -include/lean_ext/library/export_decl.h -include/lean_ext/library/expr_address.h -include/lean_ext/library/expr_lt.h -include/lean_ext/library/expr_pair.h -include/lean_ext/library/expr_pair_maps.h -include/lean_ext/library/expr_unsigned_map.h -include/lean_ext/library/feature_search.h -include/lean_ext/library/fingerprint.h -include/lean_ext/library/fun_info.h -include/lean_ext/library/handle.h -include/lean_ext/library/head_map.h -include/lean_ext/library/idx_metavar.h -include/lean_ext/library/inductive_compiler/add_decl.h -include/lean_ext/library/inductive_compiler/basic.h -include/lean_ext/library/inductive_compiler/compiler.h -include/lean_ext/library/inductive_compiler/ginductive.h -include/lean_ext/library/inductive_compiler/ginductive_decl.h -include/lean_ext/library/inductive_compiler/init_module.h -include/lean_ext/library/inductive_compiler/mutual.h -include/lean_ext/library/inductive_compiler/nested.h -include/lean_ext/library/inductive_compiler/util.h -include/lean_ext/library/init_module.h -include/lean_ext/library/inverse.h -include/lean_ext/library/io_state.h -include/lean_ext/library/io_state_stream.h -include/lean_ext/library/kernel_serializer.h -include/lean_ext/library/library_task_builder.h -include/lean_ext/library/local_context.h -include/lean_ext/library/local_instances.h -include/lean_ext/library/locals.h -include/lean_ext/library/max_sharing.h -include/lean_ext/library/message_builder.h -include/lean_ext/library/messages.h -include/lean_ext/library/metavar_context.h -include/lean_ext/library/metavar_util.h -include/lean_ext/library/module.h -include/lean_ext/library/module_mgr.h -include/lean_ext/library/mt_task_queue.h -include/lean_ext/library/native_compiler/cpp_compiler.h -include/lean_ext/library/noncomputable.h -include/lean_ext/library/normalize.h -include/lean_ext/library/num.h -include/lean_ext/library/parray.h -include/lean_ext/library/pattern_attribute.h -include/lean_ext/library/persistent_context_cache.h -include/lean_ext/library/phash_map.h -include/lean_ext/library/phashtable.h -include/lean_ext/library/pipe.h -include/lean_ext/library/placeholder.h -include/lean_ext/library/pp_options.h -include/lean_ext/library/predict/predict.h -include/lean_ext/library/print.h -include/lean_ext/library/private.h -include/lean_ext/library/process.h -include/lean_ext/library/profiling.h -include/lean_ext/library/projection.h -include/lean_ext/library/protected.h -include/lean_ext/library/quote.h -include/lean_ext/library/reducible.h -include/lean_ext/library/relation_manager.h -include/lean_ext/library/replace_visitor.h -include/lean_ext/library/replace_visitor_with_tc.h -include/lean_ext/library/scoped_ext.h -include/lean_ext/library/shared_environment.h -include/lean_ext/library/sorry.h -include/lean_ext/library/st_task_queue.h -include/lean_ext/library/string.h -include/lean_ext/library/tactic/ac_tactics.h -include/lean_ext/library/tactic/algebraic_normalizer.h -include/lean_ext/library/tactic/app_builder_tactics.h -include/lean_ext/library/tactic/apply_tactic.h -include/lean_ext/library/tactic/assert_tactic.h -include/lean_ext/library/tactic/backward/backward_chaining.h -include/lean_ext/library/tactic/backward/backward_lemmas.h -include/lean_ext/library/tactic/backward/init_module.h -include/lean_ext/library/tactic/cases_tactic.h -include/lean_ext/library/tactic/change_tactic.h -include/lean_ext/library/tactic/clear_tactic.h -include/lean_ext/library/tactic/congr_lemma_tactics.h -include/lean_ext/library/tactic/destruct_tactic.h -include/lean_ext/library/tactic/dsimplify.h -include/lean_ext/library/tactic/elaborate.h -include/lean_ext/library/tactic/elaborator_exception.h -include/lean_ext/library/tactic/eqn_lemmas.h -include/lean_ext/library/tactic/eval.h -include/lean_ext/library/tactic/exact_tactic.h -include/lean_ext/library/tactic/fun_info_tactics.h -include/lean_ext/library/tactic/generalize_tactic.h -include/lean_ext/library/tactic/gexpr.h -include/lean_ext/library/tactic/hole_command.h -include/lean_ext/library/tactic/hsubstitution.h -include/lean_ext/library/tactic/induction_tactic.h -include/lean_ext/library/tactic/init_module.h -include/lean_ext/library/tactic/intro_tactic.h -include/lean_ext/library/tactic/kabstract.h -include/lean_ext/library/tactic/match_tactic.h -include/lean_ext/library/tactic/occurrences.h -include/lean_ext/library/tactic/revert_tactic.h -include/lean_ext/library/tactic/rewrite_tactic.h -include/lean_ext/library/tactic/simp_lemmas.h -include/lean_ext/library/tactic/simp_result.h -include/lean_ext/library/tactic/simp_util.h -include/lean_ext/library/tactic/simplify.h -include/lean_ext/library/tactic/smt/congruence_closure.h -include/lean_ext/library/tactic/smt/congruence_tactics.h -include/lean_ext/library/tactic/smt/ematch.h -include/lean_ext/library/tactic/smt/hinst_lemmas.h -include/lean_ext/library/tactic/smt/init_module.h -include/lean_ext/library/tactic/smt/smt_state.h -include/lean_ext/library/tactic/smt/theory_ac.h -include/lean_ext/library/tactic/smt/util.h -include/lean_ext/library/tactic/subst_tactic.h -include/lean_ext/library/tactic/tactic_evaluator.h -include/lean_ext/library/tactic/tactic_log.h -include/lean_ext/library/tactic/tactic_state.h -include/lean_ext/library/tactic/unfold_tactic.h -include/lean_ext/library/tactic/user_attribute.h -include/lean_ext/library/tactic/vm_local_context.h -include/lean_ext/library/tactic/vm_monitor.h -include/lean_ext/library/tactic/vm_type_context.h -include/lean_ext/library/time_task.h -include/lean_ext/library/tlean_exporter.h -include/lean_ext/library/trace.h -include/lean_ext/library/type_context.h -include/lean_ext/library/typed_expr.h -include/lean_ext/library/unfold_macros.h -include/lean_ext/library/unification_hint.h -include/lean_ext/library/unique_id.h -include/lean_ext/library/update_declaration.h -include/lean_ext/library/user_recursors.h -include/lean_ext/library/util.h -include/lean_ext/library/vm/init_module.h -include/lean_ext/library/vm/interaction_state.h -include/lean_ext/library/vm/interaction_state_imp.h -include/lean_ext/library/vm/optimize.h -include/lean_ext/library/vm/vm.h -include/lean_ext/library/vm/vm_array.h -include/lean_ext/library/vm/vm_aux.h -include/lean_ext/library/vm/vm_declaration.h -include/lean_ext/library/vm/vm_eformat.h -include/lean_ext/library/vm/vm_environment.h -include/lean_ext/library/vm/vm_exceptional.h -include/lean_ext/library/vm/vm_expr.h -include/lean_ext/library/vm/vm_float.h -include/lean_ext/library/vm/vm_format.h -include/lean_ext/library/vm/vm_int.h -include/lean_ext/library/vm/vm_io.h -include/lean_ext/library/vm/vm_json.h -include/lean_ext/library/vm/vm_level.h -include/lean_ext/library/vm/vm_list.h -include/lean_ext/library/vm/vm_module_info.h -include/lean_ext/library/vm/vm_name.h -include/lean_ext/library/vm/vm_nat.h -include/lean_ext/library/vm/vm_option.h -include/lean_ext/library/vm/vm_options.h -include/lean_ext/library/vm/vm_ordering.h -include/lean_ext/library/vm/vm_override.h -include/lean_ext/library/vm/vm_parser.h -include/lean_ext/library/vm/vm_pexpr.h -include/lean_ext/library/vm/vm_pos_info.h -include/lean_ext/library/vm/vm_rb_map.h -include/lean_ext/library/vm/vm_string.h -include/lean_ext/library/vm/vm_task.h -include/lean_ext/shell/emscripten.h -include/lean_ext/shell/lean_js.h -include/lean_ext/shell/server.h -include/lean_ext/shell/simple_pos_info_provider.h -include/lean_ext/util/ascii.h -include/lean_ext/util/bit_tricks.h -include/lean_ext/util/bitap_fuzzy_search.h -include/lean_ext/util/buffer.h -include/lean_ext/util/cancellable.h -include/lean_ext/util/compiler_hints.h -include/lean_ext/util/debug.h -include/lean_ext/util/escaped.h -include/lean_ext/util/exception.h -include/lean_ext/util/exception_with_pos.h -include/lean_ext/util/extensible_object.h -include/lean_ext/util/file_lock.h -include/lean_ext/util/flet.h -include/lean_ext/util/freset.h -include/lean_ext/util/fresh_name.h -include/lean_ext/util/hash.h -include/lean_ext/util/init_module.h -include/lean_ext/util/int64.h -include/lean_ext/util/interrupt.h -include/lean_ext/util/lbool.h -include/lean_ext/util/lean_json.h -include/lean_ext/util/lean_path.h -include/lean_ext/util/line_endings.h -include/lean_ext/util/list.h -include/lean_ext/util/list_fn.h -include/lean_ext/util/log_tree.h -include/lean_ext/util/lru_cache.h -include/lean_ext/util/macros.h -include/lean_ext/util/map.h -include/lean_ext/util/memory.h -include/lean_ext/util/memory_pool.h -include/lean_ext/util/message_definitions.h -include/lean_ext/util/name.h -include/lean_ext/util/name_generator.h -include/lean_ext/util/name_hash_map.h -include/lean_ext/util/name_hash_set.h -include/lean_ext/util/name_map.h -include/lean_ext/util/name_set.h -include/lean_ext/util/null_ostream.h -include/lean_ext/util/numerics/mpq.h -include/lean_ext/util/numerics/mpz.h -include/lean_ext/util/object_serializer.h -include/lean_ext/util/optional.h -include/lean_ext/util/output_channel.h -include/lean_ext/util/pair.h -include/lean_ext/util/parser_exception.h -include/lean_ext/util/path.h -include/lean_ext/util/priority_queue.h -include/lean_ext/util/rb_map.h -include/lean_ext/util/rb_multi_map.h -include/lean_ext/util/rb_tree.h -include/lean_ext/util/rc.h -include/lean_ext/util/safe_arith.h -include/lean_ext/util/scoped_map.h -include/lean_ext/util/scoped_set.h -include/lean_ext/util/sequence.h -include/lean_ext/util/serializer.h -include/lean_ext/util/sexpr/format.h -include/lean_ext/util/sexpr/init_module.h -include/lean_ext/util/sexpr/option_declarations.h -include/lean_ext/util/sexpr/options.h -include/lean_ext/util/sexpr/sexpr.h -include/lean_ext/util/sexpr/sexpr_fn.h -include/lean_ext/util/shared_mutex.h -include/lean_ext/util/small_object_allocator.h -include/lean_ext/util/sstream.h -include/lean_ext/util/stackinfo.h -include/lean_ext/util/subscripted_name_set.h -include/lean_ext/util/task.h -include/lean_ext/util/task_builder.h -include/lean_ext/util/test.h -include/lean_ext/util/thread.h -include/lean_ext/util/timeit.h -include/lean_ext/util/timer.h -include/lean_ext/util/trie.h -include/lean_ext/util/unit.h -include/lean_ext/util/unlock_guard.h -include/lean_ext/util/utf8.h -include/lean_ext/util/worker_queue.h -lib/lean/leanpkg/README.md -lib/lean/leanpkg/leanpkg.toml -lib/lean/leanpkg/leanpkg/git.lean -lib/lean/leanpkg/leanpkg/lean_version.lean -lib/lean/leanpkg/leanpkg/main.lean -lib/lean/leanpkg/leanpkg/manifest.lean -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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202410301955.49UJtXvr021037>