Commit graph

3671 commits

Author SHA1 Message Date
Leonardo de Moura
16562adb87 feat(frontends/lean): add 'coercions' and 'instances' to 'print' command, closes 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 
2014-10-03 10:11:21 -07:00
Soonho Kong
b78043ae24 feat(emacs/lean-mode): add 'clean-cache' to the menu
Related issue: 
2014-10-03 10:11:21 -07:00
Soonho Kong
fffb4e6019 feat(emacs/lean-server): delete cache file (.clean) after visit/load
fix 
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 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 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 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 2014-10-01 11:24:45 -07:00
Leonardo de Moura
966366e18e feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes 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 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 
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 .
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
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 
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 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 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 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 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 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 
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
Leonardo de Moura
358074ae3d refactor(kernel/record): remove kernel extension for records, we will
implement it outside of the kernel on top of the inductive datatypes
2014-09-24 10:12:28 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-24 10:12:28 -07:00
Leonardo de Moura
4dd7abb14e refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
Leonardo de Moura
27ff42d2e0 refactor(library): remove dead files 2014-09-23 10:28:20 -07:00
Leonardo de Moura
83b22823a6 refactor(library/tactic): explicit initialization/finalization 2014-09-23 10:06:15 -07:00
Leonardo de Moura
29d6bff785 refactor(frontends/lean): explicit initialization/finalization 2014-09-23 10:00:36 -07:00
Leonardo de Moura
79cfb32ec7 refactor(util): explicit initialization/finalization 2014-09-23 08:13:33 -07:00
Leonardo de Moura
4437a65d0b refactor(frontends/lean/builtin_cmds): explicit token initialization 2014-09-22 19:22:53 -07:00
Leonardo de Moura
531046626a refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
Leonardo de Moura
b6781711b1 refactor(*): explicit initialization/finalization for serialization
modules, expression annotations, and tactics
2014-09-22 15:26:41 -07:00
Leonardo de Moura
b1ee888aae refactor(*): start move to explicit initialization/finalization,
explicitly initialize/finalize options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-22 10:41:07 -07:00
Leonardo de Moura
648f209cfe fix(util/memory): redefine the non-throwing versions of the new
operator.

In some platforms, the following operator new is used

   void* operator new(std::size_t sz, std::nothrow_t const &)

Since, it was not defined by memory.cpp, a crash would happen whenever
our delete was invoked.

   void  operator delete(void * ptr) throw() { return lean::free(ptr); }

Our delete assumes the memory was allocated with our new at memory.cpp

   void* operator new(std::size_t sz)
2014-09-21 10:54:41 -07:00
Leonardo de Moura
10a4148adb fix(tests): make sure tests can be executed on Windows msys2 shell 2014-09-20 15:51:24 -07:00
Leonardo de Moura
704e203cd7 feat(util/lean_path): support LEAN_PATH that uses ':' instead of ';' on Windows 2014-09-20 15:24:20 -07:00
Leonardo de Moura
8867f47dd6 feat(build): build standard library when building on Windows 2014-09-20 10:52:59 -07:00
Leonardo de Moura
e3ac1f66e0 feat(util/lean_path): normalize path in function dirname 2014-09-20 10:52:58 -07:00
Soonho Kong
ee4255eb3d fix(emacs/lean-type): disable eldoc at flycheck error/warning
fix 
2014-09-20 10:20:47 -07:00
Soonho Kong
3e4755db25 fix(emacs/lean-tags): support windows 2014-09-20 10:06:42 -07:00
Soonho Kong
af4e18dd44 fix(emacs/lean-flycheck): support windows
In windows, we need to first call python interpreter to call linja.
2014-09-20 10:06:42 -07:00
Leonardo de Moura
8fe7465ade fix(frontends/lean/pp): when formatting a coercion to function-class
that contains implicit arguments
2014-09-20 09:56:46 -07:00
Leonardo de Moura
fd5daa8fda feat(frontends/lean): use coercions to function-class and sort-class in
function arguments, closes 
2014-09-20 09:00:10 -07:00
Leonardo de Moura
e430dc8bab feat(frontends/lean): add 'irreducible' as syntax sugar for 'reducible [off]' 2014-09-19 15:54:32 -07:00
Leonardo de Moura
4e2377ddfc refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
5d8c7fbdf1 refactor(frontends/lean): replace '[private]' modifier with 'private
definition' and 'private theorem', '[private]' is not a hint.
2014-09-19 15:54:32 -07:00
Leonardo de Moura
97b1998def refactor(frontends/lean): replace '[opaque]' modifier with 'opaque
definition', '[opaque]' is not a hint, but a kind of definition
2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef feat(frontends/lean): allow transient classes/instances, i.e.,
classes/instances that are not saved in .olean files
2014-09-19 15:54:32 -07:00
Leonardo de Moura
93c2c30310 feat(frontends/lean): allow transient coercions, i.e., coercions that
are not saved in .olean files
2014-09-19 15:54:32 -07:00
Leonardo de Moura
cbafa0dbf9 feat(library/scoped_ext): allow extensions to mark whether an entry is
persistent or not
2014-09-19 15:54:32 -07:00
Soonho Kong
5b9b814fd1 fix(shell/lean.cpp): use binary mode to open cache file 2014-09-19 09:36:23 -07:00
Leonardo de Moura
a3e43c2173 refactor(util/thread_script_state): remove 'enable_script_state_recycling' hack 2014-09-19 08:14:50 -07:00
Leonardo de Moura
49d5af473d refactor(kernel): remove support for proof irrelevant classes
Motivation: we can use Prop
2014-09-19 07:32:07 -07:00
Leonardo de Moura
87592cdb43 refactor(library): remove dead code 2014-09-18 22:45:53 -07:00
Leonardo de Moura
2bde3f55d5 feat(shell): include build type when printing version 2014-09-18 22:40:05 -07:00
Leonardo de Moura
dd31ed60b0 refactor(library): remove unnecessary file hott_kernel, HoTT and
standard library have been merged
2014-09-18 20:30:37 -07:00
Leonardo de Moura
b53b1825ae fix(frontends/lean/info_manager): get_closest_env_opts 2014-09-18 17:03:59 -07:00
Leonardo de Moura
9e29602934 fix(frontends/lean/info_manager): make sure env_info is not lost when
starting parser in the middle of the 'file'
2014-09-18 16:51:59 -07:00
Leonardo de Moura
970ad72bc3 fix(frontends/lean/pp): protect pretty printer from exceptions 2014-09-18 16:21:20 -07:00
Leonardo de Moura
b3e05a2fe9 refactor(frontends/lean/scanner): remove dependency to seekg and unget
methods

It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:

seekg() and seekp()

This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:

     seekg ( pos_type position );
     seekp ( pos_type position );

Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.

      seekg ( off_type offset, seekdir direction );
      seekp ( off_type offset, seekdir direction );

Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:

          ios::beg	offset specified from the beginning of the stream
          ios::cur	offset specified from the current position of the stream pointer
          ios::end	offset specified from the end of the stream

The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
2014-09-18 15:24:48 -07:00
Leonardo de Moura
243f80231a chore(kernel): fix style and lua bindings 2014-09-17 18:30:28 -07:00
Leonardo de Moura
ea1bae0143 refactor(kernel/converter): replace extra_opaque_set with predicate
It gives us more flexibility.
2014-09-17 17:05:13 -07:00
Leonardo de Moura
1fbb554a16 feat(library/module): provide predicate module::is_definition 2014-09-17 16:32:00 -07:00
Leonardo de Moura
9733401c20 fix(frontends/lean/tactic_hint): failure when compiling lean terms into
tactics: mismatch on the number of universe parameters
2014-09-17 15:23:10 -07:00
Leonardo de Moura
8b76deb971 fix(util/thread_script_state): style 2014-09-17 15:23:10 -07:00
Leonardo de Moura
19148af7ae feat(build): do not display WARNING message when tcmalloc is not found 2014-09-17 15:23:10 -07:00
Leonardo de Moura
26918022d8 feat(build): use Release when compilation mode is not specified 2014-09-17 15:23:10 -07:00
Leonardo de Moura
e3e1668f27 fix(util/thread_script_state): disable script_state recycling at finalization time
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-17 09:57:17 -07:00
Leonardo de Moura
a72a11db8e fix(util/script_state_manager): crash when compiling with msys2 stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-17 08:39:06 -07:00
Leonardo de Moura
aa5abefaff fix(util/thread_script_state): make sure system does not crash during
finalization
2014-09-17 08:25:21 -07:00
Soonho Kong
9161a6a210 fix(emacs/lean-type): change where to trigger eldoc
Previously, eldoc is triggered regardless of current position.
Now, it is triggered:

 - *NOT* looking-at whitespace or
 - looking-back end-parens such as ')', '}', ']', etc
2014-09-17 00:24:30 -07:00
Leonardo de Moura
9a2f1ba423 fix(util): compilation problems when using msys2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-16 21:29:51 -07:00
Leonardo de Moura
f03f0aa8b9 fix(util/thread): MULTI_THREAD=OFF mode 2014-09-16 20:44:43 -07:00
Leonardo de Moura
2b0623c0a1 fix(frontends/lean): assertion violations 2014-09-16 18:59:51 -07:00
Leonardo de Moura
78ad24a697 feat(frontends/lean/server): add SYNC command, closes 2014-09-16 18:42:34 -07:00
Leonardo de Moura
e3e2370a38 feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-16 18:03:40 -07:00
Leonardo de Moura
4b51d50ad4 fix(frontends/lean/elaborator): coercion overloading 2014-09-16 15:12:20 -07:00
Leonardo de Moura
dffe9a6f17 fix(frontends/lean/elaborator): more robust support for coercions to
function-class that contains implicit arguments
2014-09-16 13:08:34 -07:00
Leonardo de Moura
d0d23eb525 fix(frontends/lean/inductive_cmd): improve name resolution in inductive
command

The new test demonstrates the problem being fixed by this commit
2014-09-16 09:48:51 -07:00
Soonho Kong
2a8ddf055b fix(emacs/lean-option): fix lean-get-options 2014-09-15 17:44:24 -07:00
Soonho Kong
aa9fe958a9 feat(emacs/lean-debug): add lean-debug minor-mode
close 
2014-09-15 16:50:35 -07:00
Leonardo de Moura
af2c3b1815 fix(frontends/lean/info_manager): bug in save_environment_options,
server was displaying old results
2014-09-15 16:05:17 -07:00
Leonardo de Moura
93e83baa1b fix(frontends/lean/parser): commit_upto invocation after 'import' 2014-09-15 16:05:17 -07:00
Leonardo de Moura
feb4993f9c fix(frontends/lean/server): '[anonymous]' entry being displayed by FINDP
This could happen when there is a declaration (e.g., nat) whose type is
equal to an active namespace.
2014-09-15 16:05:17 -07:00
Soonho Kong
18e6481ce3 test(emacs/lean-option-test): add lean-test-update-string-alist-default 2014-09-15 13:04:53 -07:00
Soonho Kong
b650793b33 feat(lean-option): handle default pp.width option value 2014-09-15 13:04:53 -07:00
Soonho Kong
254d861970 feat(bin/linja): pass -D config option to lean
Close 
2014-09-15 13:04:13 -07:00
Soonho Kong
2bdc415a34 fix(emacs/lean-option): handle lean-option-string when it's nil 2014-09-15 11:26:53 -07:00
Soonho Kong
11ff7b5d33 feat(lean-mode): enable mmm-parse-when-idle
Related issue: 
2014-09-15 10:23:38 -07:00
Soonho Kong
f94e28ce39 fix(emacs/lean-mode): disable flycheck-lua inside of lean-mode
Related issue: 
2014-09-15 10:23:31 -07:00
Soonho Kong
c3d39938ac test(emacs): add lean-option-test 2014-09-15 09:48:33 -07:00
Soonho Kong
4bbfe4ec79 feat(emacs/lean-tags): add lean-global-search
close 
2014-09-15 09:48:33 -07:00
Soonho Kong
ff6862f587 fix(emacs/lean-mode): pass lean-options to lean-execute
Related issue: 
2014-09-15 09:48:26 -07:00
Soonho Kong
75ab5e07d6 feat(emacs/lean-option): save lean-options to lean-global-option-alist 2014-09-15 09:46:06 -07:00
Soonho Kong
f25f9a8fab fix(emacs/lean-mmm-lua): add 'insert' for mmm-insert-region (C-c % l)
Related issue: , https://github.com/flycheck/flycheck/issues/349, https://github.com/purcell/mmm-mode/issues/32
2014-09-15 00:03:21 -07:00
Soonho Kong
1527efb108 fix(emacs/lean-mode): run company-lean--check-prefix before auto-complete
fix 
2014-09-14 23:15:24 -07:00
Soonho Kong
27b20c5585 fix(emacs/lean-company): fix auto-complete behavior after tab
fix 
2014-09-14 23:15:24 -07:00
Soonho Kong
81ecbb4c94 fix(emacs/lean-company): import auto complete bug
fix 
2014-09-14 23:15:24 -07:00
Soonho Kong
d424cdd336 feat(emacs/lean-company): add custom-variable lean-company-type-foreground
Close 
2014-09-14 23:15:24 -07:00
Soonho Kong
87ad568ae6 fix(emacs/CMakeLists.txt): add all *.el files when install 2014-09-14 23:15:24 -07:00
Soonho Kong
50213fc664 fix(emacs/Makefile): add missing Makefile 2014-09-14 23:14:42 -07:00
Soonho Kong
df588d6ba0 fix(lean-flycheck): make column optional when detecting error/messages
fix 
2014-09-14 23:14:42 -07:00
Leonardo de Moura
d47412d201 fix(frontends/lean/parser): error line numbers for lua code, fixes 2014-09-14 21:03:09 -07:00
Leonardo de Moura
841658ec37 feat(library/error_handling): generate valid line and column information
when in flycheck mode
2014-09-14 20:15:22 -07:00
Leonardo de Moura
edcbe6fe10 feat(frontends/lean): allow multiple coercions from class A to B, closes
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-14 12:59:43 -07:00
Leonardo de Moura
1b6d4460e9 chore(library/coercion): cleanup 2014-09-14 12:59:43 -07:00
Soonho Kong
765d9b032f feat(src/cmake/modules/CleanOlean.cmake): add CleanOlean.cmake
Instead of using 'find -delete', use CMAKE's FILE GLOB_RECURSE and FILE
REMOVE to implement clean-olean.

Related issue: 
2014-09-14 01:40:21 -07:00
Soonho Kong
2d29d6d319 feat(emacs/lean-company): auto-completion for import
Close 
2014-09-14 00:00:25 -07:00
Soonho Kong
bf9ff192ca chore(emacs/README.md): add 'f' as a required package for lean-mode 2014-09-13 23:35:38 -07:00
Leonardo de Moura
d647954f93 feat(frontends/lean/elaborator): constraints associated with 'proof-qed'
blocks are solved independently, closes 
2014-09-13 10:21:10 -07:00
Leonardo de Moura
8c8c9d1c4a feat(frontends/lean/elaborator): cleanup and remove unnecessary code 2014-09-12 17:55:27 -07:00
Leonardo de Moura
0c50517058 refactor(frontends/lean/elaborator): do not save/restore cache 2014-09-12 17:39:11 -07:00
Leonardo de Moura
6db46e0505 fix(frontends/lean/server): std::unordered_map::insert does replace
existing entry, fixes 
2014-09-12 16:50:06 -07:00
Leonardo de Moura
b7023ce1d8 fix(frontends/lean/placeholder_elaborator): do not truncate stream of
solutions during class-instance resolution, closes 

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
2014-09-12 16:12:23 -07:00
Leonardo de Moura
b482f27543 fix(util/lazy_list): bug in filter operation 2014-09-12 16:12:23 -07:00
Leonardo de Moura
b7dcb8f833 fix(frontends/lean/elaborator): remove annotation left-over 2014-09-12 16:12:23 -07:00
Soonho Kong
563cfa73ec feat(emacs/lean-changes): handle before/after-revert 2014-09-12 14:25:08 -07:00
Soonho Kong
27ae03878c refactor(emacs/lean-server): rename flush-changed-lines to server-flush-changed-lines 2014-09-12 14:25:08 -07:00
Soonho Kong
c034c54f50 refactor(emacs/debug): rename lean-server-debug to lean-debug 2014-09-12 14:25:08 -07:00
Leonardo de Moura
029acbd1df feat(library/coercion): better support for coercions to function-class. closes 2014-09-12 13:17:20 -07:00
Leonardo de Moura
62585f1c56 fix(library/coercion): remove spurious '\n' 2014-09-12 13:08:47 -07:00
Leonardo de Moura
a2e36e97f2 fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes 2014-09-12 12:13:29 -07:00
Leonardo de Moura
010ecebfea feat(frontends/lean): add proof-qed expression
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
2014-09-11 18:14:49 -07:00
Leonardo de Moura
7ffe73b8ca fix(frontends/lean): name clash inside section, fixes 2014-09-11 16:37:23 -07:00
Leonardo de Moura
85f7132efe feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes , closes , closes 2014-09-11 14:49:35 -07:00
Leonardo de Moura
03902d4b45 refactor(library/unifier): add option m_discard too unifier, if m_discard == false, then unsolved flex-flex constraints are returned, the unifier also does not apply "last resource" techniques that may miss many solutions. 2014-09-11 14:49:35 -07:00
Leonardo de Moura
935ba35292 feat(library/unifier): keep normalization result when processing universe level unification constraints 2014-09-11 14:49:35 -07:00
Leonardo de Moura
c7c35becb2 feat(library/io_state): add default constructor to io_state 2014-09-11 14:49:35 -07:00
Leonardo de Moura
80fd14b39e refactor(frontends/lean): replace collect_metavars with metavar_closure helper class 2014-09-11 14:49:35 -07:00
Soonho Kong
b31edb2cee fix(emacs/lean-company): pass dummy continuation for WAIT 2014-09-11 13:46:07 -07:00
Soonho Kong
0b507777f9 fix(emacs/lean-company): repaint background in the candidate only when required 2014-09-11 13:44:54 -07:00
Soonho Kong
389fe02597 fix(emacs/lean-server): handle modified buffer only when process start 2014-09-11 12:40:10 -07:00
Soonho Kong
733c0e4a77 chore(emacs/lean-server): make trace-mode and debug-mode non-local vars 2014-09-11 12:34:23 -07:00
Soonho Kong
89f38b3945 test(emacs/features): add ecukes template 2014-09-11 12:33:49 -07:00
Soonho Kong
2ba43f1432 refactor(emacs): move tests in *.el files to 'test' directory 2014-09-11 12:29:32 -07:00
Soonho Kong
45b7327d63 doc(emacs/README.md): add contribution section 2014-09-11 12:29:00 -07:00
Soonho Kong
c879b2ce6d chore(emacs/Cask): add ert-runner, ecukes 2014-09-11 11:12:05 -07:00
Soonho Kong
4b556a41ed feat(emacs/lean-server): async task queue holds type of cmds as well 2014-09-11 04:09:21 -07:00
Soonho Kong
565402f3d6 feat(lean-server): handle signals (error/quit) in continuations
Related with 
2014-09-11 04:07:50 -07:00
Soonho Kong
5b28480809 chore(emacs/lean-server): send signal info to lean-server-trace 2014-09-11 04:04:20 -07:00
Soonho Kong
92f8a22ea1 fix(emacs/lean-company): send dummy continuation when send wait 2014-09-11 04:03:23 -07:00
Leonardo de Moura
1e5ba9bd75 refactor(frontends/lean/elaborator): move coercion_elaborator to its own module 2014-09-10 16:42:49 -07:00
Leonardo de Moura
6bc41f8dde refactor(frontends/lean/elaborator): move placeholder_elaborator to its own module 2014-09-10 16:42:49 -07:00
Leonardo de Moura
9ce356e515 refactor(frontends/lean/local_context): do not use references in the local context 2014-09-10 16:42:49 -07:00
Soonho Kong
63c0510a05 feat(emacs/lean-tags): detect and support multiple TAGS
Close 
2014-09-10 16:38:36 -07:00
Soonho Kong
1ea8b66a39 fix(emacs/lean-company): enable auto-complete when prefix length >= 1
[skip ci]
2014-09-10 16:21:44 -07:00
Soonho Kong
1c5497e632 feat(emacs/lean-project): add lean-project-create to imenu
Related with 
2014-09-10 15:19:11 -07:00
Soonho Kong
b05ca1db0f fix(emacs/lean-tags): handle exceptions from find-tag 2014-09-10 14:14:42 -07:00
Soonho Kong
b51e8dd1b9 fix(emacs/lean-server): respect order of messages in check-buffer-and-partition 2014-09-10 14:14:42 -07:00
Soonho Kong
7c4debd1d1 feat(emacs/lean-server): handle modified buffer when send VISIT cmd
Close 
2014-09-10 14:14:42 -07:00
Leonardo de Moura
669b1bff45 refactor(frontends/lean/elaborator): rename choice_elaborator to choice_iterator and move to separate module 2014-09-10 11:20:16 -07:00
Leonardo de Moura
e128610711 chore(tests): use option -t 100000 to speedup tests 2014-09-10 11:20:16 -07:00
Leonardo de Moura
4a4de27a6c refactor(frontends/lean/elaborator): move local_context to separate file 2014-09-10 11:20:16 -07:00
Leonardo de Moura
4ea322febc chore(frontends/lean/elaborator): minor cleanup 2014-09-10 11:20:16 -07:00
Soonho Kong
cab1811927 feat(emacs/lean-server): print out signal event to debug buffer 2014-09-10 09:07:16 -07:00
Leonardo de Moura
b82092a123 fix(frontends/lean/parser): segmentation fault after REPLACE, fixes 2014-09-10 08:39:39 -07:00
Soonho Kong
8fd938e142 fix(util/lean_path.cpp): get_exe_location follows symbolic link in OSX
Previously, we had different behaviors on Linux and OSX when
get_exe_location finds a location of executable:

 - Linux: follow symbolic link
 - OSX: not follow symbolic link
2014-09-10 07:41:14 -07:00
Leonardo de Moura
570879b55f feat(frontends/lean): add declaration to namespace without opening it, closes 2014-09-09 18:02:14 -07:00