Leonardo de Moura
6107da05db
fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283
2014-10-29 19:47:14 -07:00
Leonardo de Moura
9547e2d077
feat(library/tactic): add rotate_left/rotate_right tactics, closes #278
2014-10-29 19:13:55 -07:00
Leonardo de Moura
8e9f97e95e
fix(frontends/lean): do not save identifier info
2014-10-29 17:38:59 -07:00
Leonardo de Moura
c1653a9fb4
feat(frontends/lean): only valid proof states should be displayed, closes #275
2014-10-29 17:29:40 -07:00
Soonho Kong
5ad312f6ce
test(emacs/lean-info-test): add test cases for goal visualization
...
[skip ci]
2014-10-29 17:09:08 -07:00
Soonho Kong
6973d3e7aa
feat(emacs/lean-info): add goal visualization options 'lean-proofstate-display-style'
...
lean-proofstate-display-style:
- 'show-all: Show all goals
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ b ∧ c
- 'show-first: Show only the first
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
- 'show-first-and-other-conclusions: Show the first goal, and the
conclusions of all other goals (DEFAULT OPTION)
a : Prop,
b : Prop,
c : Prop,
H_1 : a,
H_2 : b,
H_3 : c
⊢ id a
⊢ b ∧ c
Close #279
2014-10-29 17:08:55 -07:00
Leonardo de Moura
a98b12f067
fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276
2014-10-29 16:51:06 -07:00
Leonardo de Moura
95e843e8ed
feat(library/tactic/proof_state): add empty line between goals, closes #281
2014-10-29 16:51:06 -07:00
Leonardo de Moura
b0a7888346
fix(emacs/lean-flycheck): should accept error messages with empty lines
2014-10-29 16:51:06 -07:00
Leonardo de Moura
1c9992800f
fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277
2014-10-29 16:51:06 -07:00
Leonardo de Moura
88d55bfef0
fix(library/definitional/projection): remove redundant 'error in'
2014-10-29 16:51:06 -07:00
Soonho Kong
854e7ba1be
fix(emacs/lean-type): improve displaying proof state messages
...
- Do not repeat the same message
- Do not display the empty message
- Do not display "[stale]" for proof states
2014-10-29 16:02:48 -07:00
Soonho Kong
99f85c8dbc
fix(emacs/lean-info): proofstate display problem
2014-10-29 14:33:05 -07:00
Soonho Kong
fe710ac6d0
test(emacs/lean-info-test): add test for proofstate info
2014-10-29 14:33:05 -07:00
Soonho Kong
17455d191b
feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer
2014-10-29 14:33:05 -07:00
Soonho Kong
12824c3e27
fix(emacs/lean-syntax): fix Type1, Type2 highlight
2014-10-29 14:33:05 -07:00
Soonho Kong
b0e249ce63
feat(emacs/lean-type): output INFO to *lean-info* buffer in addition to minibuffer
...
Close #260
2014-10-29 14:33:05 -07:00
Soonho Kong
0d8658d762
feat(emacs/lean-settings): add lean-show-proofstate-in-minibuffer option
2014-10-29 14:33:05 -07:00
Soonho Kong
53f79ec9c2
feat(emacs): extract proof state information attached to ","
2014-10-29 14:33:05 -07:00
Soonho Kong
fdf5f3ff8a
feat(emacs/lean-info): add PROOF_STATE info
...
Close #259
2014-10-29 14:33:05 -07:00
Soonho Kong
cb83eca2f3
feat(emacs/lean-input): add lean-input-export-translations
2014-10-29 14:33:05 -07:00
Leonardo de Moura
30571ce418
fix(library/definitional/projection): error messages for projection generation
2014-10-29 13:39:17 -07:00
Leonardo de Moura
fe4ea48381
feat(library/definitional/projection): add projection generator, closes #257
2014-10-29 13:13:05 -07:00
Leonardo de Moura
0c185fc4ab
fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274
2014-10-29 08:57:34 -07:00
Leonardo de Moura
a2ef835809
fix(frontends/lean): squiggle position for unary begin-end block
2014-10-28 23:26:24 -07:00
Leonardo de Moura
e22eb3543c
feat(library/tactic): add whnf tactic, closes #270
2014-10-28 23:18:49 -07:00
Leonardo de Moura
83e4c0fcec
feat(frontends/lean): hide tactic "types"
...
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508
feat(frontends/lean): modify begin-end semantics, closes #258
2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc
feat(frontends/lean/info_manager): add separator -- when displaying PROOF_STATE info
...
This feature was implemented to address issue #259
2014-10-28 16:39:21 -07:00
Leonardo de Moura
186e598bf8
feat(library/tactic/goal): add option pp.compact_goals
2014-10-28 16:30:37 -07:00
Leonardo de Moura
a3801e84d4
fix(library/tactic/goal): avoid unnecessary line break when possible
2014-10-28 16:17:33 -07:00
Leonardo de Moura
ea739100b3
fix(library/unifier): broken optimization in the unifier
...
See new comments and tests for details.
2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660
fix(kernel/inductive): relax eliminator generation rules for empty types
...
This commit also removes the workaround false.rec_type. It is not needed anymore
2014-10-28 10:31:00 -07:00
Leonardo de Moura
60f32fa709
fix(frontends/lean): begin-end automatic tactic notation bug, fixes #262
2014-10-27 17:12:25 -07:00
Leonardo de Moura
78bc3ef7e4
feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization
...
This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
2014-10-27 16:49:29 -07:00
Leonardo de Moura
bca2be56ec
feat(library/normalize): add new flavors of normalize procedure
2014-10-27 16:25:30 -07:00
Leonardo de Moura
7516fcad97
feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261
2014-10-27 13:16:50 -07:00
Leonardo de Moura
2e5ad274a5
fix(frontends/lean/elaborator): remove invalid assertions
...
These assertions became invalid when we changed the behavior of undef
indentifiers at
8e6de93394
2014-10-27 10:31:09 -07:00
Leonardo de Moura
ee5a982c01
feat(shell/lean): add '--server-trace' flag, closes #264
2014-10-27 10:26:29 -07:00
Leonardo de Moura
d66e5a6c41
fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming
2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab
fix(frontends/lean/elaborator): nested begin-end bug
2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba
fix(frontends/lean): improve begin-end construct
2014-10-26 15:47:29 -07:00
Leonardo de Moura
08e8161243
feat(emacs/lean-syntax): add 'eassumption' highlight
2014-10-26 15:45:26 -07:00
Leonardo de Moura
fd60cf6a79
feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification
...
See new node.inj4 theorem, we need the extra power to be able to avoid type information at
exact (assume e₁ e₂, e₁)
2014-10-26 10:27:33 -07:00
Leonardo de Moura
aed9a88b38
fix(frontends/lean/parser): save identifier info for undef local
2014-10-26 10:19:44 -07:00
Leonardo de Moura
8e6de93394
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
2014-10-26 09:47:11 -07:00
Leonardo de Moura
50948be66b
fix(emacs/lean-syntax): syntax highlight for composite names in declarations
2014-10-26 09:27:17 -07:00
Leonardo de Moura
707584376a
fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file
2014-10-25 17:56:22 -07:00
Leonardo de Moura
c7f6a6b94e
feat(library/definitional/cases_on): automatically add 'cases_on'
2014-10-25 17:22:02 -07:00
Leonardo de Moura
c751bdd9e6
chore(library/definitional): remove dead code
2014-10-25 15:11:48 -07:00
Leonardo de Moura
fa1bf40d0f
fix(library/definitional): make sure argument is an inductive datatype
2014-10-25 15:09:24 -07:00
Leonardo de Moura
cdcde661ef
feat(library/definitional/induction_on): automatically add 'induction_on'
2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Leonardo de Moura
7240a1a640
feat(kernel/inductive): add get_num_minor_premises and get_num_type_formers APIs
2014-10-25 11:17:29 -07:00
Leonardo de Moura
2bc034da2c
feat(kernel/inductive): expose 'get_elim_name' API
2014-10-25 10:47:12 -07:00
Leonardo de Moura
9e69a95b26
feat(kernel/inductive): add API for retrieving the number of indices in an inductive datatype
2014-10-25 10:42:05 -07:00
Leonardo de Moura
c30c0fa3b8
fix(kernel/metavar): avoid crash due to stack overflow, closes #253
2014-10-25 00:20:59 -07:00
Leonardo de Moura
096c67b2e5
fix(library/unifier): occurs-check bug
2014-10-25 00:16:02 -07:00
Leonardo de Moura
5830da9e2d
fix(frontends/lean/tokens): typo
2014-10-24 14:44:59 -07:00
Leonardo de Moura
aaad9633fb
fix(library/tactic/expr_to_tactic): memory leak
2014-10-24 14:40:36 -07:00
Leonardo de Moura
7a033ac07e
feat(frontends/lean): add 'print axioms' command, close #251
2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0
feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant
2014-10-24 08:23:26 -07:00
Leonardo de Moura
79d0347721
feat(library/tactic): add generalize tactic, closes #34
...
Remark: the intros tactic has been added in a different commit: 7d0100a340
2014-10-23 22:40:15 -07:00
Leonardo de Moura
b83b065d00
feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic.
2014-10-23 22:36:32 -07:00
Leonardo de Moura
f9aa1a1b84
refactor(library/tactic/goal): remove unnecessary parameter
2014-10-23 21:22:52 -07:00
Leonardo de Moura
ab4c292872
fix(build): do not disable unicode chars on Windows
2014-10-23 20:58:23 -07:00
Leonardo de Moura
f027acb5cb
fix(frontends/lean): missing type info in expressions nested in tactics
2014-10-23 18:31:05 -07:00
Leonardo de Moura
a6571c3273
feat(frontends/lean): add 'print definition' command
2014-10-23 14:54:15 -07:00
Soonho Kong
04b4e36701
doc(emacs/README.md): fix typo
...
[skip ci]
2014-10-23 14:32:36 -07:00
Leonardo de Moura
22ae42d3af
fix(frontends/lean/info_manager): use fresh formatter displaying each info object
...
The formatter may cache results.
2014-10-23 14:29:17 -07:00
Leonardo de Moura
20ab59c740
fix(frontends/lean/pp): avoid unnecessary parentheses when pretty printing delimited notation
2014-10-23 14:14:08 -07:00
Leonardo de Moura
43cfd5c26a
fix(library/tactic): add missing file
2014-10-23 14:04:12 -07:00
Leonardo de Moura
212ae0b61c
feat(frontends/lean): automatically add 'info' tactic in begin-end blocks
...
Actually, the tactic is only added when Lean is in collect-info mode.
2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a
feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode
2014-10-23 13:18:30 -07:00
Leonardo de Moura
40235c6af0
fix(kernel/type_checker): propagate 'memoize' flag to default_converter
2014-10-23 13:15:53 -07:00
Leonardo de Moura
8e3ac023bb
feat(library/reducible): expose 'memoize' flag
2014-10-23 13:09:59 -07:00
Leonardo de Moura
cadc9b3ff3
feat(frontends/lean/info_manager): add proof_state info
2014-10-23 10:40:07 -07:00
Leonardo de Moura
38a9aa2a98
feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions
2014-10-23 10:26:19 -07:00
Leonardo de Moura
00f9a10e82
refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic
...
This change also enabled us to remove hacks used in the tests modified
by this commit.
2014-10-23 10:26:19 -07:00
Leonardo de Moura
2c330e704e
fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures
2014-10-23 10:26:19 -07:00
Leonardo de Moura
6fcba192b2
refactor(library/tactic): move 'unfold' tactic to separate module
2014-10-23 10:26:19 -07:00
Leonardo de Moura
96d7d9c8d9
feat(library/tactic/elaborate): do not invoke unifier if no constraints were generated during elaboration
2014-10-23 10:26:19 -07:00
Leonardo de Moura
f3fdc70400
refactor(library/tactic): add auxiliary module 'library/tactic/elaborate'
2014-10-23 10:26:11 -07:00
Leonardo de Moura
3aec70b92c
feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time
2014-10-22 22:13:37 -07:00
Leonardo de Moura
c50227ea6e
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
...
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
2014-10-22 18:11:09 -07:00
Leonardo de Moura
60132912a4
refactor(library/tactic): remove unnecessary hack
...
It is not needed anymore.
We had to use this hack when we had tactic_macro_definition_cell.
2014-10-22 17:41:19 -07:00
Leonardo de Moura
7c62446023
refactor(frontends/lean): remove dead code
2014-10-22 17:39:06 -07:00
Leonardo de Moura
eb2b59ce4f
refactor(frontends/lean): remove unnecessary files
2014-10-22 17:33:16 -07:00
Leonardo de Moura
e95c7c5f70
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-22 17:29:50 -07:00
Leonardo de Moura
9a316092d1
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic
2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
2014-10-22 17:29:50 -07:00
Leonardo de Moura
7c617955d0
refactor(library/tactic): move 'exact' tactic to separate module
2014-10-22 17:29:44 -07:00
Leonardo de Moura
323715e951
refactor(library/tactic): move 'tracing' tactics to separate module
2014-10-22 14:12:45 -07:00
Soonho Kong
ef60e6abd2
fix(shell/lean.cpp): use temp ios
2014-10-21 17:23:02 -07:00
Leonardo de Moura
33f18b9454
fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion
...
The bug is exposed by new unit test
2014-10-21 16:54:25 -07:00
Leonardo de Moura
6b89080b1a
feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248
2014-10-21 16:28:36 -07:00
Leonardo de Moura
e24225fabf
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
2014-10-21 15:39:47 -07:00
Leonardo de Moura
1896e6e273
feat(frontends/lean): allow 'reserve' inside namespaces
2014-10-21 15:39:47 -07:00
Leonardo de Moura
bb953b80aa
feat(frontends/lean): reserve notation, closes #95
2014-10-21 15:39:47 -07:00
Soonho Kong
ba9d0a2b7f
fix(shell/CMakeLists.txt): merge into a single lean.js file
2014-10-21 16:18:12 -04:00
Soonho Kong
ec43ad51ca
feat(shell/lean.cpp): use trust_lvl=10000, flycheck for EMSCRIPTEN
2014-10-21 00:43:26 -07:00
Leonardo de Moura
2f62a5e887
fix(frontends/lean/info_manager): disable notation pretty printer when displaying OVERLOAD information
...
We need that otherwise the Lean emacs mode will display useless overload
information such as:
[+] int.add : ℤ → ℤ → ℤ
overloaded with #1 + #0 , #1 + #0
Note that this only became an issue after we implemented the new pretty printer
2014-10-20 22:06:33 -07:00
Leonardo de Moura
92acd9affc
chore(emacs): do not highlight arbitrary types
2014-10-20 19:17:02 -07:00
Leonardo de Moura
815dc9b63d
chore(library/tactic/expr_to_tactic): remove dead code
2014-10-20 18:59:57 -07:00
Leonardo de Moura
8a44dfc1df
fix(frontends/lean/pp): bug in pretty printer notation match procedure
2014-10-20 18:58:27 -07:00
Leonardo de Moura
40fb66bf07
feat(frontends/lean): change default precedence to 1
2014-10-20 18:40:55 -07:00
Leonardo de Moura
e2fa981e89
fix(frontends/lean/pp): avoid parentheses around atomic notation
2014-10-20 18:08:13 -07:00
Leonardo de Moura
53a64ac767
refactor(library/tactic): move intros_tactic initialization to intros_tactic module
2014-10-20 17:47:52 -07:00
Leonardo de Moura
3c4419ff23
refactor(library/tactic): move rename_tactic to separate module
2014-10-20 17:41:40 -07:00
Leonardo de Moura
ac9397816f
refactor(library/tactic): move apply_tactic initialization to apply_tactic module
2014-10-20 17:32:32 -07:00
Leonardo de Moura
e68007a727
fix(frontends/lean/builtin_tactics): adjust tactics precedence
2014-10-20 17:10:16 -07:00
Leonardo de Moura
9b8f60b739
feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block
...
This is useful when debugging proofs.
2014-10-20 15:59:49 -07:00
Leonardo de Moura
a3aca96cb9
fix(frontends/lean/builtin_exprs): error position
2014-10-20 15:56:58 -07:00
Leonardo de Moura
fd40999909
feat(frontends/lean): uniform unsolved goals "error" position
2014-10-20 15:52:06 -07:00
Leonardo de Moura
7d0100a340
feat(library/tactic): add 'intros' tactic
2014-10-20 15:26:16 -07:00
Leonardo de Moura
5cba7244ce
fix(library/tactic/expr_to_tactic): argument evaluation order is not part of the standard
2014-10-20 15:16:38 -07:00
Leonardo de Moura
33c4715f4c
fix(frontends/lean/pp): suppress unnecessary '[annotation]' marks
2014-10-20 11:16:21 -07:00
Leonardo de Moura
f0cc17af87
fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used
2014-10-20 08:31:36 -07:00
Leonardo de Moura
a1006073d4
feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence
2014-10-19 13:39:06 -07:00
Leonardo de Moura
469368f090
refactor(frontends/lean/scanner): move basic UTF8 procedures to separate module
2014-10-19 13:29:15 -07:00
Leonardo de Moura
4d4bc0551f
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation
2014-10-19 13:08:15 -07:00
Leonardo de Moura
ed1afe26bd
feat(frontends/lean/pp): support scopedexpr notation in the pretty printer
2014-10-19 12:50:40 -07:00
Leonardo de Moura
f63d47fef3
feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer
2014-10-19 11:16:24 -07:00
Leonardo de Moura
100b3abf1d
fix(frontends/lean/pp): bug in notation matching procedure
2014-10-19 10:48:41 -07:00
Leonardo de Moura
d7cc7cbd8c
refactor(frontends/lean/pp): remove 'reverse' hack
2014-10-19 09:56:18 -07:00
Leonardo de Moura
eef1cc4ac2
fix(frontends/lean/pp): implicit arguments in notation
2014-10-19 09:04:43 -07:00
Leonardo de Moura
555d26aa61
feat(frontends/lean/pp): take notation declarations into account when pretty printing
...
TODO: support foldl/foldr and binders
2014-10-19 08:41:29 -07:00
Leonardo de Moura
8cfb3ae687
fix(library/module): bug in import_module
2014-10-18 21:03:22 -07:00
Leonardo de Moura
6a31a79265
refactor(frontends/lean/inductive_cmd): move auxiliary method to expr.h
2014-10-18 15:11:26 -07:00
Leonardo de Moura
eb79af98ba
feat(frontends/lean/parse_config): add get_notation_entries auxiliary function for returning the list of notation declarations that start with a given head symbol
...
This API is need to take notation declarations into account when pretty
printing expressions.
2014-10-18 11:49:27 -07:00
Leonardo de Moura
f17e67efcb
feat(frontends/lean/parse_table): add get_head_index auxiliary function for indexing notation declarations
2014-10-18 10:55:39 -07:00
Leonardo de Moura
f76c5bbde9
fix(init): initialization problem
2014-10-18 09:01:24 -07:00
Leonardo de Moura
2369388629
refactor(kernel/instantiate): cleanup beta-reduce
2014-10-17 20:19:51 -07:00
Leonardo de Moura
1ce3b83d79
fix(kernel/metavar): compilation error in some compilers
2014-10-17 17:22:25 -07:00
Leonardo de Moura
6285c3a217
perf(util/list): use memory pool for list cells
2014-10-17 17:08:39 -07:00
Leonardo de Moura
58aff5b4af
perf(kernel/metavar): used thread local cache for instantiate_metavars
2014-10-17 17:08:35 -07:00
Leonardo de Moura
6d64da2981
perf(kernel/expr_eq_fn): use thread local cache, and avoid memory allocation/deallocation
2014-10-17 16:44:20 -07:00
Leonardo de Moura
7cc3dd0b4d
chore(kernel/replace_fn): "name" constant
2014-10-17 14:20:35 -07:00
Leonardo de Moura
b6afbcb7f5
perf(kernel/replace_fn): use 'recursive' replace_fn for "small" terms
2014-10-17 14:15:09 -07:00
Leonardo de Moura
c21c8c582f
feat(util/buffer): expose capacity method
2014-10-17 14:05:36 -07:00
Leonardo de Moura
10b880ce3b
perf(kernel/metavar): improve occurs_expr and occurs performance
2014-10-17 14:05:22 -07:00
Leonardo de Moura
50e4c6f252
feat(util/rb_tree): add find_if method
2014-10-17 12:53:43 -07:00
Leonardo de Moura
d2cbd25985
refactor(kernel): replace_visitor doesn't need to be in the kernel anymore
2014-10-17 10:23:35 -07:00
Leonardo de Moura
14ebbda8cb
perf(kernel/metavar): minor improvement
2014-10-16 21:43:54 -07:00
Leonardo de Moura
8974b52f7b
perf(library/unifier): avoid unnecessary wasteful computation
2014-10-16 17:16:49 -07:00
Leonardo de Moura
fe484b26f3
refactor(kernel/expr): remove dead code
2014-10-16 13:45:36 -07:00
Leonardo de Moura
3b6b23c921
refactor(kernel/expr): remove silly overloads
2014-10-16 13:37:55 -07:00
Leonardo de Moura
c4f02bd16a
refactor(kernel/expr): remove dead code
2014-10-16 13:09:26 -07:00
Leonardo de Moura
97a7dae12a
refactor(kernel/expr): remove code duplication
2014-10-16 12:48:49 -07:00
Leonardo de Moura
28128e0330
fix(frontends/lean): EXTRA_TYPE info
2014-10-16 12:25:18 -07:00
Leonardo de Moura
8907dd5b91
refactor(frontends/lean): minimize the use of 'set_tag'
2014-10-15 13:17:09 -07:00
Leonardo de Moura
814778abb1
refactor(kernel/expr): tag expressions at "creation" time
2014-10-15 13:12:09 -07:00
Leonardo de Moura
d960c1994e
refactor(library/tactic/apply_tactic): reuse type_checker object
2014-10-15 09:28:01 -07:00
Leonardo de Moura
bbe4017790
refactor(library/tactic/apply_tactic): remove dead code
2014-10-15 09:15:11 -07:00
Leonardo de Moura
b94d121580
refactor(library): move flycheck "helper" classes to separate module
2014-10-15 09:08:04 -07:00
Soonho Kong
9a6e18ad2a
fix(style): remove "using namespace emscripten"
2014-10-14 21:09:33 -07:00
Soonho Kong
4143716311
fix(emacs/lean-util): fix lean-path-list to only include existing dirs
...
Fix #246
2014-10-14 20:48:56 -07:00
Soonho Kong
1915674b4d
feat(CMakeLists.txt): support emscripten
2014-10-14 18:59:15 -07:00
Soonho Kong
e75c9fe9fc
feat(shell/lean.cpp): expose functions to javascript side
...
lean_init, lean_import_module, lean_process_file
2014-10-14 18:59:15 -07:00
Soonho Kong
e99463980a
feat(util/lean_path.cpp): use '/library' as LEAN_PATH for emscripten
2014-10-14 18:59:15 -07:00
Leonardo de Moura
e6606ef2ac
feat(library/tactic): add 'rename' hypothesis tactic
2014-10-14 18:19:34 -07:00
Leonardo de Moura
fc01edee4d
fix(frontends/lean/elaborator): perform translation using "user-level" names
2014-10-14 17:53:24 -07:00
Leonardo de Moura
90dba868e3
feat(library/tactic/proof_state): apply substitutions when pretty printing state
2014-10-14 17:37:20 -07:00
Leonardo de Moura
58c9421bab
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44 , fixes #70
2014-10-14 17:18:40 -07:00
Soonho Kong
0f5d88517d
chore(library/rewriter): remove lean-0.1 files
2014-10-14 16:03:34 -07:00
Leonardo de Moura
5ff200c516
chore(library/simplifier): delete old simplifier
...
This was the simplifier used in Lean 0.1.
2014-10-14 15:56:09 -07:00
Leonardo de Moura
de7c850782
feat(kernel/converter): relax is_def_eq test for local constants and meta-variables
2014-10-14 15:31:57 -07:00
Leonardo de Moura
940092a975
fix(kernel/constraint): bug in operator<<
2014-10-14 15:22:03 -07:00
Leonardo de Moura
a30232b99a
fix(library/module): race condition on m_imported
2014-10-14 15:19:50 -07:00
Soonho Kong
343a9a690e
feat(emacs/lean-type): add lean-show-type-add-to-kill-ring option
...
If a customization option 'lean-show-type-add-to-kill-ring' is non-nil
and a user runs 'lean-show-type' by explicitly typing 'C-c C-t',
lean-mode saves the displayed type information message into kill-ring
, which can be pasted by yank (C-y) command.
Close #245
2014-10-14 09:27:25 -07:00
Leonardo de Moura
7231aa0d73
fix(library/module): allow multiple calls to import_modules with the same modules
...
The idea is to store a set of already imported files.
This feature is useful when using the import_modules API directly (e.g.,
from javascript).
2014-10-14 08:13:41 -07:00
Leonardo de Moura
d75a9c840c
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
2014-10-13 21:08:36 -07:00
Leonardo de Moura
b7c1b348d1
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
2014-10-13 20:53:09 -07:00
Leonardo de Moura
9edf780a00
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem
2014-10-13 18:35:11 -07:00
Leonardo de Moura
2431de542f
refactor(frontends/lean/parser): add missing 'const'
2014-10-13 13:07:42 -07:00
Leonardo de Moura
7d0db4cc60
feat(library/kernel_serializer): compress binder modifier annotations when saving .olean file
2014-10-13 10:14:56 -07:00
Leonardo de Moura
bc70e7244d
feat(frontends/lean): add option '-X': discard all proofs after theorems are checked
...
This option is useful for generating compact .olean files for web demos
2014-10-13 10:05:38 -07:00
Leonardo de Moura
698dc0472d
fix(frontends/lean/decl_cmds): error messages
2014-10-13 07:17:33 -07:00
Leonardo de Moura
ab90a350b3
fix(emacs/lean-syntax): syntax highlight for declarations with explicit universes
2014-10-13 06:52:36 -07:00
Leonardo de Moura
a26618e0f2
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
2014-10-12 13:06:00 -07:00
Leonardo de Moura
549f24335e
feat(frontends/lean): do not allow coercion definition in sections
2014-10-11 18:41:17 -07:00
Leonardo de Moura
78b8a67015
refactor(library/scoped_ext): sections are just "nameless" namespaces
2014-10-11 17:36:46 -07:00
Leonardo de Moura
158682219f
feat(frontends/lean): allow parameters only in contexts
2014-10-11 17:13:56 -07:00
Leonardo de Moura
f984b51291
feat(frontends/lean/notation_cmd): remove the cleanup notation hack
2014-10-11 16:40:26 -07:00
Leonardo de Moura
334a4c84d1
refactor(frontends/lean): do not expose unnecessary functions
2014-10-11 16:40:26 -07:00
Leonardo de Moura
33ad41b93e
refactor(frontends/lean): adjust function names to reflect how parameters/variables behave
2014-10-11 15:33:31 -07:00
Leonardo de Moura
ca632cca13
feat(frontends/lean): add 'universe variable' command
...
We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature
```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```
The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
2014-10-11 14:22:33 -07:00
Leonardo de Moura
6a40f80612
fix(emacs/lean-syntax): glitch on syntax highlight
2014-10-11 10:56:28 -07:00
Leonardo de Moura
1cc8007b9a
refactor(frontends/lean): rename parser methods is_section* to is_local*
2014-10-11 10:25:39 -07:00
Leonardo de Moura
b0f8d86f26
feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242
2014-10-10 18:08:03 -07:00
Leonardo de Moura
5e6ff3eef3
fix(frontends/lean/elaborator): bug when reporting error position
2014-10-10 17:31:12 -07:00
Leonardo de Moura
f0523a3465
feat(frontends/lean): namespaces also define scope for variables
2014-10-10 16:21:30 -07:00
Leonardo de Moura
0641ee33ce
feat(frontends/lean): allow variables anywhere
2014-10-10 16:16:19 -07:00
Leonardo de Moura
4010767c20
feat(shell): add options --cpp and --discard
2014-10-10 15:55:08 -07:00
Leonardo de Moura
3d65b1c25c
fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241
2014-10-10 15:41:55 -07:00
Leonardo de Moura
d61e6fdd89
refactor(frontends/lean/util): add auxiliary function
2014-10-10 15:21:08 -07:00
Leonardo de Moura
235b8975d2
feat(kernel/inductive): K-like reduction in the kernel
...
Given (H_1 : a = a), we have that
eq.rec H_2 H_1
reduces to H_2
This is not exclusive to equality.
It applies to any inductive datatype in Prop, containing only one
constructor with zero "arguments" (we say they are nullary).
BTW, the restriction to only one constructor is not needed, but it is
does not buy much to support multiple nullary constructors since Prop is
proof irrelevant.
2014-10-10 14:37:45 -07:00
Leonardo de Moura
5a71542aeb
feat(kernel/inductive): track when K-like reduction can be used
2014-10-10 08:50:24 -07:00
Leonardo de Moura
402a351937
feat(frontends/lean): add 'universes' command
2014-10-10 08:45:59 -07:00
Leonardo de Moura
9ba59c6b25
feat(library/universe): improve support for universe level constraints in the unifier
2014-10-09 20:28:39 -07:00
Leonardo de Moura
052bc6ff20
fix(frontends/lean/elaborator): better specific universe detection
2014-10-09 14:43:07 -07:00
Floris van Doorn
1612070350
feat(lean-input.el): add some new notation
2014-10-08 23:14:44 -07:00
Leonardo de Moura
8947bf4347
feat(frontends/lean): display type of binders, closes #238
2014-10-08 22:54:10 -07:00
Leonardo de Moura
25fd370c51
fix(frontends/lean): bug when using nested sections and parameters
...
see tests/lean/run/section4.lean
2014-10-08 22:23:20 -07:00
Leonardo de Moura
f7bbe09db2
feat(frontends/lean): add helper function mk_section_local_ref
2014-10-08 22:23:20 -07:00
Leonardo de Moura
d445857f56
fix(frontends/lean): change how "as-is" expressions are handled
...
Implicit arguments are consumed.
2014-10-08 22:23:20 -07:00
Leonardo de Moura
86410d392b
feat(util/list_fn): generalize map_filter template
2014-10-08 22:23:20 -07:00
Leonardo de Moura
0651496bf6
refactor(frontends/lean/notation_cmd): remove unnecessary uses of add_local_expr
2014-10-08 22:23:20 -07:00
Leonardo de Moura
57c85221fe
fix(frontends/lean): collect used universe levels after elaboration in the check command
2014-10-08 22:23:19 -07:00
Leonardo de Moura
eab9321a3b
fix(frontends/lean): make all variables/parameters visible for 'variables' command
2014-10-08 22:23:19 -07:00
Leonardo de Moura
93e0599a0f
feat(kernel/level): add missing normalization rule
2014-10-08 22:23:19 -07:00
Soonho Kong
24227f0e51
feat(emacs/lean-settings): enable linja '--keep-going' option
...
Fix #234
2014-10-08 13:12:16 -07:00
Soonho Kong
b6d475c3ac
fix(emacs/lean-project): use better prompt message for lean-project-create
2014-10-08 13:04:31 -07:00
Soonho Kong
d542771ba1
doc(emacs/README.md): add 'Unicode' subsection in 'Known Issues' section
2014-10-08 10:43:58 -07:00
Soonho Kong
8c0f01ac34
doc(emacs/README.md): do package-refresh-contents only once
...
Close #233
2014-10-08 10:41:52 -07:00
Leonardo de Moura
3b23bec25b
feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231
2014-10-08 08:40:55 -07:00
Leonardo de Moura
5b9bd279af
chore(frontends/lean/parser): minor cleanup
2014-10-08 08:40:55 -07:00
Leonardo de Moura
744cee8dd8
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228
2014-10-07 18:02:15 -07:00
Leonardo de Moura
d8572e249d
feat(frontends/lean/builtin_cmds): add 'print classes' command
2014-10-07 17:30:57 -07:00
Leonardo de Moura
c31c026f46
feat(frontends/lean/class): accept only inductive datatypes (and records) as classes
2014-10-07 17:30:57 -07:00
Leonardo de Moura
8fa171cb92
refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument
2014-10-07 17:30:57 -07:00
Soonho Kong
826166c257
feat(CMakeLists.txt): use bin/package_version if needed
...
1) When git sha1 is available:
Lean (version 0.2.0, commit 4a119a0424Close #229
2014-10-07 16:58:44 -07:00
Leonardo de Moura
92c424936a
refactor(kernel/macro_definition_cell): improve macro get_type API
2014-10-07 16:38:31 -07:00
Leonardo de Moura
16041e4948
fix(frontends/lean/elaborator): 'as-is' expressions
...
The elaborator should not introduce implicit arguments on terms marked
as 'as-is'.
2014-10-07 16:38:31 -07:00
Soonho Kong
78e9854bae
fix(emacs): support tabs in a file
...
Fix #226
2014-10-07 14:42:35 -07:00
Soonho Kong
e40ef9f6c5
feat(util/lean_path.cpp): add "exe_path/../lib/lean" to LEAN_PATH
...
Related issue: #223
2014-10-07 13:38:23 -07:00
Soonho Kong
d5abaf6446
feat(CMakeLists.txt): install lean library to LIBRARY_DIR (default: lib/lean)
2014-10-07 12:30:39 -07:00
Soonho Kong
013cd5640e
fix(CMakeLists.txt): rename EMACS_LIB to EMACS_LISP_DIR (default: share/eamcs/site-lisp/lean)
2014-10-07 12:30:39 -07:00
Soonho Kong
103cf57a46
chore(CMakeLists.txt): standard_lib target generates TAGS for library
2014-10-07 12:30:39 -07:00
Soonho Kong
2cf6cf19c0
feat(src): add LEAN_VERSION_PATCH
2014-10-07 12:30:38 -07:00
Soonho Kong
900c7c41a1
fix(shell/lean.cpp): print git commit in version string only when it's available
2014-10-07 12:30:38 -07:00
Leonardo de Moura
531de7990d
refactor(frontends/lean/tactic_hint): simplify tactic_hints
2014-10-07 11:34:58 -07:00
Leonardo de Moura
90ece4dd1b
feat(frontends/lean): remove tactic hints for specific classes
...
The idea is to separate class-instance resolution and tactic framework
as two independent engines.
2014-10-07 09:44:01 -07:00
Leonardo de Moura
dc0e6861b7
fix(emacs/lean-mode): wrong pp highlighting, fixes #225
2014-10-07 02:32:59 -07:00
Soonho Kong
39645390ff
chore(util/*): add cstddef header before including gmp.h/mpfr.h
...
Reference: https://gcc.gnu.org/gcc-4.9/porting_to.html
------
Header <cstddef> changes
The <cstddef> header was updated for C++11 support and this breaks some
libraries which misuse macros meant for internal use by GCC only. For
instance with GMP versions up to 5.1.3, you may see:
/usr/include/c++/4.9.0/cstddef:51:11: error: ‘::max_align_t’ has not been declared
using ::max_align_t;
^
Another possible error is:
someheader.h:99:13: error: ‘ptrdiff_t’ does not name a type
A workaround until libraries get updated is to include <cstddef> or
<stddef.h> before any headers from that library.
2014-10-07 02:36:57 -04:00
Soonho Kong
286aae933c
chore(CMakeLists.txt): add EMACS_LIB option to specify installation path for emacs stuff
2014-10-06 11:20:13 -07:00
Leonardo de Moura
dc92f67588
feat(frontends/lean/server): CLEAR_CACHE forces buffer to be reprocessed
2014-10-06 08:42:20 -07:00
Leonardo de Moura
16562adb87
feat(frontends/lean): add 'coercions' and 'instances' to 'print' command, closes #71
2014-10-05 18:50:48 -07:00
Leonardo de Moura
1306d08399
feat(emacs/lean-input): add shortcuts for subscripts
2014-10-05 13:34:05 -07:00
Leonardo de Moura
60d8369688
fix(library/unifier): missing justification when updating choice constraints
...
The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out
2014-10-04 10:40:53 -07:00
Leonardo de Moura
a9741c5c30
chore(frontends/lean/placeholder_elaborator): indent code
2014-10-04 10:36:10 -07:00
Leonardo de Moura
0a288aec40
chore(frontends/lean/proof_qed_elaborator): remove obsolete comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-04 09:19:33 -07:00
Leonardo de Moura
64f6601fe3
fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost
2014-10-04 09:15:42 -07:00
Leonardo de Moura
bf01cfeec5
fix(frontends/lean): avoid superfluous local references of the form @-1 (@ f),
...
This kind of term also confuses the elaborator
2014-10-04 07:55:32 -07:00
Leonardo de Moura
e71d4548de
fix(frontends/lean): universe levels associated with section variables should not be fixed in the section
2014-10-04 07:13:19 -07:00
Leonardo de Moura
b9e7fecb1f
fix(frontends/lean/elaborator): style
2014-10-03 16:26:28 -07:00
Leonardo de Moura
a1bb6d6017
refactor(frontends/lean/elaborator): expose elaborator class
2014-10-03 16:10:36 -07:00
Leonardo de Moura
dccf8a3a75
chore(frontends/lean/elaborator): fix field name
2014-10-03 15:34:23 -07:00
Leonardo de Moura
938e12baa1
feat(frontends/lean/notation_cmd): allow local numeric notation
2014-10-03 13:55:57 -07:00
Leonardo de Moura
dbb7f834af
refactor(frontends/lean/parser_config): merge notation_ext and mpz_notation_ext
2014-10-03 13:55:57 -07:00
Leonardo de Moura
73eca1ef44
feat(frontends/lean/notation_cmd): notation defined in context overrides existing ones
2014-10-03 13:55:57 -07:00
Soonho Kong
7ea9c32ec8
feat(emacs/lean-server): send SYNC command when visiting a modified buffer
...
Close #201
2014-10-03 10:11:21 -07:00
Soonho Kong
b78043ae24
feat(emacs/lean-mode): add 'clean-cache' to the menu
...
Related issue: #75
2014-10-03 10:11:21 -07:00
Soonho Kong
fffb4e6019
feat(emacs/lean-server): delete cache file (.clean) after visit/load
...
fix #75
2014-10-03 10:11:21 -07:00
Soonho Kong
e255b02fca
fix(emacs/lean-changes): visit file before process any changes
...
This solves many instances of the modified buffer problem.
2014-10-03 10:11:21 -07:00
Leonardo de Moura
c0725d1934
refactor(frontends/lean): remove 'including' expressions
2014-10-03 09:09:27 -07:00
Leonardo de Moura
01d4644026
fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored
2014-10-03 08:52:35 -07:00
Leonardo de Moura
284f300440
feat(frontends/lean): add 'include' and 'omit' commands, closes #184
2014-10-03 07:23:24 -07:00
Leonardo de Moura
6950b4aa9b
fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables
2014-10-02 18:29:41 -07:00
Leonardo de Moura
d5cad765a0
feat(frontends/lean): enforce new semantics for section 'variables'
...
The library file logic/core/connectives uses the new feature.
2014-10-02 17:55:34 -07:00
Leonardo de Moura
f006d93794
feat(frontends/lean): section variables occur after section parameters
2014-10-02 17:55:34 -07:00
Leonardo de Moura
0a13e7863a
feat(frontends/lean): enforce rule section parameters cannot depend on section variables
2014-10-02 17:55:34 -07:00
Leonardo de Moura
bf081ed431
refactor(kernel): rename var_decl to constant_assumption
...
Motivation: it matches the notation used to declare it.
2014-10-02 17:55:34 -07:00
Leonardo de Moura
4946f55290
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-02 17:55:34 -07:00
Soonho Kong
91f789c3db
feat(emacs/lean-cmd): add SYNC command
2014-10-02 17:30:03 -07:00
Soonho Kong
5e551db9be
chore(CMakeLists.txt): use $PYTHON_EXECUTABLE instead of "python"
2014-10-02 17:25:13 -07:00
Leonardo de Moura
f78d831de3
refactor(frontends/lean): remove hardcoded Type', and define it using notation
2014-10-02 14:29:51 -07:00
Leonardo de Moura
4cb54ac825
feat(frontends/lean/elaborator): more strict test for bad universe solution
2014-10-02 14:29:51 -07:00
Leonardo de Moura
98e66586e9
feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit
2014-10-02 14:29:51 -07:00
Leonardo de Moura
db9671d7c3
fix(frontends/lean/decl_cmds): remove assertion that does not hold anymore
2014-10-02 09:19:40 -07:00
Leonardo de Moura
9a75298892
feat(emacs): highlight Type'
2014-10-02 08:04:00 -07:00
Leonardo de Moura
5bd8e9d141
fix(frontends/lean/decl_cmds): allow private transparent definitions
...
Example:
section
universe l
private definition T := Type.{max 1 l}
...
end
2014-10-02 07:56:01 -07:00
Leonardo de Moura
153e3927ac
feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type.
2014-10-01 18:50:17 -07:00
Leonardo de Moura
ead827d6b7
feat(frontends/lean): add ! operator the "dual" of @, closes #220
2014-10-01 17:13:41 -07:00
Soonho Kong
72beb438e6
fix(emacs/lean-server): merge server-trace-mode to debug-mode
2014-10-01 14:38:23 -07:00
Leonardo de Moura
c46ec6a548
fix(frontends/lean): missing type information for INFO, fixes #218
2014-10-01 14:29:07 -07:00
Leonardo de Moura
f863d82e69
fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216
2014-10-01 11:24:45 -07:00
Leonardo de Moura
966366e18e
feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes #217
2014-10-01 10:56:05 -07:00
Leonardo de Moura
263b081e69
fix(frontends/lean/inductive_cmd): temporary aliases must take explicit universes into account, fixes #215
2014-10-01 10:24:44 -07:00
Leonardo de Moura
71077f5c89
feat(frontends/lean/parser): allow _ at level expressions
2014-10-01 10:24:44 -07:00
Soonho Kong
3775d07d5f
fix(emacs/lean-company): use lean-grab-hname for findp auto-completion
...
fix #214
2014-10-01 09:53:48 -07:00
Leonardo de Moura
2730e5163e
feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message
...
See new test for explanation.
2014-09-30 18:04:04 -07:00
Soonho Kong
89a929e9cd
feat(emacs/lean-syntax): add more word constituents to syntax table
2014-09-30 15:41:18 -07:00
Soonho Kong
9024cb23fd
fix(emacs/lean-util): fix lean-grab-id
2014-09-30 15:41:16 -07:00
Soonho Kong
d5e77c05cb
fix(emacs/lean-flycheck): fix error/warning pattern to work on windows
2014-09-30 15:40:57 -07:00
Soonho Kong
41acc10d49
feat(emacs/lean-flycheck): detect and use flycheck error buffer width
...
Detect the width of flycheck error list buffer and set pp.width when
calling flycheck. It uses the same heuristic that `split-window-sensibly`
function is using.
A user can also set `lean-flycheck-msg-width` custom variable to enforce
a certain width.
Close #205 .
2014-09-30 05:54:46 -07:00
Leonardo de Moura
486839881c
feat(*): use environment fingerprint to detect when the cache cannot be used because the configuration changed, closes #75
...
We are not taking into the account the options object yet.
2014-09-29 18:30:00 -07:00
Leonardo de Moura
19dec32844
feat(library): add environment fingerprint
2014-09-29 18:30:00 -07:00
Leonardo de Moura
530997638a
feat(library/definition_cache): store the hashcode of direct dependencies
...
Actually we store the has code of their types.
2014-09-29 18:30:00 -07:00
Soonho Kong
b538b3e0bf
fix(emacs/lean-company): handle singleton candidate case
...
If we have a singleton auto-complete candidate (e.g. proof_irrel) and it
does not matched with input prefix (e.g. foo), we add the input
prefix (foo) as an extra candidate to prevent the
candidate (proof_irrel) from being automatically selected and completed.
2014-09-29 17:06:01 -07:00
Leonardo de Moura
113879a7dd
feat(frontends/lean/server): sort exact matches by size in FINDP
2014-09-29 16:44:55 -07:00
Leonardo de Moura
334977b8bd
fix(frontends/lean/info_manager): crash when accessing INFO in the end of the file
2014-09-29 16:44:55 -07:00
Leonardo de Moura
a0c37b231f
feat(kernel/expr): add hash_bi function that takes binder information into account
2014-09-29 16:44:55 -07:00
Soonho Kong
7ab8b8acb7
fix(emacs/lean-company): respect lean syntax to extract findp prefix
...
close #207
2014-09-29 16:00:00 -07:00
Leonardo de Moura
0d6d746d98
feat(frontends/lean): check modification time of imported files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-29 15:17:27 -07:00
Soonho Kong
6c2e576dff
fix(emacs/lean-mode): trigger eri-indent only at the beginning of line
2014-09-29 12:53:22 -07:00
Leonardo de Moura
1a1e9a2340
feat(build): add 'CONSERVE_MEMORY' cmake option
...
When CONSERVE_MEMORY=ON and gcc is being used, we provide additional
command line options that will minimize the amount of memory used by gcc
when compiling Lean.
This is an attempt to fix the "out-of-memory" failures when building
Lean at Travis.
2014-09-29 12:44:29 -07:00
Leonardo de Moura
6630ed8165
fix(frontends/lean/decl_cmds): warning message when compiling with clang++
2014-09-29 12:34:00 -07:00
Soonho Kong
f7ab2f7903
feat(emacs/lean-company): add auto-completion for option names
2014-09-29 12:32:46 -07:00
Soonho Kong
51a0d154d1
fix(emacs/lean-company): always allow typing for FIND_P
2014-09-29 12:32:46 -07:00
Soonho Kong
106399179f
fix(emacs/lean-syntax): use word-boundary instead of symbol-boundary
2014-09-29 12:32:46 -07:00
Leonardo de Moura
21be308884
feat(frontends/lean/inductive_cmd): infer implicit argument annotation after elaboration, allow user to disable it by using '()' annotation, closes #210
2014-09-29 11:11:17 -07:00
Leonardo de Moura
9c55bbb871
feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208
2014-09-29 08:18:10 -07:00
Leonardo de Moura
fbbd1d25cd
chore(frontends/lean/decl_cmds): disable incorrect warning message produced by gcc
2014-09-28 12:32:47 -07:00
Leonardo de Moura
397395bbc9
feat(frontends/lean): allow user to associate priorities to class-instances, closes #180
2014-09-28 12:20:42 -07:00
Leonardo de Moura
9f6a8827e0
refactor(*): use name_map
2014-09-28 10:23:11 -07:00
Leonardo de Moura
33fe409dc6
chore(frontends/lean/placeholder_elaborator): cleanup
2014-09-27 22:24:36 -07:00
Leonardo de Moura
22e47430b5
feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore
2014-09-27 21:50:39 -07:00
Leonardo de Moura
e40f8ffe57
fix(util/sexpr/option_declarations): default value in help message, fixes #212
2014-09-27 10:12:59 -07:00
Leonardo de Moura
8e7aac1eb4
fix(frontends/lean): add 'eval' command
2014-09-26 20:16:03 -07:00
Leonardo de Moura
23960da532
feat(emacs/lean-input): shortcut for long arrow
2014-09-26 17:50:33 -07:00
Leonardo de Moura
69f50adb2e
fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209
2014-09-26 15:36:47 -07:00
Leonardo de Moura
a3e38dc8a0
feat(frontends/lean): allow users to define "numeral notation"
2014-09-26 14:55:23 -07:00
Leonardo de Moura
9928390605
fix(library/match): memory leak that only happens with compiling with clang++
2014-09-26 10:24:38 -07:00
Leonardo de Moura
6bf905aea8
fix(frontends/lean/pp): do not invoke type checker on expressions
...
containing free variables.
This could happened when the pretty printer was used from Lua to print
nested subterms
2014-09-26 09:38:36 -07:00
Leonardo de Moura
8143b51c7e
feat(build): add 'CROSS_COMPILE' cmake option
...
When CROSS_COMPILE=ON, the Lean standard library will not be compiled.
2014-09-26 09:26:40 -07:00
Leonardo de Moura
480bc639ea
feat(build): add IGNORE_SORRY cmake option
...
It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
2014-09-26 08:55:54 -07:00
Leonardo de Moura
f05bb9daeb
fix(util/memory): warning when compiling with clang++
2014-09-26 08:42:47 -07:00
Soonho Kong
4b60499f7d
fix(emacs/lean-company): take out '@' from prefix for findp
...
fix #207
2014-09-26 08:53:48 +02:00
Leonardo de Moura
d02ab15c88
fix(frontends/lean/proof_qed_elaborator): must also create
...
metavar_closure before solving nested proof_qed
The bug was exposed by the new policy for handling class-instance
resolution. In the new policy, we reject partial solutions.
The bug fixed in this commit was being masked by a partial solution that
was being "completed" later.
2014-09-25 20:07:51 -07:00
Leonardo de Moura
c775da16ec
feat(frontends/lean/elaborator): discard partial solution during
...
class-instance resolution, use only tactic_hints associated with
classes, enforce is_strict
2014-09-25 19:46:08 -07:00
Leonardo de Moura
318fec43a4
feat(frontends/lean/elaborator): use tactic_hints for unsolved placeholders
2014-09-25 17:54:10 -07:00
Leonardo de Moura
bb1c6d44ac
fix(frontends/lean/elaborator): missing register_meta
2014-09-25 17:52:36 -07:00
Leonardo de Moura
bcb30f6232
fix(frontends/lean/placeholder_elaborator): missing 'return'
2014-09-25 15:00:06 -07:00
Leonardo de Moura
03f71c73dc
perf(kernel/instantiate): cache result of instantiate_type_univ_params
...
and instantiate_value_univ_params
2014-09-25 13:24:43 -07:00
Leonardo de Moura
23ddacad19
perf(frontends/lean/class): improve is_ext_class procedure
2014-09-25 12:26:09 -07:00
Leonardo de Moura
28796593e3
fix(kernel/type_checker): bug in new is_opaque method
2014-09-25 12:24:14 -07:00
Leonardo de Moura
1d92097781
refactor(kernel/declaration): return reference to type/value/name
2014-09-25 12:17:04 -07:00
Leonardo de Moura
d4236e40b4
feat(kernel/type_checker): expose is_opaque
2014-09-25 11:19:54 -07:00
Leonardo de Moura
8747f12118
refactor(frontends/lean/elaborator): remove unnecessary
...
set_local_context_for method
2014-09-25 10:21:31 -07:00
Leonardo de Moura
b8eb65aac2
perf(frontends/lean/placeholder_elaborator): reuse local_context, this
...
is possible now because local_context is a mainly "functional object"
2014-09-25 10:11:41 -07:00
Leonardo de Moura
2e2d2d21f1
refactor(local_context): local_context::scope auxiliary object is not
...
needed anymore
2014-09-25 09:59:27 -07:00
Leonardo de Moura
cd87539de5
fix(library/unifier): bug in the new next_delta_unfold_case_split
2014-09-25 09:56:32 -07:00
Leonardo de Moura
09162e5fea
refactor(frontends/lean/local_context): remove name_generator from local_context
2014-09-25 09:44:34 -07:00
Leonardo de Moura
354c456639
refactor(frontends/lean/local_context): move mvar2meta mapping to elaborator
2014-09-25 09:31:03 -07:00
Leonardo de Moura
fce1113b80
refactor(frontends/lean/coercion_elaborator): simplify
...
coercion_elaborator interface
2014-09-25 08:48:31 -07:00
Leonardo de Moura
a61b95a87e
refactor(frontends/lean/proof_qed_elaborator): simplify
...
proof_qed_elaborator interface
2014-09-25 08:38:02 -07:00
Leonardo de Moura
18cfce60b9
refactor(frontends/lean/local_context): simplify local_context representation
2014-09-25 08:13:27 -07:00
Leonardo de Moura
0488ee4ee2
perf(library/unifier): process delta expansion case split lazily
2014-09-24 19:16:12 -07:00
Leonardo de Moura
d4c0c01e0b
fix(build): add missing file
2014-09-24 12:54:17 -07:00
Leonardo de Moura
516c0c73b9
refactor(*): remove dependency to thread_local C++11 keyword, the
...
current compilers have several bugs associated with it
We use the simpler __thread (gcc and clang) and
__declspec(thread) (visual studio).
2014-09-24 12:51:04 -07:00
Leonardo de Moura
ca1b8ca80f
refactor(util/memory_pool): simplify memory_pool, it is not a template anymore
2014-09-24 10:48:32 -07:00
Leonardo de Moura
41433a4002
refactor(util/rb_tree): remove optimization that creates problems for
...
some compilers
2014-09-24 10:33:25 -07:00
Leonardo de Moura
9b61b18eaa
perf(kernel/replace_visitor): use more expensive/precise cache
...
It does not use pointer equality, but structural equality
2014-09-24 10:12:29 -07:00
Leonardo de Moura
5489e46ce5
refactor(util/numerics): explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
4205368718
fix(util/sexpr): missing explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
7e84d5df3d
refactor(util): explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
8466115665
fix(frontends/lean/class): missing explicit initialization/finalization
2014-09-24 10:12:29 -07:00
Leonardo de Moura
dbe1763b1a
refactor(frontends/lean/server): explicit initialization/finalization
2014-09-24 10:12:29 -07:00
