Leonardo de Moura
2c926478dd
feat(bin): add leanemacs startup script
2015-01-30 13:05:30 -08:00
Leonardo de Moura
9910547913
feat(emacs): add script for loading lean mode and its dependencies
2015-01-30 13:05:30 -08:00
Leonardo de Moura
a57251913a
feat(emacs): assume lua-mode and mmm-mode are available
2015-01-30 13:05:30 -08:00
Leonardo de Moura
d0ce4cf62f
fix(CMakeLists.txt): path to ninja
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 10:37:49 -08:00
Leonardo de Moura
a44fec6eb4
fix(CMakeLists.txt): path to ninja
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 10:32:35 -08:00
Leonardo de Moura
1ee52a3ddc
feat(CMakeLists.txt): include ninja in Windows binary distribution package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-30 09:59:55 -08:00
Leonardo de Moura
7c59c959db
fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms"
2015-01-30 09:52:42 -08:00
Soonho Kong
d98f04fd3a
chore(emacs/README.md): add numbering on configuration
...
[skip ci]
2015-01-30 03:08:11 -05:00
Soonho Kong
04249a292c
feat(emacs/README.md): add per-installation-method configurations
2015-01-30 03:05:35 -05:00
Soonho Kong
ce0aed12ec
fix(emacs/Cask): add GNU package repository
...
Related issue #410
2015-01-30 02:52:55 -05:00
Soonho Kong
d69505a092
doc(emacs/README.md): add GNU package repository
...
flycheck uses let-alist package which is in GNU repository. @awody reported a problem and I hope that this can help (I'll test it later).
Reference: https://github.com/flycheck/flycheck/issues/551
Related issue: #410
2015-01-30 02:52:05 -05:00
Leonardo de Moura
f04e462bf3
test(tests/lean/interactive): add more tests for lean server
2015-01-29 16:30:07 -08:00
Leonardo de Moura
e9e1f86b7f
fix(library/app_builder): many bugs, add use_cache option, add tests
2015-01-29 15:30:31 -08:00
Leonardo de Moura
e6f022e3f2
fix(library/match): index out of bounds
2015-01-29 14:41:38 -08:00
Leonardo de Moura
b5d1f4e54c
feat(library/match): add low-level match API
2015-01-29 14:09:09 -08:00
Leonardo de Moura
f587cc3e1d
feat(library/app_builder): expose app_builder API in Lua
2015-01-29 11:38:56 -08:00
Leonardo de Moura
5efd91e435
fix(library/app_builder): missing initialization
2015-01-29 11:38:28 -08:00
Leonardo de Moura
5bb2a41c64
feat(library/reducible): expose Lua API for reducible hints
2015-01-29 10:37:15 -08:00
Leonardo de Moura
4cf2dcaa7e
feat(library/app_builder): add helper class for creating applications efficiently using type inference
...
The idea is to use this class in the simplifier.
For example, we will use to create: symmetry, reflexivity, transitivity
and congruence proof steps.
2015-01-28 18:40:21 -08:00
Leonardo de Moura
4e08cc0659
feat(library/match): add flag for tracking whether matcher assigned anything
2015-01-28 18:39:50 -08:00
Leonardo de Moura
dbc8e9e13a
refactor(*): add method get_num_univ_params
2015-01-28 17:22:18 -08:00
Leonardo de Moura
5aaade47d8
feat(library/match): add new API
2015-01-28 16:42:42 -08:00
Leonardo de Moura
e4b5e07498
fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics
...
closes #415
2015-01-28 13:32:56 -08:00
Leonardo de Moura
1119a8018a
fix(util/buffer): destructor was not being invoked at erase and erase_elem
...
This bug was producing a weird memory leak in the definition package.
The methods erase and erase_elem are not used very often. This is why
this bug was never detected.
2015-01-27 18:48:02 -08:00
Leonardo de Moura
ad4c7c20f9
fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term
2015-01-27 11:22:14 -08:00
Leonardo de Moura
1dbe4b8fb7
feat(kernel/extension_context): add auxiliary method is_def_eq
2015-01-27 11:17:54 -08:00
Leonardo de Moura
2a5658ebe2
fix(frontends/lean/elaborator_context): memory leak
2015-01-26 16:08:51 -08:00
Leonardo de Moura
e2c41fca75
feat(frontends/lean): modify syntax for local notation
...
The idea is to make it uniform with the syntax for defining local
attributes.
2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed
feat(frontends/lean): 'attribute' command is persistent by default
2015-01-26 11:51:17 -08:00
Leonardo de Moura
a1eeb0a6a1
fix(library/print): typo in is_used_name
...
closes #408
2015-01-25 08:58:08 -08:00
Leonardo de Moura
4f2e0c6d7f
refactor(frontends/lean): add 'attribute' command
...
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
2015-01-24 20:23:21 -08:00
Leonardo de Moura
b5c4e603db
feat(frontends/lean): allow parameters to be used in sections
...
Restriction:
- coercions and notations cannot be defined in parametric sections
closes #401
2015-01-23 17:42:19 -08:00
Leonardo de Moura
27f6bfd3f0
refactor(*): add file constants.txt with all constants used by the Lean binary
2015-01-23 16:50:32 -08:00
2d69444da5
fix(cmake/Modules/cpplint.py): python3 compatible without six
2015-01-22 13:05:56 -08:00
c1bfafd2a7
style(cmake/Modules/cpplint.py)
2015-01-22 13:05:56 -08:00
a2f30322a9
fix(cmake/Modules/cpplint.py): delete ending colon
...
Delete the erroneous ending colon.
2015-01-22 13:05:56 -08:00
51c771f334
revert(cmake/Modules/cpplint.py): roll back to python2 version
...
This reverts commit 65cc4d3c08
.
2015-01-22 13:05:42 -08:00
Leonardo de Moura
880faf89e0
feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command
...
closes #354
2015-01-21 18:12:29 -08:00
Leonardo de Moura
a53098385c
refactor(frontends/lean/type_util): move infer_implicit_params to library
2015-01-21 17:22:41 -08:00
Soonho Kong
65cc4d3c08
fix(cmake/Modules/cpplint.py): roll back to python2 version
2015-01-21 19:26:38 -05:00
Leonardo de Moura
12674114a4
feat(shell): set default behavior to "trusted"
...
closes #402
2015-01-21 16:25:09 -08:00
073c1d1c31
feat(python): add python 3 compatibility
...
Add Python 3 compatibility through python-six library.
Closes #393 .
2015-01-21 17:13:55 -05:00
Leonardo de Moura
1d6ff5f761
feat(library/definitional/projection): throw exception if unsupported case occurs
...
The user can workaround it by using trust-level 0 (i.e., no option -t num or -T)
2015-01-20 17:42:34 -08:00
Leonardo de Moura
01ce57e52e
feat(library/definitional/projection): add projection macro
2015-01-20 16:21:50 -08:00
Leonardo de Moura
b6750e9d29
feat(library/util): add auxiliary functions
2015-01-20 15:44:58 -08:00
Leonardo de Moura
c51e2ac428
feat(kernel/type_checker): expose get_arity function
2015-01-20 14:25:07 -08:00
Leonardo de Moura
c43b2c8640
feat(kernel/extension_context): add auxiliary methods
2015-01-20 14:23:10 -08:00
Leonardo de Moura
8355ed55d7
refactor(library/definitional/projection): remove dead code
2015-01-20 13:40:09 -08:00
Leonardo de Moura
752b54085b
refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used
...
Now, we unfold untrusted macros outside of the Lean kernel.
2015-01-20 12:36:56 -08:00
Leonardo de Moura
5ab7ff62b5
feat(CMakeLists): add --Trust option when building standard/hott libraries
2015-01-20 11:11:35 -08:00
Leonardo de Moura
260795f981
fix(frontends/lean/structure_cmd): collect universe levels that only occur in structure parameters
...
fixes #395
2015-01-19 22:18:09 -08:00
Leonardo de Moura
002050fa97
feat(frontends/lean): increase binding power of ! and @
...
Remark: I did not add the constant "app".
Reason: It would break the standard library in many places.
Moreover, the current "max" is not just the binding power of
application, but also the binding power of identifiers, (, [, ...
It would be weird to call it "app"
closes #388
2015-01-19 18:40:33 -08:00
Leonardo de Moura
dfbe6662be
feat(frontends/lean/elaborator): add option 'elaborator.fail_if_missing_field'
2015-01-19 17:47:39 -08:00
Leonardo de Moura
2717adde94
feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant
2015-01-19 16:23:29 -08:00
Leonardo de Moura
d0e9e0e21c
feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors
2015-01-18 20:58:40 -08:00
Leonardo de Moura
858d21f20b
feat(library/definitional/projection): store projection information
2015-01-18 16:26:56 -08:00
Soonho Kong
901c9bf67a
refactor: rename ltags => leantags
...
fix #394
2015-01-18 13:44:41 +09:00
Leonardo de Moura
edcc92d9c7
feat(frontends/lean): remove 'using' from structure instance command
2015-01-17 09:38:10 -08:00
Leonardo de Moura
f9d7480f5c
feat(frontends/lean): notation for creating structure instances
2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d
feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields
...
See new test for an example.
closes #371
2015-01-16 13:04:48 -08:00
Leonardo de Moura
13660cfecd
feat(frontends/lean/parser): add parse_qualified_expr
2015-01-16 12:42:42 -08:00
Leonardo de Moura
6c07ca5d41
perf(library/print): improve is_used_name
2015-01-15 19:01:13 -08:00
Leonardo de Moura
c6290f01d0
perf(kernel/free_vars): improve has_free_var
2015-01-15 18:42:56 -08:00
Leonardo de Moura
f397da111a
perf(kernel/error_msgs): avoid unnecessary work
2015-01-15 18:32:52 -08:00
Leonardo de Moura
ce0b1d17a2
perf(kernel/free_vars): improve has_free_var
2015-01-15 18:31:43 -08:00
Leonardo de Moura
ddcc8de09e
fix(shell/lean): catch errors when loading bad cache file
2015-01-15 18:06:22 -08:00
Leonardo de Moura
30817aa2b1
feat(emacs): allow user to provide extra commands to lean-server
2015-01-15 16:54:55 -08:00
Leonardo de Moura
907f90096e
feat(kernel): add memory consumption checks at replace_fn and for_each_fn
2015-01-15 16:54:55 -08:00
Leonardo de Moura
8ab775bd6f
feat(*): distinguish between logical and runtime exceptions.
...
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
2015-01-15 16:54:55 -08:00
Leonardo de Moura
3a865e95fe
feat(shell/lean): add option '-M' to limit amount of memory consumed
2015-01-15 16:54:55 -08:00
Leonardo de Moura
5c9a277dea
feat(CMakeLists): include runtime files in Windows binary distribution package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-14 12:37:25 -08:00
Leonardo de Moura
730e038dd3
feat(CMakeLists): add basic example to binary distribution package
2015-01-14 10:39:07 -08:00
Leonardo de Moura
0509baa64a
feat(CMakeLists): add README file for binary distribution packages
2015-01-14 10:35:51 -08:00
Leonardo de Moura
ee98523c2a
feat(shell/lean): add option '-T' alias for '-t 1025'
2015-01-14 10:21:57 -08:00
Leonardo de Moura
3813aeede5
fix(util/lean_path): relative position of library files in binary
...
distribution packages
2015-01-14 10:14:17 -08:00
Leonardo de Moura
c9132648a2
feat(CMakeLists): include HoTT library in binary package
2015-01-14 10:00:35 -08:00
Leonardo de Moura
ef529c660f
fix(library/definitional/no_confusion): mark no_confusion as reducible
...
Auxiliary definitions should be marked as reducible
2015-01-13 18:44:47 -08:00
Leonardo de Moura
e48df78938
feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs
...
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
2015-01-13 18:05:22 -08:00
Leonardo de Moura
37e852ba61
feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs
2015-01-13 14:38:25 -08:00
Leonardo de Moura
e9338669dc
feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages
2015-01-13 13:30:12 -08:00
Leonardo de Moura
41935906a8
chore(frontends/lean): use update_if_undef
2015-01-13 13:02:14 -08:00
Leonardo de Moura
e5a8c67d22
fix(library/definitional/equations): assertion violation
2015-01-13 11:57:14 -08:00
Leonardo de Moura
1fbfe59a9a
feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line
...
closes #391
2015-01-13 11:14:44 -08:00
Leonardo de Moura
4f519be55e
fix(frontends/lean/elaborator): compilation problem
2015-01-11 20:58:41 -08:00
Leonardo de Moura
75d7e4ab9e
feat(frontends/lean): add 'end' token to match expressions
2015-01-10 12:35:29 -08:00
Leonardo de Moura
5796640392
fix(frontends/lean): do report unassigned metavariables in equation lhs
2015-01-10 10:39:47 -08:00
Leonardo de Moura
b172229a72
feat(frontends/lean): add 'match' expressions
...
We reuse the equations infrastructure to compile them.
2015-01-10 10:11:13 -08:00
Leonardo de Moura
6df9ffe5f6
fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler
2015-01-10 09:18:27 -08:00
Leonardo de Moura
a3bc1b0cd5
fix(library/definitional/equations): add more equation validation to avoid obscure error message
2015-01-09 18:52:21 -08:00
Leonardo de Moura
2e4a2451e6
refactor(library/reducible): simplify reducible/irreducible semantics
2015-01-08 18:52:18 -08:00
Leonardo de Moura
698754b2bb
feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases
2015-01-08 12:00:47 -08:00
Leonardo de Moura
4fef19230d
feat(util/sexpr/options): add update_if_undef method
2015-01-08 11:55:30 -08:00
Leonardo de Moura
f344dd75c4
feat(library/pp_options): add get_pp_purify_locals_name
2015-01-08 11:55:08 -08:00
Leonardo de Moura
87d41e90fc
fix(frontends/lean/decl_cmds): store equations positions
2015-01-07 18:50:56 -08:00
Leonardo de Moura
5c118127ae
fix(library/definitional/equations): memory access violation
2015-01-07 17:06:41 -08:00
Leonardo de Moura
597f7385e8
fix(library/unifier): incorrect fix
2015-01-07 16:57:02 -08:00
Leonardo de Moura
15b5344626
feat(library/definitional/equations): copy tags
2015-01-07 14:00:46 -08:00
Leonardo de Moura
2990a6d029
fix(library/unifier): missing "set_conflict" in process_delta
2015-01-07 12:41:01 -08:00
Leonardo de Moura
a9b6e20a22
fix(frontends/lean): save equations position
2015-01-06 15:55:04 -08:00
Leonardo de Moura
760dc2162a
chore(library/definitional/equations): cleanup
2015-01-06 14:53:21 -08:00
Leonardo de Moura
a3a6697f44
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
2015-01-06 14:07:17 -08:00
Leonardo de Moura
559ee3e3e1
fix(util/buffer): bug in expand method
...
fixes #385
2015-01-06 11:42:40 -08:00
Leonardo de Moura
5f182dc1cc
fix(util/lean_path): memory leak
2015-01-06 10:22:45 -08:00
Leonardo de Moura
c33928f202
fix(library/pp_options): memory leak
2015-01-06 10:22:23 -08:00
Leonardo de Moura
828ce3f8dc
feat(frontends/lean/decl_cmds): minor modifications for supporting mutually recursive functions
2015-01-05 19:23:50 -08:00
Leonardo de Moura
322cdb8a98
feat(library/definitional/equations): add 'equations_result' macro used to wrap multiple functions being defined by recursive equations
...
This is only useful when compiling "mutually recursive" functions.
2015-01-05 19:09:20 -08:00
Leonardo de Moura
3325d791de
fix(library/definitional/equations): bug in recursive application elimination
2015-01-05 17:17:14 -08:00
Leonardo de Moura
eedc31f7e9
fix(library/definitional/equations): bug in "complete" transition
2015-01-05 16:27:29 -08:00
Leonardo de Moura
3889b60152
feat(library/definitional/equations): allow inductive datatype parameters in recursive equations
2015-01-05 15:56:28 -08:00
Leonardo de Moura
6eba4b4ac1
chore(library/definitional/equations): cleanup
2015-01-05 13:57:13 -08:00
Leonardo de Moura
b46c377aa2
feat(library/definitional/equations): add "complete" transition for overlapping patterns
2015-01-05 11:49:27 -08:00
Leonardo de Moura
fdef3e5407
feat(library/definitional/equations): add support for reflexive datatypes in the definitional package
2015-01-05 11:13:35 -08:00
Leonardo de Moura
5e228d92d2
fix(library/definitional/equations): missing case
2015-01-04 20:49:53 -08:00
Leonardo de Moura
576c053c25
fix(library/tactic/inversion_tactic): bug at implementation_list update
2015-01-04 19:56:10 -08:00
Leonardo de Moura
faf78ce3e6
feat(library/definitional/equations): brec_on compilation
2015-01-04 17:45:13 -08:00
Leonardo de Moura
98a856373d
feat(library/util): add dec_level auxiliary procedure
2015-01-04 13:25:58 -08:00
Leonardo de Moura
926c140e17
fix(library/definitional/equations): fix clang compilation problems
2015-01-04 10:18:19 -08:00
Leonardo de Moura
bdfa919098
feat(library/definitional/equations): add brec_on based compilation
2015-01-03 22:23:37 -08:00
Leonardo de Moura
42354cd4fa
feat(library/locals): add auxiliary templates
2015-01-03 22:23:08 -08:00
Leonardo de Moura
376126241e
fix(library/definitional/equations): typo and bug
2015-01-03 15:29:34 -08:00
Leonardo de Moura
21a9cd58a3
fix(library/definitional/equations): bug when compiling in proof relevant kernels
2015-01-02 23:17:33 -08:00
Leonardo de Moura
7f7d318b22
feat(library/definitional/equations): add dependent pattern matching compilation
2015-01-02 22:06:40 -08:00
Leonardo de Moura
762a515a5b
feat(library/tactic/inversion_tactic): mark new arguments that have been "unified" into terms
2015-01-02 22:02:15 -08:00
Leonardo de Moura
3fb2d8bbc0
feat(library/tactic/inversion_tactic): use the "simpler" compilation approach in more cases
...
The approach implemented in the commit 8974d70c11ef7b9b2c5d can be
extended to indexed inductive families. See comments in the code.
2015-01-01 19:33:15 -08:00
Leonardo de Moura
be9e2500ce
feat(library/tactic/inversion_tactic): add more efficient "compilation" for non-indexed inductive datatypes
2015-01-01 19:33:14 -08:00
Leonardo de Moura
9be67bc0b1
feat(util/buffer): add method erase_elem
2015-01-01 19:33:14 -08:00
Leonardo de Moura
57490a6431
feat(library/tactic/inversion_tactic): avoid unnecessary eq.rec's
2015-01-01 19:33:14 -08:00
Leonardo de Moura
58f052b1bb
fix(library/normalize): unitialized variable
2015-01-01 19:33:14 -08:00
Leonardo de Moura
761810f350
feat(library/tactic/inversion_tactic): generate auxiliary information
2015-01-01 19:33:14 -08:00
Leonardo de Moura
e76ef18980
feat(util/name_map): add rename_map
2015-01-01 19:33:14 -08:00
Leonardo de Moura
1f13bfa4f7
feat(library/tactic/inversion_tactic): add inversion::apply procedure
...
The new procedure is essentially a "customized" version of the
inversion (aka cases) tactic for the equations package
2015-01-01 19:33:14 -08:00
Soonho Kong
f370871574
fix(emacs/lean-syntax): highlight axioms
...
fix #382
2014-12-30 14:25:19 -05:00
Leonardo de Moura
0aa7e4a9f9
fix(frontends/lean/pp): option 'pp.private_names' should also affect private declarations defined in the current file
2014-12-28 14:22:36 -08:00
Leonardo de Moura
d082fb7402
fix(shell/lean): crash when trying to read file without extension
2014-12-28 14:22:36 -08:00
Leonardo de Moura
1d79cb9c07
fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library
2014-12-22 09:40:15 -08:00
Leonardo de Moura
d2958044fd
feat(frontends/lean): add multiple_instances command
...
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command
multiple_instances <class-name>
closes #370
2014-12-21 17:28:44 -08:00
Leonardo de Moura
5efadb09cc
feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library
...
This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.
The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
2014-12-21 15:19:25 -08:00
Leonardo de Moura
677ec2a2fe
feat(library/tactic/inversion_tactic): adjust inversion tactic to HoTT lib
2014-12-20 11:32:27 -08:00
Leonardo de Moura
7a75325416
feat(kernel/abstract): add new abstract_local procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
Leonardo de Moura
2070ac849c
feat(library/util): add get_intro_rule_names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
Leonardo de Moura
d9d822baa7
feat(library/tactic/class_instance_synth): add mk_hset_instance procedure
2014-12-19 22:00:25 -08:00
Leonardo de Moura
8c63045492
feat(library/util): add more auxiliary procedures
2014-12-19 22:00:25 -08:00
Leonardo de Moura
d6f79423e9
feat(library/tactic/class_instance_synth): add mk_class_instance procedures
2014-12-19 20:09:09 -08:00
Leonardo de Moura
4421069e34
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
2014-12-19 19:57:38 -08:00
Leonardo de Moura
ded869b7e0
refactor(frontends/lean): move placeholder_elaborator to library/tactic
2014-12-19 15:23:22 -08:00
Leonardo de Moura
a22dc773b7
refactor(frontends/lean): move some auxiliary procedures to library/tactic
2014-12-19 15:19:45 -08:00
Leonardo de Moura
07d7ea2f4e
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
2014-12-19 15:08:21 -08:00
Leonardo de Moura
69750c50c6
refactor(frontends/lean): move pp_options to library
2014-12-19 15:00:05 -08:00
Leonardo de Moura
caf0a4bf15
refactor(frontends/lean): move type_checker_ptr typedef to library
2014-12-19 14:40:15 -08:00
Leonardo de Moura
02de288a51
refactor(frontends/lean): move choice_iterator to library
2014-12-19 14:29:32 -08:00