Gabriel Ebner
41643d6400
fix(library/compiler/vm_compiler): prevent segfault
2016-11-04 09:47:17 -07:00
Leonardo de Moura
5075891f66
chore(library/vm/vm): fix gcc 4.8 warning
2016-11-04 09:46:16 -07:00
Gabriel Ebner
ef1fc9871b
feat(library/vm/vm): profiler: show cumulative runtimes
2016-11-04 09:39:12 -07:00
Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Leonardo de Moura
6173d95d18
feat(library/module,frontends/lean): store line/column number information
2016-11-02 16:55:21 -07:00
Leonardo de Moura
3212d9c83a
fix(library/module): store .olean file where inductive datatype was defined
2016-11-02 16:07:36 -07:00
Leonardo de Moura
cea572a167
feat(library/module): store .olean file name for imported declarations
2016-11-02 15:37:33 -07:00
Leonardo de Moura
3958d8485a
chore(library/module): remove dead code
2016-11-02 15:02:49 -07:00
Leonardo de Moura
9d3aa5b627
fix(library/compiler/elim_recursors): bug in elim_recursors
...
We may fail to type check auxiliary definitions that use rec_fn_macro.
The problem is that this macro cannot be unfolded.
So, we fix the problem by not type checking them. We add them as
constants, and store the definition in an auxiliary vector.
2016-11-02 14:19:28 -07:00
Leonardo de Moura
e62810c9b8
fix(library/compiler/lambda_lifting): make sure constructors are eta-expanded
...
closes #1133
2016-11-02 13:26:15 -07:00
Leonardo de Moura
30ae8a29b6
fix(library/compiler/elim_recursors): some recursor applications were not being eliminated
2016-11-02 13:05:52 -07:00
Daniel Selsam
05add2ea02
fix(library/tactic/simplify.cpp): fix debug tracing names
2016-11-02 10:23:38 -07:00
Leonardo de Moura
b22192eee1
fix(library/equations_compiler/elim_match): fixes #1171
...
We should not use value-transition (based on if-then-else) when there
are dependencies.
2016-10-31 17:42:39 +08:00
Gabriel Ebner
e18370585d
fix(frontends/lean/server): fix relative dependency lookups
2016-10-30 08:42:05 +08:00
Leonardo de Moura
a77e4b5abf
fix(library/compiler/erase_irrelevant): bug at is_comp_irrelevant
2016-10-27 11:51:37 +08:00
Leonardo de Moura
fa3475fa66
fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode
...
This commit also removes a "hack" that tried to fix this problem for
universe meta-variables only. Moreover, the hack was incomplete, since
it would not consider nested metavars.
2016-10-21 13:33:07 -07:00
Leonardo de Moura
a9fe684f26
chore(library/tactic/simplify): fix warning in release mode
2016-10-21 13:28:12 -07:00
Sebastian Ullrich
989761045b
fix(src/emacs/lean-server): revert 133b70c0 for emacs < 25
2016-10-19 19:47:36 -07:00
Leonardo de Moura
99299d1915
feat(library/tactic/simplify): use propext in rewriting rules when simplify_config.use_axioms is tt
2016-10-19 17:59:01 -07:00
Leonardo de Moura
a4ef8f385d
feat(library/tactic/simplify): add basic support for lambda-expressions
2016-10-19 14:15:56 -07:00
Leonardo de Moura
205d524409
refactor(library/tactic/simplify): delete old simplifier
2016-10-19 14:03:14 -07:00
Sebastian Ullrich
f10d5e4d8c
fix(library/vm/vm_io): disable get_line in server mode
2016-10-19 10:02:58 -07:00
Sebastian Ullrich
044b989679
fix(library/vm/vm_io): capture put_str/put_nat output in server mode
2016-10-19 10:02:58 -07:00
Sebastian Ullrich
133b70c0e3
fix(emacs): don't try to parse server stderr as json, instead notify on server crash
2016-10-19 10:02:58 -07:00
Leonardo de Moura
64c3927e0b
feat(library/equations_compiler/elim_match): report unused equations
...
closes #1162
2016-10-19 09:58:08 -07:00
Leonardo de Moura
e74cfa9db7
fix(library/equations_compiler/elim_match): bug at complete transition
...
It also updates the condition for triggering the inaccessible
transition. Before this commit, we would only perform this kind
of transition if *all* terms were marked inaccessible. Now,
we perform it if *some* are marked inaccessible. Reason:
when we perform the complete transition we don't have enought
information for deciding whether an argument should be marked as
inaccessible or not. If this decision creates confusion for users,
we may try to mark them with an "maybe-inaccessible" annotation, and
then enforce that the inaccessible transition is performed onlty if
*all* terms are marked as inaccessible or *maybe-inaccessible"
2016-10-19 09:10:19 -07:00
Leonardo de Moura
053389b70b
feat(library/init/meta/simp_tactic): add new simp primitives
2016-10-19 08:41:25 -07:00
Leonardo de Moura
4d52de6f33
refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested
2016-10-18 16:18:25 -07:00
Leonardo de Moura
fa01e062ef
feat(library/tactic/simplifier): add simplify_core_fn
...
TODO: remove dead code from old simplifier
2016-10-17 09:51:49 -07:00
Leonardo de Moura
7b806755d9
chore(library/tactic/simplify): remove subsingleton support
...
It is left over from the blast tactic.
Moreover, it is incomplete.
2016-10-16 22:11:12 -07:00
Leonardo de Moura
835c888936
feat(library/tactic/simplify): simplify cache
2016-10-16 16:39:33 -07:00
Leonardo de Moura
bd8478bb25
chore(library/tactic/simplify): remove m_ctx_slss
2016-10-16 16:28:50 -07:00
Leonardo de Moura
aee951af9b
chore(library/tactic): move simplifier to tactic folder
2016-10-16 16:25:14 -07:00
Leonardo de Moura
f833736e35
chore(library/tactic/simplifier): remove unnecessary file
2016-10-16 16:19:01 -07:00
Leonardo de Moura
9810a5f941
refactor(library/tactic/simplifier): simplify simplifier
2016-10-16 15:55:30 -07:00
Gabriel Ebner
ec0aa6d248
refactor(*): integrate emscripten build
2016-10-16 14:41:35 -07:00
Leonardo de Moura
0f72de217a
chore(library/tactic/simplifier): simplify simplifier
2016-10-15 18:14:59 -07:00
Leonardo de Moura
5318b0cf39
fix(library/tactic/backward/backward_lemmas): uninitialized value
2016-10-15 13:21:46 -07:00
Leonardo de Moura
0bb155a427
chore(*): remove .clean support
...
In Lean2, we used to cache elaborated definitions in .clean files. The
main goal was to optimize each flycheck invocation produced by Emacs.
The Lean3 definition package was not updating this cache. Moreover, it
is not necessary because the new compilation server subsumes it.
2016-10-13 19:58:58 -07:00
Leonardo de Moura
0ee1eed751
chore(library/type_context): comment assertion violated by the pretty printer
2016-10-13 19:34:58 -07:00
Gabriel Ebner
b14a0c43ff
feat(frontends/lean/parser,library/module): warn if imported modules are out-of-date
2016-10-13 18:49:10 -07:00
Gabriel Ebner
60afce092a
fix(library/trace): prevent memory corruption with scope_traces_as_messages
2016-10-13 18:49:10 -07:00
Gabriel Ebner
66be9c31db
refactor(library/flycheck): use flycheck_message_stream instead of option
2016-10-13 18:49:10 -07:00
Gabriel Ebner
5acb722d46
refactor(library/flycheck,library/trace): convert trace output to messages independently of flycheck
2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2
refactor(*): structured message objects
2016-10-13 18:49:10 -07:00
Leonardo de Moura
bf7bae6eaf
feat(library/init/meta/tactic): add beta/zeta tactics
2016-10-13 18:47:27 -07:00
Daniel Selsam
b4644acba4
fix(meta/mk_dec_eq_instance): handle indices and ginductives
2016-10-13 10:12:37 -07:00
Daniel Selsam
ae730532c8
fix(inductive_compiler): preserve invariant that all basic ir names are <ind_name>.<atomic>
2016-10-13 10:12:08 -07:00
Daniel Selsam
047556528d
refactor(inductive_compiler): keep simulated inductive types semireducible
2016-10-13 10:12:08 -07:00
Leonardo de Moura
881aa6d023
perf(library/type_context): small optimization
...
It makes a big difference in examples such as:
example (p : nat → Prop) (a : nat) (h : false) : p (a + 5000) :=
begin
unfold add has_add.add nat.add bit0 bit1 one has_one.one,
contradiction
end
2016-10-12 21:39:10 -07:00
