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

144 commits

Author SHA1 Message Date
Leonardo de Moura
feea8ecccd feat(library/compiler/llnf): avoid inc/dec operations on persistent objects 
inc/dec operations are noop's for persistent objects.
 2019-02-18 20:22:18 -08:00
Leonardo de Moura
b752dd1984 fix(library/compiler/emit_cpp): mark global objects as persistent 
They may be used by tasks, but they are not directly reachable from
task starting point.
 2019-02-17 11:45:51 -08:00
Leonardo de Moura
8ac1a1969d fix(runtime/object): task.bind and task.map should also invoke to_mt 2019-02-17 11:11:41 -08:00
Leonardo de Moura
827021a6c5 feat(runtime/object): given mk_task(o), mark objects reachable from o as MTHeap 2019-02-17 10:29:41 -08:00
Leonardo de Moura
d100f95469 feat(runtime/object): make dbg_trace thread safe 2019-02-17 09:50:55 -08:00
Leonardo de Moura
7623f64b5e feat(runtime,library/init/util): add some debugging helper function 2019-02-17 09:22:37 -08:00
Leonardo de Moura
9e0b28d8ce feat(library/init/data/array/basic): improve 2019-02-16 16:08:10 -08:00
Leonardo de Moura
3c73c43ab2 feat(runtime,library/init/data/array/basic): add builtin support for arrays 2019-02-16 15:27:23 -08:00
Leonardo de Moura
00b177ad54 chore(runtime/object): enable Lazy RC by default 
@kha I tried a compiling a few .lean examples using Lazy RC, and I did
not observe any significant increase in memory consumption.
 2019-02-15 12:10:57 -08:00
Leonardo de Moura
06f1a2b1a0 feat(runtime/object): lazy RC 
In this commit, we replace the option `LEAN_DEFERRED_FREE` with
`LEAN_LAZY_RC`. The idea is to match the nomenclature used in the
literature. See paper:
https://dl.acm.org/citation.cfm?id=964019
The following slide deck summarizes the paper:
http://www.hboehm.info/popl04/refcnt.pdf

We also implement the very simple approach described on this paper
where a `del(o)` just puts `o` in the "to free" list, and each
allocation frees at most one object. As pointed out in the paper
above lazy RC may prevent a lot of memory from being reclaimed.
For now, I am keeping the new option disabled.

That being said, the test `arith_eval_nat.lean` is 29% faster when
using lazy RC, and beats the OCaml version.

In the following paper
https://www.microsoft.com/en-us/research/wp-content/uploads/2017/01/tm567-1.pdf
a separate thread keeps processing the "to free" list. However, I
think this approach is not compatible with our
`object_memory_kind::STHeap` trick.

Tomorrow, I will measure the space overhead when compiling the Lean
corelib using Lazy RC using my linux desktop

cc @kha
 2019-02-14 17:41:11 -08:00
Sebastian Ullrich
956a047d1e chore(library/compiler/extern_attribute): style 2019-02-14 14:07:05 -08:00
Sebastian Ullrich
7cffe6935e feat(frontends/lean/vm_elaborator): port to new runtime 2019-02-14 14:07:05 -08:00
Leonardo de Moura
03d5ac2a3c feat(runtime): add LEAN_DEFERRED_FREE compilation option 
It prevents the runtime from performing arbitrarily long pauses when
invoking `del`.
 2019-02-14 10:40:10 -08:00
Leonardo de Moura
b722885137 feat(library/init/io): add unsafe_io and timeit 2019-02-13 16:59:24 -08:00
Leonardo de Moura
e10240fe5c refactor(runtime/io): use extern "C" for io primitives 2019-02-13 11:21:29 -08:00
Leonardo de Moura
4627929a83 refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI 2019-02-13 08:27:23 -08:00
Leonardo de Moura
425a4b70d1 feat(library/init/data/int/basic): use extern attribute, and fix div/mod mess 
Now, int.div and int.mod behave like C++ `/` and `%` for int,
moreover, they satisfy

          (a/b)*b + (a%b) = a
 2019-02-12 11:41:46 -08:00
Leonardo de Moura
6be47dfb97 feat(library/init/data/string/basic): use extern attribute 2019-02-11 17:54:24 -08:00
Sebastian Ullrich
ece423300b fix(runtime/object): avoid implicit string allocation in string.iterator.curr/next/remove 2019-02-09 14:18:04 +01:00
Leonardo de Moura
434627ee8e chore(runtime/io): implement io.prim.put_str just to be able to test 2019-02-06 14:35:13 -08:00
Leonardo de Moura
fbc6c47094 chore(boot): update 2019-02-06 09:59:22 -08:00
Sebastian Ullrich
83e0c35204 chore(runtime/object): closure double-free assert 2019-02-06 09:38:35 -08:00
Leonardo de Moura
c4e8770342 feat(runtime,boot): second part of the previous commit 2019-02-05 16:28:18 -08:00
Leonardo de Moura
2058d33d07 feat(runtime,library/compiler): add name.dec_eq builtin 2019-02-05 14:36:02 -08:00
Leonardo de Moura
eb57a904af chore(runtime): avoid overloads 2019-02-05 14:04:29 -08:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Leonardo de Moura
579ac58b62 chore(runtime/object): expose thunk_map and thunk_bind 2019-02-04 13:11:37 -08:00
Leonardo de Moura
98edae152a fix(runtime): replace lean::alloca with macro 
Functions using `alloca` are not inlined even when marked with
`inline` in some compilers.

Remark: GCC will _not_ inline a function calling alloca unless it is
annotated with always_inline.
 2019-02-04 09:36:53 -08:00
Leonardo de Moura
0918a599ae feat(*): builtin support for uint functions 
@kha The VM versions just throw exceptions. They are just stubs to
make sure we can compile Lean.
I implemented the uint functions in the new runtime, but there are a
few missing cases marked with TODO.
I needed these builtins to be able to compile the C++ generated code for
corelib.
 2019-02-01 17:04:24 -08:00
Sebastian Ullrich
a8f668a3d2 feat(runtime/object): add LEAN_FAKE_FREE option to disable freeing runtime objects while debugging 2019-02-01 16:33:18 +01:00
Sebastian Ullrich
c162ec9583 fix(runtime/object): mk_option_some 2019-02-01 16:33:13 +01:00
Sebastian Ullrich
e3afa47c9e fix(runtime/object): fix some string primitives 2019-02-01 16:33:11 +01:00
Sebastian Ullrich
e0fc2a7812 feat(runtime/object): string_to_std 2019-02-01 16:32:52 +01:00
Leonardo de Moura
4166851574 feat(library/compiler/emit_cpp): emit_box and emit_unbox 2019-01-31 16:16:30 -08:00
Leonardo de Moura
7c3354f15f feat(library/compiler/emit_cpp): emit_reset 2019-01-31 12:33:17 -08:00
Leonardo de Moura
d2cbf9584f feat(library/compiler/emit_cpp): emit _apply instruction 2019-01-30 14:37:21 -08:00
Leonardo de Moura
bb43567273 fix(runtime/object): typos 2019-01-29 16:03:40 -08:00
Sebastian Ullrich
ead4e8998d feat(library/init/lean/elaborator): elaborate constants 2018-12-19 15:04:48 +01:00
Leonardo de Moura
3a7d407d6c feat(library/compiler/builtin): register io primitives 
TODO: implement `io` primitives in the new runtime
 2018-11-15 16:14:50 -08:00
Leonardo de Moura
b501613f8c feat(library/compiler/builtin): register string primitive functions 2018-11-15 13:26:41 -08:00
Leonardo de Moura
70c4e33cf2 feat(runtime/object): missing string.iterator builtin functions 2018-11-15 13:05:29 -08:00
Leonardo de Moura
d0e96ee600 feat(runtime/object): missing int builtins 2018-11-15 12:31:34 -08:00
Leonardo de Moura
a3db4e8e09 chore(*): style 2018-11-15 10:59:17 -08:00
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
ed4eeddf0a feat(runtime/object): add more string primitives 2018-11-14 16:51:10 -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
9258a12ed4 feat(library/compiler): add new builtin management module 
TODO: register `int`, `string` and `io` primitives
 2018-11-14 15:58:12 -08:00
Leonardo de Moura
81545c12f2 chore(runtime/object): fix comment 2018-09-11 14:31:14 -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
e8fa692611 chore(runtime/object): change default object_memory_kind to STHeap 2018-09-11 13:57:55 -07:00