Date: Tue, 21 Jul 2020 22:40:26 +0000 (UTC) From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r542813 - in head/math/lean: . files Message-ID: <202007212240.06LMeQ16025153@repo.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: yuri Date: Tue Jul 21 22:40:25 2020 New Revision: 542813 URL: https://svnweb.freebsd.org/changeset/ports/542813 Log: math/lean: Update 3.4.2 -> 3.17.1 The original Microsoft's account 'leanprover' is now archived, and the community account 'leanprover-community' carries the project on. Also: * remove tests from build * add 'test' target Modified: head/math/lean/Makefile head/math/lean/distinfo head/math/lean/files/patch-CMakeLists.txt head/math/lean/pkg-descr head/math/lean/pkg-plist Modified: head/math/lean/Makefile ============================================================================== --- head/math/lean/Makefile Tue Jul 21 22:10:19 2020 (r542812) +++ head/math/lean/Makefile Tue Jul 21 22:40:25 2020 (r542813) @@ -2,8 +2,7 @@ PORTNAME= lean DISTVERSIONPREFIX= v -DISTVERSION= 3.4.2 -PORTREVISION= 1 +DISTVERSION= 3.17.1 CATEGORIES= math PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX} @@ -17,11 +16,20 @@ LIB_DEPENDS= libgmp.so:math/gmp USES= cmake compiler:c++11-lang USE_GITHUB= yes -GH_ACCOUNT= leanprover +GH_ACCOUNT= leanprover-community USE_LDCONFIG= yes WRKSRC_SUBDIR= src -PORTSCOUT= limit:.*[0-9]+\.[0-9]+$$ +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 <bsd.port.mk> Modified: head/math/lean/distinfo ============================================================================== --- head/math/lean/distinfo Tue Jul 21 22:10:19 2020 (r542812) +++ head/math/lean/distinfo Tue Jul 21 22:40:25 2020 (r542813) @@ -1,3 +1,3 @@ -TIMESTAMP = 1548236438 -SHA256 (leanprover-lean-v3.4.2_GH0.tar.gz) = ec4488be8473577666f38dec81123d0f7b26476139d3caa2e175a571f6c00d87 -SIZE (leanprover-lean-v3.4.2_GH0.tar.gz) = 1807616 +TIMESTAMP = 1595369167 +SHA256 (leanprover-community-lean-v3.17.1_GH0.tar.gz) = 6df0bfd67986546d751fd91513f9fd2fdf5d4f075ceec31f8c4cc23e5956b8a9 +SIZE (leanprover-community-lean-v3.17.1_GH0.tar.gz) = 1843488 Modified: head/math/lean/files/patch-CMakeLists.txt ============================================================================== --- head/math/lean/files/patch-CMakeLists.txt Tue Jul 21 22:10:19 2020 (r542812) +++ head/math/lean/files/patch-CMakeLists.txt Tue Jul 21 22:40:25 2020 (r542813) @@ -1,16 +1,25 @@ ---- CMakeLists.txt.orig 2018-06-21 16:27:49 UTC +--- CMakeLists.txt.orig 2020-07-08 16:29:47 UTC +++ CMakeLists.txt -@@ -215,7 +215,7 @@ if (NOT DEFINED CMAKE_MACOSX_RPATH) - set(CMAKE_MACOSX_RPATH 0) - endif() +@@ -179,7 +179,7 @@ endif() --if (${CMAKE_SYSTEM_NAME} MATCHES "Linux") -+if (${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly") - # The following options is needed to generate a shared library - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC") + 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() -@@ -304,13 +304,7 @@ else() - endif() # DL -if (EMSCRIPTEN) @@ -24,3 +33,12 @@ # 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) Modified: head/math/lean/pkg-descr ============================================================================== --- head/math/lean/pkg-descr Tue Jul 21 22:10:19 2020 (r542812) +++ head/math/lean/pkg-descr Tue Jul 21 22:40:25 2020 (r542813) @@ -5,4 +5,4 @@ framework that supports user interaction and the const axiomatic proofs. The mathematical components library mathlib for Lean is being developed at Carnegie Mellon University. -WWW: https://leanprover.github.io/ +WWW: https://leanprover-community.github.io/ Modified: head/math/lean/pkg-plist ============================================================================== --- head/math/lean/pkg-plist Tue Jul 21 22:10:19 2020 (r542812) +++ head/math/lean/pkg-plist Tue Jul 21 22:40:25 2020 (r542813) @@ -1,38 +1,6 @@ bin/lean bin/leanchecker bin/leanpkg -include/lean.h -include/lean_bool.h -include/lean_decl.h -include/lean_env.h -include/lean_exception.h -include/lean_expr.h -include/lean_ext/api/decl.h -include/lean_ext/api/exception.h -include/lean_ext/api/expr.h -include/lean_ext/api/inductive.h -include/lean_ext/api/ios.h -include/lean_ext/api/lean.h -include/lean_ext/api/lean_bool.h -include/lean_ext/api/lean_decl.h -include/lean_ext/api/lean_env.h -include/lean_ext/api/lean_exception.h -include/lean_ext/api/lean_expr.h -include/lean_ext/api/lean_inductive.h -include/lean_ext/api/lean_ios.h -include/lean_ext/api/lean_macros.h -include/lean_ext/api/lean_module.h -include/lean_ext/api/lean_name.h -include/lean_ext/api/lean_options.h -include/lean_ext/api/lean_parser.h -include/lean_ext/api/lean_string.h -include/lean_ext/api/lean_type_checker.h -include/lean_ext/api/lean_univ.h -include/lean_ext/api/name.h -include/lean_ext/api/options.h -include/lean_ext/api/string.h -include/lean_ext/api/type_checker.h -include/lean_ext/api/univ.h include/lean_ext/checker/simple_pp.h include/lean_ext/checker/text_import.h include/lean_ext/frontends/lean/brackets.h @@ -76,6 +44,7 @@ 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 @@ -113,7 +82,6 @@ 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/arith_instance.h include/lean_ext/library/attribute_manager.h include/lean_ext/library/aux_definition.h include/lean_ext/library/aux_recursors.h @@ -177,6 +145,7 @@ 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 @@ -214,7 +183,6 @@ 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/norm_num.h include/lean_ext/library/normalize.h include/lean_ext/library/num.h include/lean_ext/library/parray.h @@ -233,7 +201,6 @@ 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/register_module.h include/lean_ext/library/relation_manager.h include/lean_ext/library/replace_visitor.h include/lean_ext/library/replace_visitor_with_tc.h @@ -271,7 +238,6 @@ 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/norm_num_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 @@ -292,7 +258,9 @@ include/lean_ext/library/tactic/tactic_evaluator.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/trace.h include/lean_ext/library/type_context.h @@ -311,30 +279,34 @@ 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_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/leandoc.h include/lean_ext/shell/server.h include/lean_ext/shell/simple_pos_info_provider.h -include/lean_ext/tests/util/interval/check.h include/lean_ext/util/ascii.h include/lean_ext/util/bit_tricks.h include/lean_ext/util/bitap_fuzzy_search.h @@ -356,6 +328,7 @@ include/lean_ext/util/int64.h include/lean_ext/util/interrupt.h include/lean_ext/util/lbool.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 @@ -372,27 +345,14 @@ 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/double.h -include/lean_ext/util/numerics/float.h -include/lean_ext/util/numerics/gcd.h -include/lean_ext/util/numerics/init_module.h -include/lean_ext/util/numerics/mpbq.h include/lean_ext/util/numerics/mpq.h include/lean_ext/util/numerics/mpz.h -include/lean_ext/util/numerics/numeric_traits.h -include/lean_ext/util/numerics/power.h -include/lean_ext/util/numerics/primes.h -include/lean_ext/util/numerics/register_module.h -include/lean_ext/util/numerics/remainder.h -include/lean_ext/util/numerics/xnumeral.h -include/lean_ext/util/numerics/zpz.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/polynomial/polynomial.h include/lean_ext/util/priority_queue.h include/lean_ext/util/rb_map.h include/lean_ext/util/rb_multi_map.h @@ -407,7 +367,6 @@ 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/register_module.h include/lean_ext/util/sexpr/sexpr.h include/lean_ext/util/sexpr/sexpr_fn.h include/lean_ext/util/shared_mutex.h @@ -426,401 +385,199 @@ 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 -include/lean_inductive.h -include/lean_ios.h -include/lean_macros.h -include/lean_module.h -include/lean_name.h -include/lean_options.h -include/lean_parser.h -include/lean_string.h -include/lean_type_checker.h -include/lean_univ.h lib/lean/leanpkg/README.md lib/lean/leanpkg/leanpkg.toml lib/lean/leanpkg/leanpkg/git.lean -lib/lean/leanpkg/leanpkg/git.olean lib/lean/leanpkg/leanpkg/lean_version.lean -lib/lean/leanpkg/leanpkg/lean_version.olean lib/lean/leanpkg/leanpkg/main.lean -lib/lean/leanpkg/leanpkg/main.olean lib/lean/leanpkg/leanpkg/manifest.lean -lib/lean/leanpkg/leanpkg/manifest.olean lib/lean/leanpkg/leanpkg/proc.lean -lib/lean/leanpkg/leanpkg/proc.olean lib/lean/leanpkg/leanpkg/resolve.lean -lib/lean/leanpkg/leanpkg/resolve.olean lib/lean/leanpkg/leanpkg/toml.lean -lib/lean/leanpkg/leanpkg/toml.olean lib/lean/library/data/bitvec.lean -lib/lean/library/data/bitvec.olean 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/lazy_list.lean -lib/lean/library/data/lazy_list.olean lib/lean/library/data/rbmap/default.lean -lib/lean/library/data/rbmap/default.olean lib/lean/library/data/rbtree/basic.lean -lib/lean/library/data/rbtree/basic.olean lib/lean/library/data/rbtree/default.lean -lib/lean/library/data/rbtree/default.olean lib/lean/library/data/rbtree/find.lean -lib/lean/library/data/rbtree/find.olean lib/lean/library/data/rbtree/insert.lean -lib/lean/library/data/rbtree/insert.olean lib/lean/library/data/rbtree/main.lean -lib/lean/library/data/rbtree/main.olean lib/lean/library/data/rbtree/min_max.lean -lib/lean/library/data/rbtree/min_max.olean lib/lean/library/data/stream.lean -lib/lean/library/data/stream.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/field.lean -lib/lean/library/init/algebra/field.olean lib/lean/library/init/algebra/functions.lean -lib/lean/library/init/algebra/functions.olean -lib/lean/library/init/algebra/group.lean -lib/lean/library/init/algebra/group.olean -lib/lean/library/init/algebra/norm_num.lean -lib/lean/library/init/algebra/norm_num.olean lib/lean/library/init/algebra/order.lean -lib/lean/library/init/algebra/order.olean -lib/lean/library/init/algebra/ordered_field.lean -lib/lean/library/init/algebra/ordered_field.olean -lib/lean/library/init/algebra/ordered_group.lean -lib/lean/library/init/algebra/ordered_group.olean -lib/lean/library/init/algebra/ordered_ring.lean -lib/lean/library/init/algebra/ordered_ring.olean -lib/lean/library/init/algebra/ring.lean -lib/lean/library/init/algebra/ring.olean -lib/lean/library/init/category/alternative.lean -lib/lean/library/init/category/alternative.olean -lib/lean/library/init/category/applicative.lean -lib/lean/library/init/category/applicative.olean -lib/lean/library/init/category/combinators.lean -lib/lean/library/init/category/combinators.olean -lib/lean/library/init/category/default.lean -lib/lean/library/init/category/default.olean -lib/lean/library/init/category/except.lean -lib/lean/library/init/category/except.olean -lib/lean/library/init/category/functor.lean -lib/lean/library/init/category/functor.olean -lib/lean/library/init/category/id.lean -lib/lean/library/init/category/id.olean -lib/lean/library/init/category/lawful.lean -lib/lean/library/init/category/lawful.olean -lib/lean/library/init/category/lift.lean -lib/lean/library/init/category/lift.olean -lib/lean/library/init/category/monad.lean -lib/lean/library/init/category/monad.olean -lib/lean/library/init/category/monad_fail.lean -lib/lean/library/init/category/monad_fail.olean -lib/lean/library/init/category/option.lean -lib/lean/library/init/category/option.olean -lib/lean/library/init/category/reader.lean -lib/lean/library/init/category/reader.olean -lib/lean/library/init/category/state.lean -lib/lean/library/init/category/state.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/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/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/rbmap/basic.lean -lib/lean/library/init/data/rbmap/basic.olean lib/lean/library/init/data/rbmap/default.lean -lib/lean/library/init/data/rbmap/default.olean lib/lean/library/init/data/rbtree/basic.lean -lib/lean/library/init/data/rbtree/basic.olean lib/lean/library/init/data/rbtree/default.lean -lib/lean/library/init/data/rbtree/default.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/instances.lean -lib/lean/library/init/data/string/instances.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/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/float.lean 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/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/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/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/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/task.lean -lib/lean/library/init/meta/task.olean +lib/lean/library/init/meta/type_context.lean 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/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/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 -lib/libleanshared.so -lib/libleanstatic.a -@dir include/lean_ext/cmake/Modules -@dir include/lean_ext/shared -@dir include/lean_ext/tests/frontends/lean -@dir include/lean_ext/tests/kernel -@dir include/lean_ext/tests/library/rewriter -@dir include/lean_ext/tests/shared -@dir include/lean_ext/tests/shell -@dir include/lean_ext/tests/util/numerics
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202007212240.06LMeQ16025153>