max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
15215 commits 1 branch 0 tags 5.3 GiB
Commit graph

861 commits

Author SHA1 Message Date
Leonardo de Moura
efa703d2b5 feat(runtime): implement string.iterator primitives in the new runtime 
Some of the primitives do not have optimal implementation.

@Kha Could you please check if everything we use in the parser has a
reasonable implementation?
 2018-11-15 10:42:23 -08:00
Leonardo de Moura
23202bada1 chore(runtime/object): allow shared objects at string_append and string_push 2018-11-14 16:30:23 -08:00
Leonardo de Moura
a368ed2185 test(tests/util/object): add map test 2018-10-27 20:50:09 -07:00
Leonardo de Moura
46d6f7bfb5 chore(runtime/object): store function pointer as void * inside closure 2018-09-11 14:27:45 -07:00
Leonardo de Moura
7c7eccf6ad test(tests/util/object): add perf test 2018-09-11 08:27:25 -07:00
Leonardo de Moura
0573d7e1d5 fix(runtime/object): parray RC bugs 2018-09-09 12:04:27 -07:00
Leonardo de Moura
36423e4389 fix(runtime): parray memory leaks 2018-09-09 10:33:15 -07:00
Leonardo de Moura
2a24f4a09b test(tests/util/object): add parray test 2018-09-09 10:21:55 -07:00
Leonardo de Moura
4863ca071a chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
Leonardo de Moura
8f195515a6 feat(runtime): add persistent arrays to runtime 2018-09-09 09:44:38 -07:00
Sebastian Ullrich
a7b1de8bf7 chore(tests/shell/test): remove 2018-09-08 18:37:58 -07:00
Sebastian Ullrich
b3c44ec56e chore(shell/{server,lean_js}): remove 2018-09-08 18:37:58 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
00032a7d37 chore(tests/shell/shell_test): fix output 
BTW, we should probably temporarily delete this test.
 2018-09-04 17:22:16 -07:00
Leonardo de Moura
805e45bba5 chore(tests/shell): fix test 2018-08-27 17:54:43 -07:00
Leonardo de Moura
3ab1ebcb3f feat(init/core): add task 2018-08-21 16:10:07 -07:00
Leonardo de Moura
0b349f1abf chore(*): fix style 2018-08-21 09:32:01 -07:00
Leonardo de Moura
dc1f5c0aa6 feat(runtime/object): task API functions can take thunks as arguments 2018-08-20 09:13:35 -07:00
Leonardo de Moura
db98397cc0 feat(runtime): object compactor 
We need more testing and performance testing.
We also need to compare serializer and compacted_region.
 2018-08-19 17:10:18 -07:00
Leonardo de Moura
684085d93f refactor(runtime/object): delete data needed to execute task after it finishes 2018-08-18 14:33:27 -07:00
Leonardo de Moura
a0b5502821 fix(runtime/object): memory leak and simplify task_object 
We remove per task condition_variable and use m_task_finished_cv.
The same condition_variable used to implement `wait_any`.
 2018-08-18 10:29:12 -07:00
Leonardo de Moura
4bc8414d2b feat(runtime/object): use "weak pointers" in the task manager, and interrupt tasks at GC time 2018-08-17 15:35:00 -07:00
Leonardo de Moura
24444d65c4 refactor(runtime/object): do not use Lean runtime lists to implement the reverse dependency list in task objects 2018-08-17 14:42:43 -07:00
Leonardo de Moura
1d5411f455 feat(runtime/object): add support for io.wait_any 2018-08-17 13:04:06 -07:00
Leonardo de Moura
5f78087b08 feat(runtime/object): add support for io.has_finished 2018-08-17 12:36:48 -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
510a5ffeaa chore(tests/util/object): adjust test 2018-08-17 08:48:11 -07:00
Leonardo de Moura
018542e2e1 fix(runtime/object): task bugs 2018-08-16 21:28:58 -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
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
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
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
Leonardo de Moura
3729c7ffb2 chore(kernel/expr): remove some old/legacy functions 2018-06-22 12:52:14 -07:00
Leonardo de Moura
bc57c66ae3 refactor(kernel/level): naming consistency 2018-06-22 10:29:56 -07:00
Leonardo de Moura
01ea596aea refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -07:00
Leonardo de Moura
e14255e7ae chore(util/sexpr): remove sexpr serializer 
It was dead code.
Moreover, sexpr will not be part of Lean4
 2018-06-20 11:27:29 -07:00
Leonardo de Moura
9ef934e090 chore(util): style 2018-06-15 16:05:11 -07:00
Leonardo de Moura
13c532d0d4 fix(*): truncation bugs 
- Lean strings (like std::string) may contain null characters. The
  codebase was ignoring this issue.

- We now have a wrapper `string_ref` for wrapping Lean string objects in
  C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
  Remark: I also found a few places where the code relies on the
  following property which is not true
  Forall s : std::string, std::string(s.c_str()) == s

- `name` object wrapper was assuming that all numerals were small
  `nat` values. This is true in most cases, but the system would
  crash when processing if it is a big number.

- The commit tries to make sure runtime/util/kernel are correct.
  Modules that will be deleted contain many `TODO` comments
  indicating they may crash and/or produce incorrect results
  when strings contain null characters and numerals are big.

cc @kha

@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.

After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.

I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
 2018-06-15 16:05:11 -07:00
Leonardo de Moura
3843c50cd7 chore(tests/kernel): remove old test 2018-06-14 13:49:27 -07:00
Leonardo de Moura
4432629eb0 feat(util/nat): add C++ wrapper for manipulating runtime nat values 2018-06-13 09:29:52 -07:00
Leonardo de Moura
62788a9ca3 refactor(kernel): fix terminology: "free_var" is actually a loose bound variable 
We represent free variables uisng local constants.
We will fix this terminology too.
 2018-06-08 13:25:36 -07:00
Leonardo de Moura
c697cf4c29 chore(tests/util): remove exception test 2018-06-07 16:28:54 -07:00
Leonardo de Moura
de82517d80 refactor(kernel): remove abstract since we only use abstract_locals 2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00