Gabriel Ebner
570d905282
chore(util/thread): do not import chrono twice
2016-12-05 12:57:15 -05:00
Leonardo de Moura
c77a987b4d
feat(util/thread): handle thread creation/join failure on Windows
2016-12-05 09:53:41 -08:00
Leonardo de Moura
612cde33b6
feat(util/thread): lthread for Windows
2016-12-05 09:42:21 -08:00
Leonardo de Moura
80d247eaff
fix(src/util): make sure thread stack size is > LEAN_STACK_BUFFER_SPACE
2016-12-03 12:05:01 -08:00
Leonardo de Moura
a9d3f36f76
feat(util/thread,library/mt_task_queue): add lthread
2016-12-03 11:29:22 -08:00
Gabriel Ebner
9ecac28061
feat(CMakeLists,util/thread): fix build with boost
2016-12-02 16:50:03 -08:00
Leonardo de Moura
79d87138f0
feat(util/memory): simplify memory tracking code
2016-12-01 16:07:46 -08:00
Leonardo de Moura
d454cc8bcd
feat(frontends/lean/elaborator): do not populate info_manager during thread finalization
2016-11-30 17:14:15 -08:00
Leonardo de Moura
d40e97b4bc
chore(*): compilation errors, fix style, fix warnings
2016-11-29 11:35:01 -08:00
Gabriel Ebner
3ecfddcbd5
fix(*): fix build
2016-11-29 11:12:43 -08:00
Gabriel Ebner
e448e4e129
refactor(util/task_queue): merge module_task into task and cancel by position
2016-11-29 11:12:43 -08:00
Gabriel Ebner
b668844afe
chore(*): fix style errors
2016-11-29 11:12:43 -08:00
Gabriel Ebner
e1cb1a8cd2
feat(util/task_queue,library/versioned_msg_buf): rudimentary support for task interruption
2016-11-29 11:12:43 -08:00
Gabriel Ebner
3a06a9c15e
feat(util/task_queue): make task_result accesses lock-free
2016-11-29 11:12:43 -08:00
Gabriel Ebner
b5113976aa
fix(util/mt_task_queue): fix segfault
2016-11-29 11:12:43 -08:00
Gabriel Ebner
385ea13688
feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction
2016-11-29 11:12:43 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
7114326b9f
fix(util/realpath): malloc/free mismatch
...
see #1190
2016-11-14 09:42:40 -08:00
Leonardo de Moura
381b2edaf7
feat(library/vm/vm): store .olean file name at vm_decl's
2016-11-11 16:19:19 -08:00
Leonardo de Moura
d66584f390
feat(library/vm,library/compiler): save argument names
2016-11-08 15:10:04 -08:00
Leonardo de Moura
ab12259ba7
chore(util/timeit): style
2016-11-08 08:36:27 -08:00
Leonardo de Moura
bb5033dc57
feat(util/timeit, frontends/lean/definition_cmds): add xtimeit
2016-11-07 17:01:19 -08:00
Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Gabriel Ebner
2d1d1570d3
feat(util/debug): emscripten support
2016-10-16 14:41:35 -07:00
Gabriel Ebner
80cd6205d7
fix(util/file_lock): disable file locks in emscripten
2016-10-16 14:41:35 -07:00
Gabriel Ebner
ec0aa6d248
refactor(*): integrate emscripten build
2016-10-16 14:41:35 -07:00
Leonardo de Moura
6c3d55ff7f
chore(util/json): workaround for mingw
2016-10-14 17:24:47 -07:00
Leonardo de Moura
3162bac4e7
feat(shell/lean): disable assertion violation dialog in server mode
2016-10-13 18:56:10 -07:00
Gabriel Ebner
9e518efe46
fix(util/debug): put lean_unreachable into a block
2016-10-13 18:49:10 -07:00
Gabriel Ebner
bd09d8febe
feat(shell/json): json-formatted error messages
2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2
refactor(*): structured message objects
2016-10-13 18:49:10 -07:00
Gabriel Ebner
837938981e
fix(tests/util/lp): fix debug build
2016-10-03 22:22:12 -07:00
Leonardo de Moura
e9ef7d1342
chore(util/parray): remove dead code
2016-10-03 19:09:57 -07:00
Leonardo de Moura
e6fbbbbc2d
feat(util/rb_map): add unsigned_map
2016-10-03 16:26:58 -07:00
Leonardo de Moura
872360db0f
feat(util/hash): use #if
2016-10-02 10:46:11 -07:00
Leonardo de Moura
ee3c857c88
fix(util/hash): 32-bit version
2016-10-02 10:03:04 -07:00
Leonardo de Moura
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
d4ed8baf3c
chore(util/thread): mark global as static
2016-09-27 15:53:49 -07:00
Leonardo de Moura
da27454c8c
chore(util): remove dead code
2016-09-23 14:29:13 -07:00
Leonardo de Moura
165e2d5b97
chore(*): fix compilation warnings
2016-09-19 17:36:28 -07:00
Gabriel Ebner
4dac796337
feat(library/local_context): make get_unused_name O(log(n))
2016-09-19 16:38:03 -07:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Leonardo de Moura
803c956d18
feat(util/sexpr/option_declarations): allow options to be registered after initialization
2016-08-19 16:58:30 -07:00
Leonardo de Moura
2899f909a6
feat(util/fresh_name): API for detecting whether a name was created using mk_fresh_name
2016-08-05 19:02:31 -07:00
Leonardo de Moura
1b528ba327
chore(util/name): remove assertion
...
The procedure get_tagged_name_suffix violates the assertion.
Alternative solution: change return type of get_tagged_name_suffix to
optional<std::string> since it is only used for pretty printing.
2016-07-30 19:53:58 -07:00
Leonardo de Moura
8b533a54c2
feat(frontends/lean/pp): improve purify_metavars
2016-07-30 15:31:06 -07:00
Sebastian Ullrich
3974d798c8
chore(util/name): remove confusing precondition comment
2016-07-29 23:44:22 -04:00
Sebastian Ullrich
6f4a6c39f3
fix(util/lp): fix compilation error
2016-07-29 23:44:22 -04:00
Sebastian Ullrich
661fafc940
refactor(frontends/lean): replace different attribute classes with single scoped_ext
2016-07-29 18:51:23 -04:00
Leonardo de Moura
01283512a6
feat(frontends/lean/elaborator): add code for deciding which function application elaboration procedure should be used
2016-07-25 12:55:28 -07:00
