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
Leonardo de Moura
1da93c4d28
feat(CMakeLists, shell/lean): add -D ALPHA=ON cmake option for enabling alpha features (i.e., wip)
...
@jroesch This commit also marks --compile as an alpha feature.
2017-02-26 23:06:45 -08:00
Leonardo de Moura
2386c18ee5
fix(library/tactic/eval): make sure old position information nested in the expression being evaluated is not used in type error messages
...
see #1401
2017-02-26 22:38:24 -08:00
Leonardo de Moura
184d505d51
fix(library/compiler/preprocess): do not unfold noncomputable definitions in the compiler
...
see #1401
2017-02-26 22:05:16 -08:00
Leonardo de Moura
d7674dd060
chore(CMakeLists): bumped master branch to 3.1.1
2017-02-25 18:12:04 -08:00
Gabriel Ebner
fcc0f30b84
fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples
2017-02-25 12:56:46 -08:00
Leonardo de Moura
52221cdbd1
fix(frontends/lean/elaborator): {} elaboration issue
2017-02-24 21:20:39 -08:00
Gabriel Ebner
7e3be51a52
chore(*): remove last remnants of mpfr
2017-02-24 21:42:58 +01:00
Gabriel Ebner
9bcfc06bd0
fix(library/module): has_sorry: check examples
2017-02-24 21:08:49 +01:00
Leonardo de Moura
552a185e6a
feat(frontends/lean): 'let' in 'do' blocks
2017-02-24 09:10:36 -08:00
Sebastian Ullrich
dd379e5b34
refactor(library/equations_compiler/elim_match): simplify is_complete_transition
2017-02-23 01:52:14 +01:00
Sebastian Ullrich
dfe1874365
refactor(frontends/lean/{parser,util}): extract quote functions
...
Also fixes ``f when f is private
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a
feat(frontends/lean/parser): ignore implicit arguments in expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
44b27a9a44
chore(library/vm/vm): fix comment
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3
feat(frontends/lean/parser): expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
3aa9e32c5f
fix(library/equations_compiler/elim_match): always prefer value transitions over complete transitions
2017-02-23 01:21:14 +01:00
Leonardo de Moura
6b76b65881
feat(library/equations_compiler/elim_match): change default max number of steps to 2048
2017-02-21 21:33:10 -08:00
Leonardo de Moura
d9307413b9
feat(library/compiler): skip bytecode optimization for interactive tactics
...
This is just overhead for begin...end blocks.
Moreover, "live variable analysis" is currently a recursive
procedure, and Lean will run of stack space when processing big begin
end blocks (> 1000 tactics).
2017-02-21 21:23:58 -08:00
Leonardo de Moura
ca31ad0107
perf(library/metavar_util): quadratic behavior when assembling the final proof
...
The peformance problem was affecting theorems that contain many `intro`
tactic applications.
@gebner After this optimization, the GAPT benchmark elaboration time went from
1.6 secs to 0.6 secs.
2017-02-21 21:02:43 -08:00
Leonardo de Moura
321105099f
feat(library/type_context): add compilation flag for disabling type inference cache
2017-02-21 20:17:25 -08:00
Leonardo de Moura
09819cb159
feat(library/type_context): add compilation flag for disabling type class resolution flag
2017-02-21 20:04:43 -08:00
Leonardo de Moura
7c57d23b46
feat(kernel): add compilation flags for disabling has_local optimization and abstraction cache
2017-02-21 19:46:31 -08:00
Leonardo de Moura
1c959f6790
feat(kernel): add compilation flag for disabling "free var range" optimization
2017-02-21 19:40:56 -08:00
Leonardo de Moura
622e9a6035
feat(library/type_context): use m_unfold_pred to decide whether macros should be unfolded or not
...
see #1394
2017-02-21 18:07:39 -08:00
Leonardo de Moura
074574be0a
feat(library/vm/vm_array): add native array.iterate and array.foreach
2017-02-21 16:22:25 -08:00
Leonardo de Moura
d9dcb4461e
perf(library/vm/vm_array): minor optimization
2017-02-21 15:43:48 -08:00
Leonardo de Moura
3f87fd15eb
feat(library/vm): add liveness analysis, and support destructive updates for lean arrays
2017-02-21 15:09:37 -08:00
Leonardo de Moura
19cf5e916b
chore(script/gen_constants_cpp): generates a warning if automatically generated C++ function is not used in the source code
2017-02-21 12:05:41 -08:00
Sebastian Ullrich
a053175714
refactor(init/meta,library/vm): use structure for position information
2017-02-21 11:06:39 -08:00
Sebastian Ullrich
bea34eb936
fix(emacs/lean-debug): disable undo in lean-debug buffer
2017-02-21 10:55:15 -08:00
Gabriel Ebner
61c380b534
fix(shell/lean): catch all exceptions
...
Fixes #1386 .
2017-02-21 10:54:46 -08:00
Gabriel Ebner
4ae9312a5f
fix(emacs/lean-input): remove overloading of \b abbreviation
2017-02-21 10:54:19 -08:00
Leonardo de Moura
613a4d6e45
chore(shell/CMakeFiles): enable SMT2 tests
2017-02-21 10:53:03 -08:00
Leonardo de Moura
d1d5428808
feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes
2017-02-21 10:45:31 -08:00
Leonardo de Moura
9863755ae1
feat(shell/lean,library/smt): fix SMT2 frontend
2017-02-21 09:28:21 -08:00
Leonardo de Moura
04fd50e4e8
chore(*): fix tests and style
2017-02-20 23:53:44 -08:00
Leonardo de Moura
87eaedc580
feat(library/vm): shrink VM stack eagerly
...
TODO: liveness analysis objects on the VM stack
2017-02-20 23:10:50 -08:00
Leonardo de Moura
e9a98362d3
feat(library): functional arrays
2017-02-20 22:00:02 -08:00
Leonardo de Moura
2e1221b1b4
chore(CMakeLists): bump version number
2017-02-20 18:06:18 -08:00
Leonardo de Moura
61254847fb
fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression)
2017-02-20 14:51:59 -08:00
Leonardo de Moura
ddee94b831
fix(frontends/lean/elaborator): incorrect invariant due to error recovery
...
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
2017-02-20 14:30:10 -08:00
Leonardo de Moura
296d4b0f09
refactor(library/tactic, library/init/meta): simplify_config => simp_config
2017-02-19 13:10:36 -08:00
Leonardo de Moura
0d22410e2e
feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode
2017-02-19 12:11:22 -08:00
Leonardo de Moura
203a0ac932
feat(library/tactic/smt/smt_state): more restrictive default intros
2017-02-18 22:48:34 -08:00
Leonardo de Moura
0a99910c52
feat(library/init/meta): add exception set to rsimp attributes, use iff lemmas
2017-02-18 19:43:21 -08:00
Leonardo de Moura
0626835530
feat(library/init/meta): add native name_set
2017-02-18 19:07:50 -08:00
Leonardo de Moura
bed3e6c2fd
feat(library/tactic/smt): add get_config and use it to implement slift
...
smt_tactic.slift was losing the configuration.
2017-02-18 17:52:45 -08:00
Leonardo de Moura
c065faaf1f
feat(frontends/lean/elaborator): improve ^. notation
2017-02-18 16:20:21 -08:00
Leonardo de Moura
74f7bc0473
feat(frontends/lean): improve notation for converting infix notation into functions
2017-02-17 23:11:22 -08:00
