7 commits

Author	SHA1	Message	Date
Leonardo de Moura	a944d158a3	feat(CMakeLists.txt): add SMALL_RC cmake option ... When used with `COMPRESSED_OBJECT_HEADER`, Lean uses a compressed object header where only 32-bits are reserved for the RC. The motivation is performance, in our experiments, it is faster to access a 32-bit counter than a 45-bit one. With a smaller RC, we can use 8-bits for the memory kind information, and speedup its access.	2019-08-28 14:54:08 -03:00
Leonardo de Moura	6553c5531c	fix(runtime): bugs at compact.cpp and object size calculation	2019-08-24 07:40:38 -07:00
Leonardo de Moura	dcd15f3424	refactor(runtime): C backend	2019-08-24 07:40:38 -07:00
Leonardo de Moura	1da4782483	feat(runtime, library/init/io): add io.ref	2019-03-16 22:16:28 -07:00
Leonardo de Moura	0b349f1abf	chore(*): fix style	2018-08-21 09:32:01 -07:00
Leonardo de Moura	a27aa53e88	refactor(runtime/compact): save task objects as thunks ... TODO: modify task API and make sure all functions there can take thunks instead of tasks as arguments.	2018-08-20 08:52: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