svn commit: r475085 - in head/math: . lean lean/files
Yuri Victorovich
yuri at FreeBSD.org
Sun Jul 22 05:58:42 UTC 2018
Author: yuri
Date: Sun Jul 22 05:58:39 2018
New Revision: 475085
URL: https://svnweb.freebsd.org/changeset/ports/475085
Log:
New port: math/lean: Theorem prover
Added:
head/math/lean/
head/math/lean/Makefile (contents, props changed)
head/math/lean/distinfo (contents, props changed)
head/math/lean/files/
head/math/lean/files/patch-CMakeLists.txt (contents, props changed)
head/math/lean/files/patch-util_path.cpp (contents, props changed)
head/math/lean/pkg-descr (contents, props changed)
head/math/lean/pkg-plist (contents, props changed)
Modified:
head/math/Makefile
Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile Sun Jul 22 04:16:38 2018 (r475084)
+++ head/math/Makefile Sun Jul 22 05:58:39 2018 (r475085)
@@ -298,6 +298,7 @@
SUBDIR += lapacke
SUBDIR += laspack
SUBDIR += ldouble
+ SUBDIR += lean
SUBDIR += levmar
SUBDIR += libRmath
SUBDIR += libflame
Added: head/math/lean/Makefile
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/Makefile Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,25 @@
+# $FreeBSD$
+
+PORTNAME= lean
+DISTVERSIONPREFIX= v
+DISTVERSION= 3.2.0-1147
+DISTVERSIONSUFFIX= -gceacfa744
+CATEGORIES= math
+PKGNAMEPREFIX= ${PYTHON_PKGNAMEPREFIX}
+
+MAINTAINER= yuri at FreeBSD.org
+COMMENT= Theorem prover
+
+LICENSE= APACHE20
+LICENSE_FILE= ${WRKSRC}/../LICENSE
+
+LIB_DEPENDS= libgmp.so:math/gmp
+
+USES= cmake:outsource
+USE_GITHUB= yes
+GH_ACCOUNT= leodemoura
+USE_LDCONFIG= yes
+
+WRKSRC_SUBDIR= src
+
+.include <bsd.port.mk>
Added: head/math/lean/distinfo
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/distinfo Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1532233323
+SHA256 (leodemoura-lean-v3.2.0-1147-gceacfa744_GH0.tar.gz) = cbb1fceae4b1876e135f20ec3d1c91816ffec6e84613ba4fa37fa39c96f61c86
+SIZE (leodemoura-lean-v3.2.0-1147-gceacfa744_GH0.tar.gz) = 1817180
Added: head/math/lean/files/patch-CMakeLists.txt
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/files/patch-CMakeLists.txt Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,26 @@
+--- CMakeLists.txt.orig 2018-06-21 16:27:49 UTC
++++ CMakeLists.txt
+@@ -215,7 +215,7 @@ if (NOT DEFINED CMAKE_MACOSX_RPATH)
+ set(CMAKE_MACOSX_RPATH 0)
+ 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")
+ endif()
+@@ -304,13 +304,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)
Added: head/math/lean/files/patch-util_path.cpp
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/files/patch-util_path.cpp Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,14 @@
+--- 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 {
Added: head/math/lean/pkg-descr
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/pkg-descr Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,8 @@
+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.
+
+WWW: https://leanprover.github.io/
Added: head/math/lean/pkg-plist
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ head/math/lean/pkg-plist Sun Jul 22 05:58:39 2018 (r475085)
@@ -0,0 +1,832 @@
+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
+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/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/arith_instance.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_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/norm_num.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/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
+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/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
+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_state.h
+include/lean_ext/library/tactic/unfold_tactic.h
+include/lean_ext/library/tactic/user_attribute.h
+include/lean_ext/library/tactic/vm_monitor.h
+include/lean_ext/library/time_task.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_environment.h
+include/lean_ext/library/vm/vm_exceptional.h
+include/lean_ext/library/vm/vm_expr.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_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_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/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
+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_path.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/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
+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/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
+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
+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/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/coinductive_predicates.lean
+lib/lean/library/init/meta/coinductive_predicates.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/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/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/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/task.lean
+lib/lean/library/init/meta/task.olean
+lib/lean/library/init/meta/transfer.lean
+lib/lean/library/init/meta/transfer.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/propext.lean
+lib/lean/library/init/propext.olean
+lib/lean/library/init/relator.lean
+lib/lean/library/init/relator.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
+ at dir include/lean_ext/cmake/Modules
+ at dir include/lean_ext/shared
+ at dir include/lean_ext/tests/frontends/lean
+ at dir include/lean_ext/tests/kernel
+ at dir include/lean_ext/tests/library/rewriter
+ at dir include/lean_ext/tests/shared
+ at dir include/lean_ext/tests/shell
+ at dir include/lean_ext/tests/util/numerics
More information about the svn-ports-all
mailing list