Leonardo de Moura
fd487d8db7
chore(*): remove old VM
2019-05-08 15:15:44 -07:00
Leonardo de Moura
9b1c5c09fb
feat(library/compiler/emit_cpp): thread io state
2019-03-18 15:33:29 -07:00
Leonardo de Moura
390c9009f7
chore(shell,boot): update boot, and initialization process
2019-02-14 14:49:16 -08:00
Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -07:00
Leonardo de Moura
ac0352b584
refactor(kernel): remove quotitent normalizer extension
...
The `quot` type is now implemented in the kernel.
We will do the same thing for inductives.
We will not support normalizer extensions anymore in Lean4.
It doesn't make sense since we settled with 2 extensions: quotients and
inductives. Moreover, any new extension would require substantial
changes (e.g., code generator).
The normalizer_extension feature was useful when we were experimenting
with different kernel flavors.
2018-06-01 10:52:17 -07:00
Sebastian Ullrich
3a2fbe2d2f
fix(util/init_module): segfault using clang
2018-05-20 11:01:37 +02:00
Leonardo de Moura
b1d8a17f1b
fix(runtime): add init_module
2018-05-14 20:38:21 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07:00
Leonardo de Moura
4b6583ae9f
refactor(util): move mpz/mpq to util
...
The new lean_obj objects will be defined at util.
Reason: we will define `name`, `options`, `format`, ... on top of lean_obj.
lean_obj depends on mpz.
Remark: lean_obj will replace vm_obj.
2018-04-12 16:43:11 -07:00
Leonardo de Moura
db4b00c7d8
chore(util,library): remove small_object_allocator
...
We use small_object_allocator to allocate vm_obj's.
However small_object_allocator is not thread safe. So, we need to copy
vm_obj's between threads. Moreover, in our experiments, we observed that
JEMALLOC is actually faster than the small_object_allocator.
Here are numbers for the reduced corelib.
small_object_allocator: 15.62 secs
gcc 4.9 allocator: 16.19 secs
jemalloc: 13.83 secs
2018-04-12 16:43:10 -07:00
Leonardo de Moura
3771748b4c
chore(library/native): remove dead code
...
The deleted code was not finished, and we are going to add a new IR
and compiler.
2018-02-07 17:29:25 -08:00
Leonardo de Moura
1e626e382f
chore(frontends/smt2): remove SMT2 frontend
2018-01-24 15:21:52 -08:00
Gabriel Ebner
f5ae60e667
feat(init/init): write allocation stats to stderr
2017-02-28 11:56:52 -08:00
Leonardo de Moura
544d5c67f4
feat(CMakeLists,kernel): add TRACK_LIVE_EXPRS=ON compilation option
2017-02-28 10:56:14 -08:00
Leonardo de Moura
ba641ce29f
feat(CMakeLists,util): add TRACK_CUSTOM_ALLOCATORS=ON compilation option
2017-02-28 10:38:09 -08:00
Jared Roesch
e65d90ac79
feat(*): C++ code generator
...
in progress move of Lean.native to init
2016-12-05 16:11:41 -08:00
Leonardo de Moura
9ef3ebbd5b
refactor(*): delete HoTT support
2016-09-27 16:33:39 -07:00
Daniel Selsam
bc7e081ac1
feat(library/inductive_compiler): scaffold for inductive compiler
2016-08-11 13:48:54 -07:00
Leonardo de Moura
65032fb9a4
fix(init/init): missing initialization
2016-08-11 10:08:30 -07:00
Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
Daniel Selsam
e946ebc8fc
feat(frontends/smt2): new frontend for smt2 format
2016-07-29 10:44:43 -07:00
Leonardo de Moura
cf073f5ed0
feat(library/tactic): add tactic_state
2016-06-08 15:12:22 -07:00
Leonardo de Moura
399b83122c
refactor(library): move vm to a separate directory
2016-05-12 14:45:06 -07:00
Leonardo de Moura
de9df69ef6
refactor(src): move compiler folder to library
2016-05-09 13:28:00 -07:00
Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -07:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Daniel Selsam
21cb409e6c
refactor(library/blast/simplifier): move simplifier module into blast
2015-11-19 19:43:04 -08:00
Leonardo de Moura
33f46fd137
feat(library/blast): parse blast tactic and invoke stub
2015-09-25 12:45:16 -07:00
Leonardo de Moura
49a574dbbf
refactor(compiler): rename elim_rec to preprocess_rec
2015-09-11 17:12:32 -07:00
Leonardo de Moura
ade3f80089
fix(util/thread,init/init): initialization problem
2015-09-03 14:43:50 -07:00
Leonardo de Moura
b02b3d362f
feat(library/simplifier): add simplifier procedure skeleton
2015-07-21 15:08:56 -07:00
Leonardo de Moura
b62e6bb133
feat(library/simplifier): add rewrite rule sets
2015-06-01 15:15:57 -07:00
Leonardo de Moura
8241863abe
feat(kernel/hits): add two builtin HITs: type_quotient and trunc
2015-04-23 15:32:31 -07:00
Leonardo de Moura
b960e123b1
feat(kernel): add experimental support for quotient types
2015-03-31 22:04:16 -07:00
Leonardo de Moura
f948241bb9
feat(library/definitional): add auxiliary functions
2014-12-03 10:28:55 -08:00
Leonardo de Moura
f76c5bbde9
fix(init): initialization problem
2014-10-18 09:01:24 -07:00
Leonardo de Moura
516c0c73b9
refactor(*): remove dependency to thread_local C++11 keyword, the
...
current compilers have several bugs associated with it
We use the simpler __thread (gcc and clang) and
__declspec(thread) (visual studio).
2014-09-24 12:51:04 -07:00
Leonardo de Moura
5489e46ce5
refactor(util/numerics): explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
7e84d5df3d
refactor(util): explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
531046626a
refactor(*): explicit initialization/finalization for environment extensions
2014-09-22 17:30:29 -07:00
Leonardo de Moura
b6781711b1
refactor(*): explicit initialization/finalization for serialization
...
modules, expression annotations, and tactics
2014-09-22 15:26:41 -07:00
Leonardo de Moura
b1ee888aae
refactor(*): start move to explicit initialization/finalization,
...
explicitly initialize/finalize options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-22 10:41:07 -07:00
