michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4227 commits 3 branches 0 tags 28 MiB
Commit graph

4227 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
345b65a91b fix(.travis.yml): trying to fix failure at travis 2014-09-26 18:00:55 -07:00
Leonardo de Moura
23960da532 feat(emacs/lean-input): shortcut for long arrow 2014-09-26 17:50:33 -07:00
Floris van Doorn
3a95734fae feat(library): changes in eq.lean sigma.lean and category.lean 
in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5
in sigma.lean, finish proving equality of triples
in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator
 2014-09-26 19:45:23 -04:00
Floris van Doorn
05fb3aa060 feat(library/data/int): remove duplicate theorem, fix one sorry 2014-09-26 19:45:23 -04:00
Floris van Doorn
5396e422d2 feat(library): add constructions of categories, some changes in eq, sigma and path 
in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach
 2014-09-26 19:45:23 -04:00
Leonardo de Moura
ab7d2b1751 fix(.travis.yml): trying old configuration for TESTCOV 2014-09-26 16:41:18 -07:00
Leonardo de Moura
adc0cef974 doc(README.md): group build instructions by system 2014-09-26 16:31:27 -07:00
Leonardo de Moura
fff0c2f84a doc(make/msys2): instructions for building native windows Lean binary 2014-09-26 16:26:32 -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
631ebc6c4b fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning. 
Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
 2014-09-26 09:42:31 -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
f49a610995 fix(.travis.yml): (try to fix) random build failures at travis 
At https://bitcointalk.org/index.php?topic=304389.0, people suggest
that the failure

    g++-4.8: internal compiler error: Killed (program cc1plus)

usually happens when the system does not have enough free memory.
A possible workaround is to disable parallel build, and compile file by
file. I added the option `-j1` to Ninja.
 2014-09-26 09:05:30 -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