diff --git a/math/lean/Makefile b/math/lean/Makefile index 53a97b8fd6e5..101bfada5d21 100644 --- a/math/lean/Makefile +++ b/math/lean/Makefile @@ -1,31 +1,35 @@ PORTNAME= lean DISTVERSIONPREFIX= v -DISTVERSION= 3.33.0 +DISTVERSION= 3.35.0 CATEGORIES= math +PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/ +PATCHFILES= aba9d05dd1c725ec0a681aaec4a391554325a51b.patch:-p2 # FreeBSD patches: https://github.com/leanprover-community/lean/pull/643 + MAINTAINER= yuri@FreeBSD.org COMMENT= Theorem prover LICENSE= APACHE20 LICENSE_FILE= ${WRKSRC}/../LICENSE LIB_DEPENDS= libgmp.so:math/gmp USES= cmake compiler:c++11-lang + USE_GITHUB= yes GH_ACCOUNT= leanprover-community WRKSRC_SUBDIR= src CMAKE_OFF= BUILD_TESTING post-install: @${FIND} ${STAGEDIR}${PREFIX} -type d -empty -delete do-test: @cd ${BUILD_WRKSRC} && \ ${SETENV} ${CONFIGURE_ENV} ${CMAKE_BIN} ${CMAKE_ARGS} -DBUILD_TESTING:BOOL=ON ${CMAKE_SOURCE_PATH} && \ ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} ${ALL_TARGET} && \ ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS} test .include diff --git a/math/lean/distinfo b/math/lean/distinfo index a15f89a7fb6e..63d0e9a472d5 100644 --- a/math/lean/distinfo +++ b/math/lean/distinfo @@ -1,3 +1,5 @@ -TIMESTAMP = 1631983261 -SHA256 (leanprover-community-lean-v3.33.0_GH0.tar.gz) = bb9b4cc1a6516726433f51d181c5089ba1eb20c2e08dc7c48c9bd862008d4003 -SIZE (leanprover-community-lean-v3.33.0_GH0.tar.gz) = 1890511 +TIMESTAMP = 1635697714 +SHA256 (leanprover-community-lean-v3.35.0_GH0.tar.gz) = 91d324089cdecff72de6a023605caece2732ed6d25f290b43aced95eef7b1a42 +SIZE (leanprover-community-lean-v3.35.0_GH0.tar.gz) = 1872221 +SHA256 (aba9d05dd1c725ec0a681aaec4a391554325a51b.patch) = 8595820a0dd31f62ebc26d5b98c5b8d3499db0b4c12d405229ba914f36bbad8f +SIZE (aba9d05dd1c725ec0a681aaec4a391554325a51b.patch) = 2477 diff --git a/math/lean/files/patch-CMakeLists.txt b/math/lean/files/patch-CMakeLists.txt deleted file mode 100644 index 1796f7cbca64..000000000000 --- a/math/lean/files/patch-CMakeLists.txt +++ /dev/null @@ -1,44 +0,0 @@ ---- CMakeLists.txt.orig 2020-07-08 16:29:47 UTC -+++ CMakeLists.txt -@@ -179,7 +179,7 @@ endif() - - if(STATIC) - message(STATUS "Creating a static executable") -- if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux") -+ if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly") - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--whole-archive -lpthread -lrt -Wl,--no-whole-archive") - endif() - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static") -@@ -212,7 +212,7 @@ endif() - - # SPLIT_STACK - if (SPLIT_STACK) -- if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) -+ if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fsplit-stack -D LEAN_USE_SPLIT_STACK") - message(STATUS "Using split-stacks") - else() -@@ -299,13 +299,7 @@ else() - endif() - - # DL --if (EMSCRIPTEN) -- # no dlopen --elseif((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) -- # TODO(Jared): config dlopen windows support --else() -- set(EXTRA_LIBS ${EXTRA_LIBS} dl) --endif() -+set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS}) - - # TRACK_MEMORY_USAGE - if(TRACK_MEMORY_USAGE) -@@ -568,7 +562,7 @@ if(NOT (${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")) - set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION}.git${GIT_SHA1}") - endif() - set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}") --if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") -+if(${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly") - SET(CPACK_GENERATOR TGZ) - else() - SET(CPACK_GENERATOR ZIP) diff --git a/math/lean/files/patch-util_path.cpp b/math/lean/files/patch-util_path.cpp deleted file mode 100644 index 2ea9fd1d73cb..000000000000 --- a/math/lean/files/patch-util_path.cpp +++ /dev/null @@ -1,14 +0,0 @@ ---- util/path.cpp.orig 2018-07-22 05:22:25 UTC -+++ util/path.cpp -@@ -82,7 +82,11 @@ std::string get_exe_location() { - char dest[PATH_MAX]; - memset(dest, 0, PATH_MAX); - pid_t pid = getpid(); -+#if defined(__FreeBSD__) -+ snprintf(path, PATH_MAX, "/proc/%d/file", pid); -+#else - snprintf(path, PATH_MAX, "/proc/%d/exe", pid); -+#endif - if (readlink(path, dest, PATH_MAX) == -1) { - throw exception("failed to locate Lean executable location"); - } else { diff --git a/math/lean/pkg-plist b/math/lean/pkg-plist index e57ddc87fa83..855276ded98d 100644 --- a/math/lean/pkg-plist +++ b/math/lean/pkg-plist @@ -1,586 +1,574 @@ 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/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/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/parser.lean lib/lean/library/data/dlist.lean -lib/lean/library/data/rbmap/default.lean -lib/lean/library/data/rbtree/basic.lean -lib/lean/library/data/rbtree/default.lean -lib/lean/library/data/rbtree/find.lean -lib/lean/library/data/rbtree/insert.lean -lib/lean/library/data/rbtree/main.lean -lib/lean/library/data/rbtree/min_max.lean -lib/lean/library/data/stream.lean lib/lean/library/data/vector.lean lib/lean/library/init/algebra/classes.lean lib/lean/library/init/algebra/default.lean lib/lean/library/init/algebra/functions.lean lib/lean/library/init/algebra/order.lean lib/lean/library/init/cc_lemmas.lean lib/lean/library/init/classical.lean lib/lean/library/init/coe.lean lib/lean/library/init/control/alternative.lean lib/lean/library/init/control/applicative.lean lib/lean/library/init/control/combinators.lean lib/lean/library/init/control/default.lean lib/lean/library/init/control/except.lean lib/lean/library/init/control/functor.lean lib/lean/library/init/control/id.lean lib/lean/library/init/control/lawful.lean lib/lean/library/init/control/lift.lean lib/lean/library/init/control/monad.lean lib/lean/library/init/control/monad_fail.lean lib/lean/library/init/control/option.lean lib/lean/library/init/control/reader.lean lib/lean/library/init/control/state.lean lib/lean/library/init/core.lean lib/lean/library/init/data/array/basic.lean lib/lean/library/init/data/array/default.lean lib/lean/library/init/data/array/slice.lean lib/lean/library/init/data/basic.lean lib/lean/library/init/data/bool/basic.lean lib/lean/library/init/data/bool/default.lean lib/lean/library/init/data/bool/lemmas.lean lib/lean/library/init/data/char/basic.lean lib/lean/library/init/data/char/classes.lean lib/lean/library/init/data/char/default.lean lib/lean/library/init/data/char/lemmas.lean lib/lean/library/init/data/default.lean lib/lean/library/init/data/fin/basic.lean lib/lean/library/init/data/fin/default.lean lib/lean/library/init/data/fin/ops.lean lib/lean/library/init/data/int/basic.lean lib/lean/library/init/data/int/bitwise.lean lib/lean/library/init/data/int/comp_lemmas.lean lib/lean/library/init/data/int/default.lean lib/lean/library/init/data/int/order.lean lib/lean/library/init/data/list/basic.lean lib/lean/library/init/data/list/default.lean lib/lean/library/init/data/list/instances.lean lib/lean/library/init/data/list/lemmas.lean lib/lean/library/init/data/list/qsort.lean lib/lean/library/init/data/nat/basic.lean lib/lean/library/init/data/nat/bitwise.lean lib/lean/library/init/data/nat/default.lean lib/lean/library/init/data/nat/div.lean lib/lean/library/init/data/nat/gcd.lean lib/lean/library/init/data/nat/lemmas.lean lib/lean/library/init/data/option/basic.lean lib/lean/library/init/data/option/instances.lean lib/lean/library/init/data/ordering/basic.lean lib/lean/library/init/data/ordering/default.lean lib/lean/library/init/data/ordering/lemmas.lean lib/lean/library/init/data/prod.lean lib/lean/library/init/data/punit.lean lib/lean/library/init/data/quot.lean -lib/lean/library/init/data/rbmap/basic.lean -lib/lean/library/init/data/rbmap/default.lean -lib/lean/library/init/data/rbtree/basic.lean -lib/lean/library/init/data/rbtree/default.lean lib/lean/library/init/data/repr.lean lib/lean/library/init/data/set.lean lib/lean/library/init/data/setoid.lean lib/lean/library/init/data/sigma/basic.lean lib/lean/library/init/data/sigma/default.lean lib/lean/library/init/data/sigma/lex.lean lib/lean/library/init/data/string/basic.lean lib/lean/library/init/data/string/default.lean lib/lean/library/init/data/string/ops.lean lib/lean/library/init/data/subtype/basic.lean lib/lean/library/init/data/subtype/default.lean lib/lean/library/init/data/subtype/instances.lean lib/lean/library/init/data/sum/basic.lean lib/lean/library/init/data/sum/default.lean lib/lean/library/init/data/sum/instances.lean lib/lean/library/init/data/to_string.lean lib/lean/library/init/data/unsigned/basic.lean lib/lean/library/init/data/unsigned/default.lean lib/lean/library/init/data/unsigned/ops.lean lib/lean/library/init/default.lean lib/lean/library/init/function.lean lib/lean/library/init/funext.lean lib/lean/library/init/init.md lib/lean/library/init/ite_simp.lean lib/lean/library/init/logic.lean lib/lean/library/init/meta/ac_tactics.lean lib/lean/library/init/meta/async_tactic.lean lib/lean/library/init/meta/attribute.lean lib/lean/library/init/meta/backward.lean lib/lean/library/init/meta/case_tag.lean lib/lean/library/init/meta/comp_value_tactics.lean lib/lean/library/init/meta/congr_lemma.lean lib/lean/library/init/meta/congr_tactic.lean lib/lean/library/init/meta/constructor_tactic.lean lib/lean/library/init/meta/contradiction_tactic.lean lib/lean/library/init/meta/converter/conv.lean lib/lean/library/init/meta/converter/default.lean lib/lean/library/init/meta/converter/interactive.lean lib/lean/library/init/meta/decl_cmds.lean lib/lean/library/init/meta/declaration.lean lib/lean/library/init/meta/default.lean lib/lean/library/init/meta/derive.lean lib/lean/library/init/meta/environment.lean lib/lean/library/init/meta/exceptional.lean lib/lean/library/init/meta/expr.lean lib/lean/library/init/meta/expr_address.lean lib/lean/library/init/meta/float.lean lib/lean/library/init/meta/format.lean lib/lean/library/init/meta/fun_info.lean lib/lean/library/init/meta/has_reflect.lean lib/lean/library/init/meta/hole_command.lean lib/lean/library/init/meta/injection_tactic.lean lib/lean/library/init/meta/interaction_monad.lean lib/lean/library/init/meta/interactive.lean lib/lean/library/init/meta/interactive_base.lean lib/lean/library/init/meta/json.lean lib/lean/library/init/meta/lean/parser.lean lib/lean/library/init/meta/level.lean lib/lean/library/init/meta/local_context.lean lib/lean/library/init/meta/match_tactic.lean lib/lean/library/init/meta/mk_dec_eq_instance.lean lib/lean/library/init/meta/mk_has_reflect_instance.lean lib/lean/library/init/meta/mk_has_sizeof_instance.lean lib/lean/library/init/meta/mk_inhabited_instance.lean lib/lean/library/init/meta/module_info.lean lib/lean/library/init/meta/name.lean lib/lean/library/init/meta/occurrences.lean lib/lean/library/init/meta/options.lean lib/lean/library/init/meta/pexpr.lean lib/lean/library/init/meta/rb_map.lean lib/lean/library/init/meta/rec_util.lean lib/lean/library/init/meta/ref.lean lib/lean/library/init/meta/relation_tactics.lean lib/lean/library/init/meta/rewrite_tactic.lean lib/lean/library/init/meta/set_get_option_tactics.lean lib/lean/library/init/meta/simp_tactic.lean lib/lean/library/init/meta/smt/congruence_closure.lean lib/lean/library/init/meta/smt/default.lean lib/lean/library/init/meta/smt/ematch.lean lib/lean/library/init/meta/smt/interactive.lean lib/lean/library/init/meta/smt/rsimp.lean lib/lean/library/init/meta/smt/smt_tactic.lean lib/lean/library/init/meta/tactic.lean lib/lean/library/init/meta/tagged_format.lean lib/lean/library/init/meta/task.lean lib/lean/library/init/meta/type_context.lean lib/lean/library/init/meta/vm.lean lib/lean/library/init/meta/well_founded_tactics.lean lib/lean/library/init/meta/widget/basic.lean lib/lean/library/init/meta/widget/default.lean lib/lean/library/init/meta/widget/html_cmd.lean lib/lean/library/init/meta/widget/interactive_expr.lean lib/lean/library/init/meta/widget/replace_save_info.lean lib/lean/library/init/meta/widget/tactic_component.lean lib/lean/library/init/propext.lean lib/lean/library/init/util.lean lib/lean/library/init/version.lean lib/lean/library/init/wf.lean lib/lean/library/library.md lib/lean/library/smt/arith.lean lib/lean/library/smt/array.lean lib/lean/library/smt/default.lean lib/lean/library/smt/prove.lean lib/lean/library/system/io.lean lib/lean/library/system/io_interface.lean lib/lean/library/system/random.lean lib/lean/library/tools/debugger/cli.lean lib/lean/library/tools/debugger/default.lean lib/lean/library/tools/debugger/util.lean