Gabriel Ebner
2edefdcc12
fix(library/vm/vm_task): fix trace messages
2017-03-23 08:57:56 +01:00
Gabriel Ebner
10e354952b
feat(emacs): do not call auto-completion on tab
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
6887a99f08
feat(library/init/category/state): make state and state_t universe polymorphic
...
The new definitions are not fully general since they force data and
state to be in the same universe.
2017-03-22 23:45:29 -07:00
Leonardo de Moura
60dd85719c
feat(library/system/io): system.io without axioms
2017-03-22 23:36:05 -07:00
Leonardo de Moura
3f42e5fbd9
chore(util/rb_tree): style
2017-03-22 08:31:48 -07:00
Corey Richardson
52f84c139b
chore(lp): don't use readdir_r on glibc
...
glibc (unfortunately) deprecated readdir_r, as their readdir is already
reentrant. Future versions of POSIX will assume readdir is reentrant,
see https://www.gnu.org/software/libc/manual/html_node/Reading_002fClosing-Directory.html
2017-03-22 08:24:55 -07:00
Leonardo de Moura
59d1b1ee2e
fix(util/rb_tree): avoid warning
...
see #1473
2017-03-22 08:24:17 -07:00
Leonardo de Moura
e6c5ba29d6
fix(library/message_builder): remove unnecessary field
...
see #1473
2017-03-22 08:23:29 -07:00
Scott Morrison
d6f5370ea7
doc(fixing_broken_links)
...
A stopgap fix for broken links in `library.md`. Addresses #1649 for now.
2017-03-22 08:13:36 -07:00
Leonardo de Moura
875493a1ee
chore(tests/lean/inject): fix test
2017-03-22 08:04:11 -07:00
Sebastian Ullrich
a5db5ae4de
refactor(init/meta/interactive): rw: parse - separately to remove hack
2017-03-22 07:54:12 -07:00
Sebastian Ullrich
9cf80a6c94
feat(init/meta/interactive): rw goal info on ]
2017-03-22 07:54:12 -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
Leonardo de Moura
c541f90d5b
fix(library/tactic/vm_monitor): compilation warning
2017-03-22 07:40:16 -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
Sebastian Ullrich
793f0baee8
feat(library/tactic/vm_monitor): use attribute for registering VM monitors
2017-03-22 07:34:27 -07:00
Rob Lewis
2e921dd533
fix(algebra): generalize theorem
2017-03-22 07:34:01 -07:00
Leonardo de Moura
8feacb27a6
feat(library/data): add buffer
2017-03-21 18:47:50 -07:00
Leonardo de Moura
40f69b976e
test(tests/lean/inject): add more tests
2017-03-21 13:38:46 -07:00
Leonardo de Moura
a31de3b7bc
feat(library/unification_hint): improve unification_hint matcher
...
Improvements:
- Use heuristic match explicit arguments first and then match implicit.
- Skip annotations.
- Follow metavariable assigments.
- Use is_def_eq when pattern doest not contain matching variables.
2017-03-21 10:19:34 -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
aa68d72fa5
fix(library/equations_compiler/elim_match): skip nonvar + inaccessible
2017-03-21 08:08:36 -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
Leonardo de Moura
31b6dc222d
feat(library/init/meta/expr): add expr.is_annotation
2017-03-18 13:40:11 -07:00
Leonardo de Moura
3322adde1b
fix(library/tactic/subst_tactic): fixes #1467
2017-03-17 19:54:35 -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
7c31e62b16
feat(init/meta/interactive): improve pretty-printing of list_of and itactic
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
Sebastian Ullrich
ae3e685c1f
chore(tests/lean): forgot to add test case
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
c387c34365
fix(test/lean/interactive/run_single): include stderr
2017-03-17 18:05:19 -07:00
Sebastian Ullrich
9137248707
fix(library/vm/vm_rb_map): assertion violation in destructor of vb_rb_map_ts_copy with nat keys or values
2017-03-17 18:05:11 -07:00
Gabriel Ebner
886c824e33
feat(library/init/data/list/instances): prove decidability of bounded quantification
2017-03-17 18:03:26 -07:00
Leonardo de Moura
b803377d5e
fix(library/tactic/smt/congruence_closure): relation used to implement congruence tables was not transitive
2017-03-17 16:04:41 -07:00
Leonardo de Moura
ed9e6fb940
chore(tests/lean/type_error_at_eval_expr): fix test
2017-03-17 14:46:41 -07:00
Leonardo de Moura
8ff176717c
feat(library/tactic/smt/congruence_closure): add check_congr_keys assertions
2017-03-17 13:48:12 -07:00
Leonardo de Moura
37c69427b3
feat(library/tactic/smt/congruence_closure): make sure congruence closure module does not assign metavariables when using is_def_eq
2017-03-17 13:48:09 -07:00
Leonardo de Moura
71cd9baf7d
feat(library/type_context): add nd_is_def_eq
2017-03-17 13:47:11 -07:00
