Leonardo de Moura
9fb7e5c931
feat(library/equations_compiler): generate equational lemmas for auxiliary _main definitions
2017-05-21 15:21:28 -07:00
Leonardo de Moura
ce71b4c5c2
feat(frontends/lean/definition_cmds): define top-level mutual definitions
...
We still need the equational lemmas.
2017-05-21 10:26:43 -07:00
Leonardo de Moura
4e496b78d5
feat(library/equations_compiler): unpack auxiliary definition
...
We still need to unpack auxiliary lemmas, and propagate information in
the frontend.
2017-05-20 20:34:18 -07:00
Leonardo de Moura
789d4e148f
feat(library/equations_compiler): add pack_mutual
...
This step packs a collection of mutually recursive functions into a
single one. We use `psum` to combine the different domains, and
`psum.cases_on` to combine the codomains.
2017-05-18 15:29:51 -07:00
Leonardo de Moura
cf9a5128c1
fix(frontends/lean/definition_cmds): check_valid_end_of_equations
...
'with' token was missing.
2017-05-18 11:28:02 -07:00
Sebastian Ullrich
aefd312a98
feat(frontends/lean/decl_util): allow opt_param shorthand in all decls
2017-05-17 10:38:12 -07:00
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
