Leonardo de Moura
4d6da3dd69
fix(runtime/compact): bug at read
2018-08-28 10:30:51 -07:00
Leonardo de Moura
161431e995
feat(kernel): implement new mutual_definition declaration object
...
This commit also removes the old `environment::add_meta` hackish method.
2018-08-28 10:30:44 -07:00
Leonardo de Moura
5c47ff82f6
chore(library/init/lean/core): remove dead code
2018-08-28 08:56:03 -07:00
Leonardo de Moura
cdb2824d86
fix(library/module): debug build
2018-08-28 08:09:57 -07:00
Leonardo de Moura
b63b05e5fd
fix(runtime/thread): MULTI_THREAD=OFF build
2018-08-28 08:08:55 -07:00
Leonardo de Moura
030669ea4d
feat(runtime): do not waste space with RC for region and stack allocated objects
...
The modification introduces an overhead of 1.5% on the
execution time. Here is the the time for compiling the corelib
Before: 8.61 secs (avg of 3 runs)
After: 8.74 secs (avg of 3 runs)
On the other hand, the size of the compacted region for the command
`#compact_tst 10` is smaller.
Before: 176687728
After: 153794704
The size before this change was 14.8% bigger.
For reference, using the old serializer we generate a buffer of size 105291117.
cc @kha
2018-08-28 07:41:55 -07:00
Leonardo de Moura
5313cd3467
fix(library/init/meta/pos): missing file
2018-08-28 07:41:41 -07:00
Leonardo de Moura
805e45bba5
chore(tests/shell): fix test
2018-08-27 17:54:43 -07:00
Leonardo de Moura
776c977742
refactor(kernel): continue constant_info/declaration refactoring
2018-08-27 17:23:26 -07:00
Leonardo de Moura
96ff6b1718
feat(util/object_ref): add helper functions
2018-08-27 16:28:37 -07:00
Leonardo de Moura
3f5db74ab4
refactor(library/init/lean/declaration): rename declaration_val ==> constant_val
...
It doesn't make sense to call it `declaration_val` anymore.
2018-08-27 16:07:38 -07:00
Leonardo de Moura
ae18cee0ea
chore(library/module): remove pos_info tracking
...
We will use a completely different approach in Lean4
2018-08-27 15:55:57 -07:00
Leonardo de Moura
2ab2265d22
chore(library/module): remove dead APIs
2018-08-27 15:40:20 -07:00
Leonardo de Moura
dec166b387
chore(library/module): remove dead info
2018-08-27 15:35:10 -07:00
Leonardo de Moura
d27a360912
chore(library/update_declaration): remove dead file
2018-08-27 15:18:23 -07:00
Leonardo de Moura
27ef29a50f
refactor(kernel/declaration): continue constant_info/declaration refactoring
2018-08-27 13:22:10 -07:00
Leonardo de Moura
7bf032d6fe
chore(frontends/lean): remove calc-expression
2018-08-27 12:20:54 -07:00
Leonardo de Moura
66adac6af6
chore(library/init): avoid calc at corelib
2018-08-27 12:17:30 -07:00
Leonardo de Moura
4917ab0c65
chore(library): remove congr_lemma
2018-08-23 16:48:43 -07:00
Leonardo de Moura
e0f7fa3bd9
chore(library/tactic): remove leftovers
2018-08-23 16:00:34 -07:00
Leonardo de Moura
d334bb1fa7
chore(*): remove more stuff
2018-08-23 15:56:31 -07:00
Leonardo de Moura
17ae59b5b0
chore(*): remove more stuff
2018-08-23 15:27:12 -07:00
Leonardo de Moura
c21555240a
chore(library/tactic): remove more stuff
2018-08-23 15:20:07 -07:00
Leonardo de Moura
646cdfdf40
chore(library/init/meta): remove well_founded_tactics
2018-08-23 15:14:22 -07:00
Leonardo de Moura
5f65b3a6f1
chore(library/tactic): remove unused bindings
2018-08-23 15:04:23 -07:00
Leonardo de Moura
e2b912237d
chore(library/native_compiler): remove leftovers
2018-08-23 14:58:57 -07:00
Leonardo de Moura
a7f6d1d38d
chore(library/tactic): remove tactic/eval.cpp and tactic/gexpr.cpp
2018-08-23 14:54:41 -07:00
Leonardo de Moura
22101a2c55
chore(library/tactic): remove assert_tactic and change_tactic
2018-08-23 14:50:55 -07:00
Leonardo de Moura
05a6d8a791
chore(library/tactic): remove destruct_tactic, generalize_tactic and fun_info_tactics
2018-08-23 14:47:51 -07:00
Leonardo de Moura
8434f43146
chore(library/init/meta): remove interactive.lean
2018-08-23 14:41:47 -07:00
Leonardo de Moura
973eb89e40
chore(library/init/meta/lean): remove old parser support
2018-08-23 14:39:10 -07:00
Leonardo de Moura
d405e54a6f
chore(library/init/meta/tactic): reduce tactic.lean
2018-08-23 14:37:40 -07:00
Leonardo de Moura
ed5d884d8f
chore(library/tactic): remove app_builder_tactics
2018-08-23 14:22:00 -07:00
Leonardo de Moura
a6604dcf56
chore(library/tactic): remove rewrite and apply and interactive tactics
2018-08-23 14:18:16 -07:00
Leonardo de Moura
7a47406c4c
chore(library/tactic): remove simp_lemmas
2018-08-23 14:10:36 -07:00
Leonardo de Moura
88c8c560a9
chore(library/equations_compiler): do not generate equation lemmas
2018-08-23 14:04:37 -07:00
Leonardo de Moura
3abcd0c9e8
chore(frontends/lean/elaborator): remove invoke_tactic
2018-08-23 13:49:47 -07:00
Leonardo de Moura
69734dfb3a
chore(tests/lean): fix tests
2018-08-23 13:49:07 -07:00
Leonardo de Moura
e5c3f04937
chore(frontends/lean): remove tactic notation
2018-08-23 13:44:52 -07:00
Leonardo de Moura
d27ef3d3b0
chore(frontends/lean/builtin_cmds): remove tactic framework dependency
2018-08-23 13:34:38 -07:00
Leonardo de Moura
d0f6bbdf02
chore(tests/lean): replace run_cmd with #eval
2018-08-23 13:32:25 -07:00
Leonardo de Moura
a1fffb2c9d
chore(tests/lean/fail/run_command): obsolete test
2018-08-23 13:30:07 -07:00
Leonardo de Moura
22ba0a1155
chore(library): remove inverse.cpp
...
We used this module to implement inductive_compiler pack/unpack functions
2018-08-23 13:16:27 -07:00
Leonardo de Moura
8e351d46a1
chore(library/equations_compiler): remove support for pack/unpack
...
We don't need it anymore because we removed inductive_compiler/nested.cpp
2018-08-23 13:16:27 -07:00
Leonardo de Moura
7fb763c50f
chore(library/tactic): remove dsimp and unfold tactics
2018-08-23 11:57:38 -07:00
Leonardo de Moura
a10e81e6a6
chore(frontends/lean/elaborator): remove unfold tactic dependency
2018-08-23 11:57:38 -07:00
Leonardo de Moura
ef27df8907
chore(library/tactic): remove simp
2018-08-23 11:57:38 -07:00
Leonardo de Moura
9b4f59e511
chore(library/inductive_compiler): remove simp references
2018-08-23 11:57:38 -07:00
Leonardo de Moura
fc96c335fb
chore(library/constructions): remove has_sizeof
...
This will be implemented in Lean in the future.
2018-08-23 11:57:38 -07:00
Leonardo de Moura
dc479c6837
chore(library/inductive_compiler): remove mutual.cpp
2018-08-23 11:57:38 -07:00
