Gabriel Ebner
7442aa0752
fix(frontends/lean/parser): better task description
2017-03-24 07:22:28 +01:00
Gabriel Ebner
c55579dd69
fix(frontends/lean/scanner): initialize m_pos
2017-03-24 07:04:35 +01:00
Leonardo de Moura
527c8851a8
refactor(library/system/io): use type classes
2017-03-23 14:29:07 -07:00
Gabriel Ebner
a6f7f31e85
refactor(shell,emacs): handle different checking modes in server
2017-03-23 09:07:09 +01:00
Gabriel Ebner
a8ba78e20a
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
2017-03-23 09:07:08 +01:00
Gabriel Ebner
9dfd8e1018
fix(shell/server): fix field completion
2017-03-23 09:03:43 +01:00
Gabriel Ebner
c7ca21625c
feat(util/log_tree): annotate nodes with detail levels
2017-03-23 09:03:43 +01:00
Gabriel Ebner
098d6f8f2a
refactor(init/meta/tactic): remove report_errors argument from to_expr
2017-03-23 09:03:42 +01:00
Gabriel Ebner
c8fff9f4ff
refactor(init/meta/interaction_monad): replace rstep by istep
2017-03-23 09:03:41 +01:00
Gabriel Ebner
98f86ccabd
chore(frontends/lean/parser): remove obsolete option
2017-03-23 09:01:00 +01:00
Gabriel Ebner
c5c0a74d77
fix(frontends/lean/definition_cmds): reinstate fallback to sorry
2017-03-23 09:01:00 +01:00
Gabriel Ebner
667d06108a
chore(*): fix clang warnings
2017-03-23 09:00:58 +01:00
Gabriel Ebner
2799375d24
chore(*): style
2017-03-23 08:57:56 +01:00
Gabriel Ebner
26ba9c23a7
refactor(util/task): add eager execution
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
60dd85719c
feat(library/system/io): system.io without axioms
2017-03-22 23:36:05 -07:00
Leonardo de Moura
e6c5ba29d6
fix(library/message_builder): remove unnecessary field
...
see #1473
2017-03-22 08:23:29 -07:00
Sebastian Ullrich
da7e21696e
feat(init/meta/interactive): rw goal info on ,
2017-03-22 07:54:12 -07:00
Sebastian Ullrich
524a381f22
refactor(lean/tactic_notation): better goal info tweak on ,
2017-03-22 07:54:12 -07:00
Sebastian Ullrich
f9854be13f
feat(frontends/lean/parser): save id info for non-overloaded constants
2017-03-22 07:35:14 -07:00
Sebastian Ullrich
897b4f9db1
fix(frontends/lean/builtin_exprs): override scope behavior for strict quoted names
2017-03-22 07:34:50 -07:00
Leonardo de Moura
3a878bd3f4
fix(frontends/lean/interactive): compilation warning with older versions of g++
2017-03-21 08:31:16 -07:00
Leonardo de Moura
fdadada3a9
fix(frontends/lean): fixes #1468
...
@kha I had to add yet another hack to fix this issue.
In notation declarations, names are resolved at notation declaration time.
So, users do not expect them to be resolved again at tactic execution time.
I addressed this problem by wrapping constants occurring in notation
declarations with a "frozen_name" annotation. This transformation is
only performed if m_in_quote is true.
Then resolve_names_fn at elaborator.cpp will not try to resolve the
names again.
This change broke two other modules. `-` notation for inverting
equations at `rw`, and `calc` expressions inside quotes.
The broke for the same reason. They were not expecting the constants
to be wrapped with an annotation.
2017-03-18 13:48:21 -07:00
Sebastian Ullrich
5e0e19c4ad
fix(frontends/lean/{interactive,tactic_notation}): fix tests
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
60a244e4f9
fix(frontends/lean,shell): fix file dependencies
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
e0856284b0
feat(frontends/lean,emacs): tactic info before elaboration, fix many edge cases
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
421a6d6f01
feat(frontends/lean/interactive,emacs): highlight current tactic parameter
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
24e7e87f7d
feat(frontends/lean/tactic_notation): fall back to tactic info when hovering over/between parameters
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
9b5e7ddcda
feat(frontends/lean/interactive,emacs): hide colon separator in front of pretty-printed types
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
c46936d180
fix(frontends/lean/interactive): hard-code tactic pretty printing
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
e3a65ee794
refactor(frontends/lean/interactive,shell/server): factor out JSON reporting code
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
803d3073ae
feat(frontends/lean): add interactive.type_formatter attribute and use it to pretty print interactive tactics
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
0792bc13db
feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer
2017-03-17 18:20:44 -07:00
Leonardo de Moura
11dcab1b31
fix(frontends/lean/elaborator): fixes #1458
2017-03-16 10:31:21 -07:00
Leonardo de Moura
a897fd3f17
fix(frontends/lean): pattern matching in the declaration header
2017-03-16 01:09:12 -07:00
Leonardo de Moura
36770119b6
feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes)
2017-03-15 14:45:13 -07:00
Daniel Selsam
7f56f23e70
chore(frontends/lean/inductive_cmds): allow sorrys
2017-03-15 14:06:56 -07:00
Sebastian Ullrich
e3b9190fe2
refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally.
2017-03-15 14:06:34 -07:00
Sebastian Ullrich
c325438453
fix(frontends/lean/elaborator): let expr patterns
2017-03-15 14:06:08 -07:00
Sebastian Ullrich
647d7a8501
fix(frontends/lean/elaborator): expr patterns should ignore binding names
2017-03-15 14:06:00 -07:00
Leonardo de Moura
9ce9c0331f
feat(frontends/lean/elaborator): add option 'elaborator.coercion'
...
This option is available in Lean 2, but it was accidentally removed
from Lean 3.
2017-03-12 11:27:41 -07:00
Leonardo de Moura
bc7089dc70
chore(frontends/lean/elaborator): retract c58f61e
...
See discussion at #1438
2017-03-12 09:58:57 -07:00
Daniel Selsam
f3e71e52fc
feat(frontends/smt2/parser.cpp): allow tracing from the smt tactic
2017-03-12 09:54:09 -07:00
Leonardo de Moura
c694dbd600
fix(frontends/lean/elaborator): conflict between (: t :) and (::) notations
...
It was preventing us from using `(::)`
2017-03-12 09:29:42 -07:00
Leonardo de Moura
9c24b81cbf
feat(frontends/lean/elaborator): improve error message
2017-03-11 16:35:40 -08:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08:00
Sebastian Ullrich
e3bfd90b06
fix(frontends/lean/elaborator): default recover_from_error to false for most commands
...
Fixes #1446
fix(frontends/lean/util): quoting private name
uncovered by now failing run test
2017-03-09 20:51:35 -08:00
