max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/library
History
Leonardo de Moura 127ecff79c fix(attribute_manager): finalization problem 
Global variables must be simple types. Reason: the finalization of
global objects in different compilation units is not specified by the
standard. The only exception is the global at src/shared/init.cpp.
It is used to automatically initialize the lean shared library.

Before this commit, attribute_manager used a std::unique_ptr in a global
variable. The test shared_test was crashing in one of my machines
because a different finalization order was being used.
2016-12-20 10:02:31 -08:00
..
compiler fix(library/compiler/erase_irrelevant): issue created by elim_unused_lets optimization 2016-12-14 18:51:53 -08:00
constructions refactor(library, library/tactic): move simp_lemmas and eqn_lemmas to tactic folder 2016-10-12 14:36:00 -07:00
equations_compiler fix(library/equations_compiler/structural_rec): bug in decoder 2016-12-18 22:51:02 -08:00
inductive_compiler feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
native_compiler fix(library/native_compiler/native_compiler): compilation error 2016-12-06 13:16:56 -08:00
tactic fix(library/tactic/simplify): missing clear cache operation 2016-12-19 21:32:46 -08:00
vm feat(library/vm): use native representation for int in the VM 2016-12-18 15:04:02 -08:00
abstract_parser.h feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
aliases.cpp feat(library/aliases,frontends/lean/parser): take local_ref's into account when defining new aliases; use get_local_ref at id_to_expr; use get_local_ref at resolve_local_name 2016-12-15 14:10:44 -08:00
aliases.h refactor(library/aliases,frontends/lean/local_ref_info): merge aliases and local_ref_info modules 2016-12-15 13:24:30 -08:00
annotation.cpp feat(frontends/lean): add support for 'suffices'-expression in the new elaborator 2016-09-08 17:26:27 -07:00
annotation.h feat(frontends/lean): add support for 'suffices'-expression in the new elaborator 2016-09-08 17:26:27 -07:00
app_builder.cpp refactor(kernel): reduce number of configurations supported in the kernel 2016-09-27 17:07:01 -07:00
app_builder.h chore(*): cleanup 2016-09-27 17:30:57 -07:00
arith_instance_manager.cpp refactor(library/type_context): new type class instance cache 2016-09-01 17:37:30 -07:00
arith_instance_manager.h fix(arith_instance_manager): do not store type_context ptr in object 2016-07-29 10:44:44 -07:00
attribute_manager.cpp fix(attribute_manager): finalization problem 2016-12-20 10:02:31 -08:00
attribute_manager.h fix(attribute_manager): finalization problem 2016-12-20 10:02:31 -08:00
aux_definition.cpp fix(library/aux_definition,frontends/lean/definition_cmds): unfold macros at trust level 0 2016-12-05 13:08:12 -08:00
aux_definition.h feat(library/aux_definition): add mk_aux_lemma 2016-09-06 08:57:04 -07:00
aux_recursors.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
aux_recursors.h feat(library): tag auxiliary no_confusion definitions 2016-05-07 15:26:49 -07:00
bin_app.cpp
bin_app.h feat(library/bin_app): uniform foldr, add helper methods for synthesizing recursive functions 2016-07-23 12:11:18 -07:00
cache_helper.h feat(library): add abstract_hash 2016-06-23 14:25:29 -07:00
choice.cpp refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
choice.h chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
class.cpp fix(library/class): bug in whnf_pred predicate 2016-11-05 11:44:05 -07:00
class.h refactor(library): reduce dependecies on old code, simplify normalize module 2016-09-19 22:12:34 -07:00
CMakeLists.txt refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
comp_val.cpp feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
comp_val.h feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
congr_lemma.cpp refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07:00
congr_lemma.h feat(library/tactic): expose congr_lemmas 2016-06-22 19:17:08 -07:00
constants.cpp feat(library): add pre_monad 2016-12-08 12:48:55 -08:00
constants.h feat(library): add pre_monad 2016-12-08 12:48:55 -08:00
constants.txt feat(library): add pre_monad 2016-12-08 12:48:55 -08:00
deep_copy.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
deep_copy.h
defeq_canonizer.cpp feat(src/library/defeq_canonizer): improve cache 2016-10-05 22:00:23 -07:00
defeq_canonizer.h feat(library): add defeq_canonizer 2016-06-24 13:17:09 -07:00
delayed_abstraction.cpp fix(library/delayed_abstraction): nested delayed abstractions 2016-09-15 15:46:25 -07:00
delayed_abstraction.h feat(library/type_context): use delayed abstraction at type_context (instead of restrict_metavars_context) 2016-07-27 14:57:39 -07:00
discr_tree.cpp feat(library): add discrimination trees 2016-10-07 17:07:31 -07:00
discr_tree.h feat(library): add discrimination trees 2016-10-07 17:07:31 -07:00
documentation.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
documentation.h feat(library/documentation, frontends/lean): add /-! -/ doc string module block 2016-11-27 12:23:53 -08:00
exception.cpp chore(library/exception): fix bad message 2016-09-06 18:38:39 -07:00
exception.h feat(library/exception): add nested_exception 2016-09-06 12:57:06 -07:00
explicit.cpp fix(library/explicit): annotation name 2016-09-15 17:57:01 -07:00
explicit.h chore(frontends/lean,library/explicit): remove dead code 2016-07-02 01:57:43 +01:00
export.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
export.h
export_decl.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
export_decl.h chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
expr_lt.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
expr_lt.h
expr_pair.h
expr_pair_maps.h
expr_unsigned_map.h
fingerprint.cpp
fingerprint.h
flycheck.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
flycheck.h feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
fun_info.cpp chore(library/fun_info): patch assertion 2016-11-04 10:14:00 -07:00
fun_info.h refactor(library/fun_info): separate subsingleton information from general param_info 2016-07-07 07:39:26 -07:00
head_map.cpp chore(frontends/lean,library/explicit): remove dead code 2016-07-02 01:57:43 +01:00
head_map.h feat(library): add kabstract 2016-07-16 15:41:31 -04:00
idx_metavar.cpp
idx_metavar.h
init_module.cpp feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
init_module.h refactor(library): move vm to a separate directory 2016-05-12 14:45:06 -07:00
inverse.cpp fix(library/inverse): m_inv_arity was not being stored in the .olean file 2016-10-07 17:08:56 -07:00
inverse.h refactor(library): injectivity ==> inverse 2016-09-07 08:16:14 -07:00
io_state.cpp feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
io_state.h feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
io_state_stream.cpp chore(library): remove lean2 old type checker 2016-09-19 22:21:19 -07:00
io_state_stream.h refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
kernel_serializer.cpp feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
kernel_serializer.h
library_system.cpp chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
library_system.h feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
local_context.cpp feat(library/local_context): make get_unused_name O(log(n)) 2016-09-19 16:38:03 -07:00
local_context.h feat(library/tactic): use annotated_head_beta_reduce instead of head_beta_reduce in tactics 2016-11-21 15:40:12 -08:00
locals.cpp feat(library/locals): add locals_subset predicate 2016-06-24 10:48:01 -07:00
locals.h feat(library/locals): add helper function 2016-08-13 13:35:14 -07:00
max_sharing.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
max_sharing.h
message_buffer.cpp refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
message_buffer.h refactor(library/message_buffer): extract definitions into extra header file 2016-12-12 08:56:15 -05:00
message_builder.cpp chore(*): compilation errors, fix style, fix warnings 2016-11-29 11:35:01 -08:00
message_builder.h fix(frontend/lean/print_cmd): make print work with incorrect proofs 2016-11-29 11:12:43 -08:00
messages.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
messages.h refactor(library/task_queue): break dependency on message_buffer 2016-12-12 09:44:05 -05:00
metavar_context.cpp fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode 2016-10-21 13:33:07 -07:00
metavar_context.h feat(library/tactic): expose new dsimplify in Lean 2016-10-12 07:25:09 -07:00
metavar_util.h fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode 2016-10-21 13:33:07 -07:00
module.cpp perf(kernel,library/module): enable expr caching when deserializing .olean files 2016-12-16 18:33:46 -08:00
module.h refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
module_mgr.cpp fix(library/module_mgr): finally fix invalidation 2016-12-16 18:18:00 -08:00
module_mgr.h fix(library/module_mgr): finally fix invalidation 2016-12-16 18:18:00 -08:00
mpq_macro.cpp fix(arith_instance_manager): shared pointers instead of references 2016-07-29 10:44:44 -07:00
mpq_macro.h feat(src/library/mpq_macro): numeral macros 2016-07-29 10:44:43 -07:00
mt_task_queue.cpp feat(shell/server,emacs): show list of currently running tasks 2016-12-12 12:40:40 -08:00
mt_task_queue.h feat(shell/server,emacs): show list of currently running tasks 2016-12-12 12:40:40 -08:00
noncomputable.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
noncomputable.h
norm_num.cpp
norm_num.h refactor(library/norm_num): use new type_context 2016-05-24 14:11:43 -07:00
normalize.cpp refactor(kernel): reduce number of configurations supported in the kernel 2016-09-27 17:07:01 -07:00
normalize.h refactor(library): reduce dependecies on old code, simplify normalize module 2016-09-19 22:12:34 -07:00
num.cpp feat(library/num): handle nat.zero and (nat.succ nat.zero) at to_num 2016-11-08 16:13:21 -08:00
num.h feat(library,frontends/lean/pp): add support for new string encoding 2016-05-24 16:20:43 -07:00
pattern_attribute.cpp feat(src/library/inductive_compiler): support for nested inductive types 2016-09-16 12:50:59 -07:00
pattern_attribute.h feat(src/library/inductive_compiler): support for nested inductive types 2016-09-16 12:50:59 -07:00
placeholder.cpp feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
placeholder.h feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
pp_options.cpp chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
pp_options.h feat(inductive_compiler): support for mutually inductive types 2016-09-10 14:22:27 -07:00
print.cpp chore(library/print): clang++ compilation warning 2016-09-28 09:11:37 -07:00
print.h feat(frontends/lean/pp): pretty print let-expressions 2016-05-25 14:04:28 -07:00
private.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
private.h chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
projection.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
projection.h chore(library): remove lean2 old type checker 2016-09-19 22:21:19 -07:00
protected.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
protected.h
quote.cpp feat(library/quote): make sure to syntactically identical quoted expressions are not equated 2016-11-10 13:35:54 -08:00
quote.h feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend 2016-06-15 16:06:39 -07:00
reducible.cpp feat(library/reducible): get_reducibility_fingerprint 2016-10-03 13:31:59 -07:00
reducible.h refactor(inductive_compiler): keep simulated inductive types semireducible 2016-10-13 10:12:08 -07:00
register_module.h
relation_manager.cpp feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware 2016-08-18 12:56:44 -07:00
relation_manager.h feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
replace_visitor.cpp fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly 2016-05-01 12:04:28 -07:00
replace_visitor.h fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly 2016-05-01 12:04:28 -07:00
replace_visitor_with_tc.cpp feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information 2016-11-09 16:51:48 -08:00
replace_visitor_with_tc.h feat(library): add replace_visitor_with_tc 2016-08-14 15:45:02 -07:00
scope_pos_info_provider.cpp refactor(frontends/lean,library): move scope_pos_info_provider to library 2016-06-30 10:19:35 +01:00
scope_pos_info_provider.h refactor(frontends/lean,library): move scope_pos_info_provider to library 2016-06-30 10:19:35 +01:00
scoped_ext.cpp chore(library/scoped_ext,tests/lean): fix issues raised by @kha 2016-12-19 10:03:16 -08:00
scoped_ext.h chore(library/scoped_ext,tests/lean): fix issues raised by @kha 2016-12-19 10:03:16 -08:00
shared_environment.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
shared_environment.h feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
sorry.cpp
sorry.h
st_task_queue.cpp refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
st_task_queue.h refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
standard_kernel.cpp refactor(kernel): support only proof irrelevant mode 2016-09-27 17:18:52 -07:00
standard_kernel.h
string.cpp feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
string.h feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
task_helper.cpp refactor(library/message_buffer): extract definitions into extra header file 2016-12-12 08:56:15 -05:00
task_helper.h refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
trace.cpp feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
trace.h fix(library/trace): prevent memory corruption with scope_traces_as_messages 2016-10-13 18:49:10 -07:00
type_context.cpp feat(library/type_context): add yet another approximation to unifier 2016-12-19 20:34:07 -08:00
type_context.h feat(library/type_context): cache failures at is_def_eq 2016-12-13 07:01:12 -08:00
typed_expr.cpp refactor(library/util): isolate util procedures that depend on old_type_checker 2016-03-21 13:36:08 -07:00
typed_expr.h
unfold_macros.cpp refactor(library/exception): avoid throw_generic_exception functions 2016-09-06 12:37:56 -07:00
unfold_macros.h
unification_hint.cpp feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware 2016-08-18 12:56:44 -07:00
unification_hint.h feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
update_declaration.cpp refactor(kernel): add reducibility_hints 2016-09-04 16:30:02 -07:00
update_declaration.h
user_recursors.cpp refactor(kernel): reduce number of configurations supported in the kernel 2016-09-27 17:07:01 -07:00
user_recursors.h feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
util.cpp feat(library/util): add mk_nat 2016-12-06 00:16:31 -08:00
util.h feat(library/util): add mk_nat 2016-12-06 00:16:31 -08:00
versioned_msg_buf.cpp feat(shell,emacs): new lean server protocol 2016-12-06 17:14:29 -08:00
versioned_msg_buf.h feat(shell,emacs): new lean server protocol 2016-12-06 17:14:29 -08:00