Gabriel Ebner
|
85673cdd8d
|
fix(frontends/lean/definition_cmds): examples in noncomputable theories
|
2017-05-13 09:04:07 +02:00 |
|
Gabriel Ebner
|
271d8ca47a
|
fix(frontends/lean/definition_cmds): make sure auxiliary definitions introduced by abstract do not clash
|
2017-04-27 16:04:18 -07:00 |
|
Gabriel Ebner
|
5324f8c3d3
|
fix(frontends/lean/definition_cmds): use real name as prefix for abstracted proofs
|
2017-04-27 16:04:18 -07:00 |
|
Gabriel Ebner
|
9424e6fa24
|
refactor(frontends/lean/definition_cmds): make profiling threshold configurable
|
2017-04-23 11:22:41 -07:00 |
|
Gabriel Ebner
|
318910f99b
|
refactor(frontends/lean/parser): store snapshots in a lazy async list
|
2017-03-27 14:00:53 -07:00 |
|
Leonardo de Moura
|
900c56be05
|
feat(frontends/lean,library/equations_compiler): abstract proofs in equations and regular definitions
|
2017-03-25 14:22:52 -07:00 |
|
Gabriel Ebner
|
c7ca21625c
|
feat(util/log_tree): annotate nodes with detail levels
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
c5c0a74d77
|
fix(frontends/lean/definition_cmds): reinstate fallback to sorry
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
2799375d24
|
chore(*): style
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
3eba8d3ffc
|
refactor(util/task): do not propagate errors
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
aebd18f136
|
feat(shell/server): only compile region of interest
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
5f872912e0
|
refactor(shell/lean): set exit status 1 iff at least one error was reported
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
595cbb8fe9
|
refactor(*): task<T>, log_tree, cancellation_token
|
2017-03-23 08:57:52 +01:00 |
|
Leonardo de Moura
|
e6c5ba29d6
|
fix(library/message_builder): remove unnecessary field
see #1473
|
2017-03-22 08:23:29 -07:00 |
|
Leonardo de Moura
|
a897fd3f17
|
fix(frontends/lean): pattern matching in the declaration header
|
2017-03-16 01:09:12 -07:00 |
|
Sebastian Ullrich
|
e3b9190fe2
|
refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally.
|
2017-03-15 14:06:34 -07:00 |
|
Gabriel Ebner
|
fcc0f30b84
|
fix(frontends/lean/definition_cmds): set scope_pos_info when checking examples
|
2017-02-25 12:56:46 -08:00 |
|
Gabriel Ebner
|
0c2878e509
|
fix(frontends/lean/definition_cmds): copy position for equation in meta definitions
Fixes #1377.
|
2017-02-17 19:57:49 -08:00 |
|
Sebastian Ullrich
|
9d8c84713c
|
refactor(*): reduce exception context info from expr to pos_info
|
2017-02-17 13:45:57 +01:00 |
|
Gabriel Ebner
|
7946b15511
|
feat(frontends/lean/elaborator): recover from most errors using sorry
|
2017-02-06 15:15:44 +01:00 |
|
Gabriel Ebner
|
95068e4e79
|
feat(library/sorry): make sorry a macro
|
2017-02-05 14:01:03 +01:00 |
|
Gabriel Ebner
|
98c2998a7b
|
feat(frontends/lean/definition_cmds): make noncomputability check non-fatal
|
2017-02-05 13:42:52 +01:00 |
|
Leonardo de Moura
|
b28ed2453e
|
feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations
|
2017-02-04 13:44:05 -08:00 |
|
Leonardo de Moura
|
01414cf21c
|
feat(frontends/lean): add token class, and procedure for consuming the tokens
|
2017-02-03 18:11:06 -08:00 |
|
Leonardo de Moura
|
4d3ff955d3
|
feat(frontends/lean): nicer syntax for default parameter values
See #1340
|
2017-01-30 15:54:26 -08:00 |
|
Gabriel Ebner
|
5fdc737dfc
|
feat(library/tactic): store name of current declaration in tactic_state
|
2017-01-28 08:27:19 +01:00 |
|
Leonardo de Moura
|
750d02c3ac
|
feat(frontends/lean/definition_cmds): remove equations_result macro from elaborated theorems
|
2017-01-24 16:51:33 -08:00 |
|
Leonardo de Moura
|
75525a1120
|
fix(frontends/lean/definition_cmds): allow '.' after equations
|
2017-01-22 12:51:23 -08:00 |
|
Gabriel Ebner
|
a230c47178
|
feat(util/task_queue,emacs,*): highlight running tasks with different background color
|
2017-01-17 17:10:37 -08:00 |
|
Gabriel Ebner
|
1a6629ce3b
|
feat(frontends/lean/parser): keep list of tasks that have to succeed
|
2017-01-17 15:31:17 -08:00 |
|
Leonardo de Moura
|
00c89f209c
|
fix(frontends/lean/definition_cmds): fix #1299
|
2017-01-10 14:38:46 -08:00 |
|
Leonardo de Moura
|
db70c78704
|
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
|
2017-01-06 11:40:34 -08:00 |
|
Leonardo de Moura
|
82f8eeb280
|
feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler
|
2017-01-05 18:02:14 -08:00 |
|
Gabriel Ebner
|
9435762643
|
fix(compiler/vm_compiler): only compile computable non-builtin definitions
|
2017-01-04 16:30:22 -08:00 |
|
Sebastian Ullrich
|
47e7df9b27
|
perf(frontends/lean/definition_cmds): skip definition elaboration during reparsing
|
2016-12-27 10:07:34 -08:00 |
|
Leonardo de Moura
|
7d1c48e673
|
fix(frontends/lean/definition_cmds): "elaboration time" for lemmas was not being reported when using profiler
|
2016-12-25 16:49:58 -08:00 |
|
Leonardo de Moura
|
f9ad1dbfc0
|
fix(frontends/lean/definition_cmds): bug at inline_new_defs
closes #1253
|
2016-12-15 20:32:06 -08:00 |
|
Gabriel Ebner
|
d89512b6fc
|
fix(util/task_queue): fix undefined behavior with null references
|
2016-12-15 09:48:57 -08:00 |
|
Gabriel Ebner
|
8e0a5904d2
|
refactor(library/message_buffer): move info_manager out of scope_message_context
|
2016-12-12 08:23:15 -05:00 |
|
Leonardo de Moura
|
e01c7bfef5
|
chore(frontends/lean/definition_cmds): update comment
|
2016-12-08 10:35:32 -08:00 |
|
Leonardo de Moura
|
e13bac41c3
|
fix(frontends/lean): 'sorry' axiom auto generation
|
2016-12-08 10:31:52 -08:00 |
|
Leonardo de Moura
|
f96d35dc1c
|
fix(library/aux_definition,frontends/lean/definition_cmds): unfold macros at trust level 0
|
2016-12-05 13:08:12 -08:00 |
|
Gabriel Ebner
|
df635b56af
|
fix(frontends/lean/definition_cmds): correctly copy _refl_lemma attributes
|
2016-11-29 11:12:44 -08:00 |
|
Gabriel Ebner
|
e448e4e129
|
refactor(util/task_queue): merge module_task into task and cancel by position
|
2016-11-29 11:12:43 -08:00 |
|
Gabriel Ebner
|
aa03dc03b4
|
refactor(library/tactic/simp_lemmas): mark rfl-lemmas with a _refl_lemma attribute
|
2016-11-29 11:12:43 -08:00 |
|
Gabriel Ebner
|
56f895d6d8
|
feat(kernel/type_checker): option to disable delayed proof-checking
|
2016-11-29 11:12:43 -08:00 |
|
Leonardo de Moura
|
78608a37e9
|
fix(frontends/lean/definition_cmds): implicit universe theorem parameters bug
See discussion at #1178
|
2016-11-29 11:12:43 -08:00 |
|
Gabriel Ebner
|
385ea13688
|
feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction
|
2016-11-29 11:12:43 -08:00 |
|
Gabriel Ebner
|
a8df381d20
|
feat(*): parallel compilation
|
2016-11-29 11:12:40 -08:00 |
|
Leonardo de Moura
|
002c62b49c
|
feat(frontends/lean): basic leandoc tool
|
2016-11-27 14:31:31 -08:00 |
|