Leonardo de Moura
|
5f78087b08
|
feat(runtime/object): add support for io.has_finished
|
2018-08-17 12:36:48 -07:00 |
|
Leonardo de Moura
|
5e63e7806c
|
chore(runtime/object): cleanup
|
2018-08-17 12:32:47 -07:00 |
|
Leonardo de Moura
|
ae9eac6781
|
feat(runtime/object): simplify and more tests
|
2018-08-17 09:41:22 -07:00 |
|
Leonardo de Moura
|
c863e86429
|
feat(runtime/object): primitives for interrupting threads
|
2018-08-17 09:25:40 -07:00 |
|
Leonardo de Moura
|
7a7d443ad5
|
test(tests/util/object): improve tests
|
2018-08-17 09:04:08 -07:00 |
|
Leonardo de Moura
|
0a2e9c109f
|
fix(runtime/object): memory leak and violation at task_bind
|
2018-08-17 09:03:45 -07:00 |
|
Leonardo de Moura
|
510a5ffeaa
|
chore(tests/util/object): adjust test
|
2018-08-17 08:48:11 -07:00 |
|
Leonardo de Moura
|
f5ecd8477f
|
fix(runtime/object): memory leak
|
2018-08-17 08:47:29 -07:00 |
|
Leonardo de Moura
|
168eaefff5
|
fix(runtime/object): finalization and avoid leak
|
2018-08-17 08:32:33 -07:00 |
|
Leonardo de Moura
|
cc13c8ee7f
|
refactor(runtime/object): remove unnecessary, fix malloc/delete mismatch
|
2018-08-17 08:10:05 -07:00 |
|
Leonardo de Moura
|
018542e2e1
|
fix(runtime/object): task bugs
|
2018-08-16 21:28:58 -07:00 |
|
Leonardo de Moura
|
066fbf2d5b
|
refactor(runtime/object): remove state field
|
2018-08-16 20:46:14 -07:00 |
|
Leonardo de Moura
|
584eddee01
|
feat(runtime/object): add support for tasks
This is just the first draft. We still need a lot of testing.
|
2018-08-16 19:09:50 -07:00 |
|
Leonardo de Moura
|
67ab1ec8f2
|
chore(util/worker_queue): remove dead code
|
2018-08-16 14:14:57 -07:00 |
|
Leonardo de Moura
|
c322ef0cab
|
fix(tests/util/object): use new calling convention for apply
|
2018-08-15 21:17:50 -07:00 |
|
Leonardo de Moura
|
d14831c470
|
fix(runtime/apply): apply should use the standard calling convention
|
2018-08-15 21:07:54 -07:00 |
|
Leonardo de Moura
|
c3be026645
|
chore(runtime/object): document calling convention for runtime primitives
|
2018-08-15 20:10:43 -07:00 |
|
Leonardo de Moura
|
74d94432da
|
fix(runtime/object): make thunk_get thread safe
|
2018-08-15 15:34:15 -07:00 |
|
Leonardo de Moura
|
4ec43a84ca
|
chore(runtime/object): document standard/borrowed calling convetion
|
2018-08-14 17:43:00 -07:00 |
|
Leonardo de Moura
|
f9bad161c9
|
chore(tests/util/object): fix "unused" variables warnings in release mode
|
2018-08-14 15:19:07 -07:00 |
|
Leonardo de Moura
|
bcb37ef862
|
feat(runtime): thunk serialization
|
2018-08-14 15:15:12 -07:00 |
|
Leonardo de Moura
|
f036a7ad16
|
chore(runtime/object): mk_thunk(c) should not modify c's RC
This is useful when we are generating a function that does not use the
"borrow semantics" for an argument `c` which is used in `mk_thunk(c)`.
|
2018-08-10 18:11:29 -07:00 |
|
Leonardo de Moura
|
6eb598268d
|
chore(runtime/object): naming convention
`dec_ref` methods assume the input object is *not* a scalar
|
2018-08-10 18:11:29 -07:00 |
|
Leonardo de Moura
|
ea8e1075d2
|
feat(runtime/thunk): add runtime support for thunks
We did not use constructor objects for implementing thunks because we
wanted to use `atomic<object *>` to implement the cached result.
|
2018-08-10 18:11:29 -07:00 |
|
Sebastian Ullrich
|
d4364850ff
|
feat(library/derive_attribute): support out_params after main parameter
|
2018-08-02 14:45:37 -07:00 |
|
Sebastian Ullrich
|
e535ebcce8
|
fix(frontends/lean/util): remove reference to obsolete match syntax
|
2018-08-02 14:16:25 -07:00 |
|
Sebastian Ullrich
|
10adf10634
|
fix(library/derive_attribute): prevent infinite loop during parsing
|
2018-08-02 08:08:21 -07:00 |
|
Sebastian Ullrich
|
eda9e4bb3f
|
feat(library/derive_attribute): temporary, hacky C++ implementation of @[derive]
|
2018-08-01 18:44:23 -07:00 |
|
Sebastian Ullrich
|
8033649335
|
chore(library/util): fix doc
|
2018-08-01 18:44:23 -07:00 |
|
Leonardo de Moura
|
9d35d31529
|
refactor(kernel): merge constant_assumption and axiom
|
2018-08-01 09:57:47 -07:00 |
|
Sebastian Ullrich
|
57c25ce01d
|
feat(src/library/vm/vm): profile: record and display self times
|
2018-07-30 17:30:20 -07:00 |
|
Leonardo de Moura
|
c0b93d3694
|
refactor(kernel): remove unnecessary certify_unchecked
|
2018-07-30 12:54:05 -07:00 |
|
Leonardo de Moura
|
6e5440d49f
|
test(tests/library/phashtable): add std::unordered_map test
|
2018-07-30 10:58:22 -07:00 |
|
Leonardo de Moura
|
049a807709
|
test(tests/library/phashtable): simple performance tests
|
2018-07-30 10:29:03 -07:00 |
|
Gabriel Ebner
|
73d4a004ac
|
fix(library/print): add missing break in switch
|
2018-07-27 16:27:57 -07:00 |
|
Sebastian Ullrich
|
046b1890ad
|
feat(src/frontends/lean/decl_util): ignore out_params when deciding whether to include an anonymous inst implicit section variable
|
2018-07-27 14:49:09 -07:00 |
|
Leonardo de Moura
|
95f758d240
|
feat(library/system/io_interface): improve iterate interface
The new version is better for lifting.
|
2018-07-26 16:07:30 -07:00 |
|
Sebastian Ullrich
|
d8122a7284
|
feat(src/frontends/lean/structure_cmd): allow default values in field parameters
|
2018-07-12 17:40:45 +02:00 |
|
Sebastian Ullrich
|
7cb90bedfe
|
fix(src/kernel/old_type_checker): literals in inductive defs
|
2018-07-12 10:55:28 +02:00 |
|
Sebastian Ullrich
|
f254a906b3
|
fix(src/library/vm/vm_io): get_cwd
|
2018-07-05 10:53:07 +02:00 |
|
Sebastian Ullrich
|
80745ba776
|
chore(library/init/data/string/basic): rename string.iterator's next_to_string to remaining_to_string
The old name implied that `curr` was not part of its result
|
2018-07-05 10:42:37 +02:00 |
|
Leonardo de Moura
|
bda46cc9ac
|
feat(kernel): add inductive_decl type on top of runtime/object, and ajust kernel/inductive.cpp
|
2018-06-26 12:16:33 -07:00 |
|
Leonardo de Moura
|
bb0b43798c
|
feat(kernel/declaration): add wrappers for accessing inductive/constructor/recursor declarations
|
2018-06-25 15:01:02 -07:00 |
|
Leonardo de Moura
|
7684860aec
|
feat(kernel): add C++ wrappers for creating inductive declarations
|
2018-06-25 14:24:48 -07:00 |
|
Leonardo de Moura
|
f62256853c
|
refactor(library/init/lean/declaration): use lean.declaration to implement init.meta.declaration
|
2018-06-25 13:08:13 -07:00 |
|
Leonardo de Moura
|
ec1aa2553c
|
refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object
TODO: inductive, constructor, recursor
|
2018-06-25 10:05:45 -07:00 |
|
Leonardo de Moura
|
9c6238e1ac
|
refactor(kernel/declaration): reducibility hints as runtime/object
|
2018-06-25 08:04:44 -07:00 |
|
Leonardo de Moura
|
fd0f142bae
|
chore(kernel/expr): comment
|
2018-06-22 14:48:42 -07:00 |
|
Leonardo de Moura
|
a18c508f5c
|
chore(kernel/old_type_checker): fix test
|
2018-06-22 14:39:46 -07:00 |
|
Leonardo de Moura
|
f809758dd3
|
refactor(kernel/expr): remove extra field
|
2018-06-22 14:35:32 -07:00 |
|