Soonho Kong
f8d2ed7936
feat(emacs/lean-type): maintain nay-retry timer
2014-08-27 00:48:55 -07:00
Soonho Kong
224a4feba2
fix(emacs/lean-type): problem with lean-eldoc-nay-retry-time
...
If (current-idle-time) is non-zero, we need to set a timer to run
eldoc-documentation-function again when idle-time = (current-idle-time)
+ retry-delay.
2014-08-26 23:58:02 -07:00
Soonho Kong
a1a14cf425
fix(emacs/lean-info): handle when both identifier and symbol info exist
...
Example: library/data/int/basic.lean file (398, 22)
The '+' symbol is attached with both of identifier info and symbol info
-- SYMBOL|398|22
+
-- ACK
-- IDENTIFIER|398|22
int.add
-- ACK
2014-08-26 22:32:57 -07:00
Soonho Kong
b9c1b1e186
fix(emacs/lean-info): type of a symbol at the end of buffer
2014-08-26 22:32:57 -07:00
Leonardo de Moura
dd99e60a00
refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:07:09 -07:00
Soonho Kong
1de515f693
feat(emacs/lean-mode): clean up old generic-mode
2014-08-26 17:16:16 -07:00
Soonho Kong
665a8f3ecb
feat(emacs/lean-server): handle signal
2014-08-26 17:16:16 -07:00
Soonho Kong
0426d04cb9
feat(emacs/README.md): add elisp which installs required packages
2014-08-26 17:16:16 -07:00
Soonho Kong
83f05e104a
fix(emacs/lean-server): fix ERROR regex pattern
2014-08-26 16:22:32 -07:00
Soonho Kong
682b13a906
feat(emacs/lean-mode): run eldoc-documentation-function at openning
2014-08-26 16:22:32 -07:00
Soonho Kong
c77e5c6b34
feat(emacs/lean-tags): try to find TAGS file upward and use it without asking
2014-08-26 16:22:32 -07:00
Soonho Kong
dfab827d22
feat(emacs/lean-tags): attach advice to tag functions to run ltags
2014-08-26 16:22:32 -07:00
Soonho Kong
1f0bfb67b0
feat(emacs/lean-tags): use full-name to look up tags
2014-08-26 16:22:32 -07:00
Soonho Kong
3d3669e45e
feat(emacs/lean-mode): add key-bindings, deps
2014-08-26 16:22:32 -07:00
Soonho Kong
dd5231d6a7
fix(emacs/lean-server): check current-file before send EVAL
2014-08-26 16:22:32 -07:00
Soonho Kong
f7ff5ec3d6
fix(emacs/lean-server): when handle dead lean-server
2014-08-26 16:22:32 -07:00
Soonho Kong
5965bcc10b
refactor(emacs/lean-server): lean-server-check-current-file takes file-name
2014-08-26 16:22:31 -07:00
Soonho Kong
cc1d44e541
feat(emacs/lean-type): implement lean-set-option and lean-eval-cmd
...
close #55
2014-08-26 16:22:31 -07:00
Soonho Kong
50063b659b
refactor(lean-variable): init server-buffer and current-file-name with nil
2014-08-26 16:22:31 -07:00
Soonho Kong
f82f0377ff
feat(emacs/lean-cmd): add cmd-to-string for SET/EVAL
2014-08-26 16:22:31 -07:00
Soonho Kong
292750c4c9
feat(emacs/lean-type): add SET/EVAL commands
2014-08-26 16:22:31 -07:00
Soonho Kong
679a034277
feat(emacs/lean-mode): use define-derived-mode
2014-08-26 16:22:31 -07:00
Soonho Kong
c1ed9b1293
refactor(emacs/lean-type): clean up eldoc-function and fill-placeholder
2014-08-26 16:22:31 -07:00
Soonho Kong
7ea5c9541d
feat(emacs/lean-info): use cl-struct lean-info-record
2014-08-26 16:22:31 -07:00
Soonho Kong
ccc1f89f61
refactor(emacs/lean-server): use global-server-message-to-process
...
We are using asynchronous process mechanism to communicate between
lean-server and emacs. A sender function like
lean-eldoc-documentation-function sends a command and waits until
lean-global-server-message-to-process is non-nil. When a message is
received from lean-server, a filter function lean-server-output-filter
is triggered. This filter function concatenates a received message to
the buffer until it sees the end of message markers (--
END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer
messages into pre, body, and post parts. Then it assembles a message to
process and attaches the message to
lean-global-server-message-to-process variable. A sender function which
is watching for the variable will recognize it, exit the polling, and
process the message.
2014-08-26 16:22:31 -07:00
Soonho Kong
fc44c7242c
feat(emacs/lean-settings): add eldoc-use and eldoc-nay-retry-time
...
close #51
2014-08-26 16:22:31 -07:00
Soonho Kong
10fb60e4dd
refactor(emacs/lean-util): remove unused functions
...
- take-first-n/last-n => use -take, -drop (from dash.el)
- string-join => use one in flycheck
- remove other unused functions
2014-08-26 16:22:31 -07:00
Soonho Kong
812934f31f
refactor(emacs/lean-flycheck): remove lean-flycheck-initialized
2014-08-26 16:22:31 -07:00
Soonho Kong
495809d86d
feat(emacs/lean-syntax): support multi-line comments /- ... -/
2014-08-26 16:22:30 -07:00
Soonho Kong
c0762333bd
feat(emacs/lean-cmd): add set and eval cmds
2014-08-26 16:22:30 -07:00
Leonardo de Moura
b8b5a59117
fix(frontends/lean/info_manager): do not rely on typeid::before, the behavior is a platform specific
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 14:23:12 -07:00
Leonardo de Moura
11711a2409
fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 12:46:24 -07:00
Leonardo de Moura
4c9723e5ed
fix(library/unifier): assertion violation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:07:34 -07:00
Leonardo de Moura
44c597724b
fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:01:17 -07:00
Leonardo de Moura
02b7f980b0
fix(library/num): bug in to_pos_num, missing test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 08:18:07 -07:00
Leonardo de Moura
3903be34a4
feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 21:26:17 -07:00
Leonardo de Moura
04d9eb17d1
feat(kernel/conveter): improve support for proof irrelevant in the converter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 11:19:18 -07:00
Leonardo de Moura
82a7de83cc
feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 10:23:28 -07:00
Leonardo de Moura
fbf13994d8
refactor(*): use + for concatenating format objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 09:35:25 -07:00
Leonardo de Moura
eb794f7491
refactor(shell): remove obsolete tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:12:19 -07:00
Leonardo de Moura
dbaf81e16d
refactor(library): remove unnecessary 'standard' subdirectory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Leonardo de Moura
df60ab4ada
fix(frontends/lean/calc): allow calc_subst to be defined for multiple operators, allow calc cmds to be organized into namespaces, fixes #65
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 16:45:04 -07:00
Leonardo de Moura
2f699fa53a
feat(*): make sections 'permanent', and add 'transient' contexts, closes #88
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 15:45:15 -07:00
Leonardo de Moura
b13851ba13
feat(frontends/lean): add kind and type to index, closes #89
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 12:39:59 -07:00
Leonardo de Moura
01736bf82a
feat(util/sexpr/format): expose flatten
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 12:00:32 -07:00
Leonardo de Moura
e602c4ba49
feat(frontends/lean): change multicomment to /- ... -/
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:55:13 -07:00
Leonardo de Moura
c5a44aca44
fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:07:12 -07:00
Leonardo de Moura
2ada3af405
fix(frontends/lean/info_manager): add instantiate method to synth_info_data, fixes #94
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:55:15 -07:00
Leonardo de Moura
a5f0593df1
feat(*): change inductive datatype syntax
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:46:10 -07:00
Leonardo de Moura
01000ff7df
feat(library): add typed_expr macro
...
We use it to enforce that a let-variable has the expected type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 11:26:06 -07:00
Leonardo de Moura
d4ac482d76
refactor(kernel): move annotation to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:38:10 -07:00
Leonardo de Moura
b746492ac8
refactor(library/simple_formatter): rename simple_formatter to print
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:32:08 -07:00
Leonardo de Moura
7d987df429
refactor(kernel/formatter): move simple_formatter to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:26:45 -07:00
Leonardo de Moura
937c465685
fix(library/unifier): too much reduction
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 21:37:51 -07:00
Leonardo de Moura
07bc0727e2
feat(frontends/lean): 'let [inline]' is the default
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 18:24:22 -07:00
Leonardo de Moura
6cf73b51e2
fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 17:56:18 -07:00
Leonardo de Moura
3498d7ad61
fix(frontends/lean/parser): missing identifier information, fixes #83
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
2071a5986f
fix(frontends/lean/server): crash: uninitialized memory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
bb6dbe0e6f
fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
725f5ba0a0
feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Soonho Kong
f4dfec548d
fix(emacs/lean-mode): add missing flycheck-init
2014-08-21 10:05:14 -07:00
Soonho Kong
39f9826dca
fix(emacs/lean-mode): enable company-etags in lean-mode
2014-08-21 10:05:14 -07:00
Soonho Kong
272c463182
fix(emacs/lean-info): temporary fix for NAY problem
2014-08-21 10:05:14 -07:00
Soonho Kong
09b6fb4f7c
fix(emacs): roll back to generic mode
2014-08-21 10:05:14 -07:00
Leonardo de Moura
359c72b02f
fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 09:28:07 -07:00
Soonho Kong
42c2fef0f2
fix(tests/util/sequence.cpp): clang build error
2014-08-20 21:20:17 -07:00
Leonardo de Moura
e5057ed155
fix(library/unifier): remove incorrect assertion, a local constant may occur in the type of a metavariable that was not instantiated yet
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 18:22:43 -07:00
Jeremy Avigad
6264fb52d6
fix(lean/library/standard): fix tests, more cleanup
2014-08-20 18:04:31 -07:00
Leonardo de Moura
f5987b7bda
refactor(library/unifier): make it easier to add new options to the unifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 17:30:08 -07:00
Leonardo de Moura
0450e81392
feat(library/unifier): allow computation when solving flex-rigid constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:20 -07:00
Leonardo de Moura
fa342c8ea7
fix(library/unifier): missing set_conflict
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
9588336c15
refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
4cf3d32e0c
chore(*): create alias for std::pair
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
fcf1778ee0
feat(util): add sequence object with O(1) concatenation operation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Soonho Kong
51b86b219b
feat(emacs/lean): add multi-line comments
...
This is related with issue #63 .
There are two known issues:
- Emacs behaves as if the multi-line comment start/end symols are "(-"
and "-)" instead of "(--" and "--)". As a result, it shows all the
correct lean comments as it is. However, it will show some examples
such as "(-5)" as a part of comment even if Lean doesn't interpret it
as it is. Technically, it's because we are using a syntax-table based
method to define comments. For more information read a documentation
of 'modify-syntax-entry' function.
- Somehow, the matching parens are broken. When we type "--)" to close
a multi-line comment. Emacs warns "Mismatched Parentheses".
2014-08-19 15:03:51 -07:00
Soonho Kong
c27a379f28
feat(emacs): add company mode (via etags)
2014-08-19 15:03:51 -07:00
Leonardo de Moura
f0d50e0d33
feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
08ae17650b
feat(frontends/lean): try overloaded notation and declarations in the order they were defined
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
919f02983e
feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
4a96fefd96
fix(library/unifier): bug in unifier priority queue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Soonho Kong
608b66c323
fix(emacs/lean-server): check buffer-modified-p before create a process
...
fix #57
2014-08-18 14:18:11 -07:00
Soonho Kong
7a8796a4ca
feat(emacs/lean-info): add identifier/symbol/nay
2014-08-18 14:17:44 -07:00
Soonho Kong
ea4cfe5e7d
refactor(emacs/lean-type): clean up
2014-08-18 13:34:13 -07:00
Soonho Kong
46013b6ad2
feat(emacs): define lean-mode as a derived-mode of prog-mode
...
Fix #52
2014-08-18 13:32:58 -07:00
Soonho Kong
5fa2b9c057
fix(emacs/lean-util): add missing 'cl-' prefix
2014-08-17 18:09:01 -07:00
Leonardo de Moura
05b0f24cb5
fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 17:03:54 -07:00
Leonardo de Moura
92ab2dac83
chore(frontends/lean/server): remove leftover
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 16:12:31 -07:00
Leonardo de Moura
3d8477f7de
fix(library/module): ignore multiple declarations of 'sorry', fixes #59
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 15:55:58 -07:00
Leonardo de Moura
dcc8f4e4fc
feat(frontends/lean/elaborator): generate identifier information for overloaded identifiers
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 15:18:51 -07:00
Leonardo de Moura
0073ddf583
feat(frontends/lean): add 'SYMBOL' and 'IDENTIFIER' information to info_manager
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 15:06:46 -07:00
Leonardo de Moura
55b0a03e3d
refactor(frontends/lean/info_manager): to allow cache to be used when producing info data, fixes #37 , closes #45
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 12:16:32 -07:00
Leonardo de Moura
c6600bdaf4
refactor(frontends/lean/info_manager): intrusive smart pointer for info_data
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 08:28:02 -07:00
Leonardo de Moura
5bc62f0ba9
fix(library/coercion): error message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-17 06:59:52 -07:00
Leonardo de Moura
1436212a34
fix(library/unifier): use depth-first search strategy for solving class-instance constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-16 13:51:24 -07:00
Soonho Kong
030eec1d06
feat(emacs): add lean-complete-tag (tab)
2014-08-15 21:30:47 -07:00
Soonho Kong
483bae0b97
feat(emacs): add lean-find-tag (M-.)
2014-08-15 21:24:34 -07:00
Leonardo de Moura
008b43d92a
refactor(frontends/lean/info_manager): add method info_data::compare
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 18:09:31 -07:00
Leonardo de Moura
14d6b6d043
fix(frontends/lean/inductive_cmd): generate index for inductive decls, introduction rules, and recursor/eliminator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 18:02:41 -07:00
Leonardo de Moura
8d4e27461c
feat(frontends/lean/server): use separate thread for processing requests in server mode, interrupt whole parser when on interruption (when collecting information)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 17:24:37 -07:00
Leonardo de Moura
56a81eda6e
fix(frontends/lean/elaborator): uninit variable
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 16:39:21 -07:00
Leonardo de Moura
dc1613f535
feat(frontends/lean): annotate 'notation' subterms with 'noinfo' annotation (goal: improve typeinfo generation); fix initialization problem (with annotations)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 15:07:14 -07:00
Leonardo de Moura
670bfe24f5
chore(build): remove hott library directory, and move hott tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:30:56 -07:00
Leonardo de Moura
6a6c9f472e
feat(frontends/lean): add synthesis information only for 'explicit' placeholder
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 12:48:36 -07:00
Soonho Kong
05b2f93d14
fix(emacs/lean-flycheck): fix eval-after-load to use library name
2014-08-15 09:07:50 -07:00
Leonardo de Moura
3bb2fb2176
fix(frontends/lean/parser): uninit variable
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 09:06:34 -07:00
Soonho Kong
74b665ea06
fix(CMakeLists.txt): use bin/lean to build library
...
close #49
2014-08-14 18:21:58 -07:00
Soonho Kong
b18124e1a2
feat(emacs): replace metavar '?M_n' with '_' in synthed expr
2014-08-14 18:21:58 -07:00
Leonardo de Moura
2edb53397f
fix(library/declaration_index): style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 18:19:17 -07:00
Leonardo de Moura
dc3e9a15d2
refactor(library/definitions_cache): rename to definition_cache
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 18:12:12 -07:00
Leonardo de Moura
29a7d6d05a
fix(library/hott): remove hott_lib from build, it will be integrated in the standard library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 18:05:48 -07:00
Leonardo de Moura
343407b1b6
feat(shell/lean): add --index option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 18:05:48 -07:00
Soonho Kong
a4e8389695
feat(emacs): add lean-fill-placeholder (C-c C-f)
2014-08-14 17:12:23 -07:00
Leonardo de Moura
b4775eb017
feat(frontends/lean/server): add EVAL command, closes #40
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 16:08:43 -07:00
Leonardo de Moura
40f7ef5097
feat(shell/lean): display src file name when printing 'file not found in the LEAN_PATH' error, closes #47
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 15:48:31 -07:00
Soonho Kong
74dafe76bb
feat(emacs): use --permissive lmake option for flycheck
...
close #42
2014-08-14 15:06:30 -07:00
Leonardo de Moura
9f3f42f6a5
feat(frontends/lean/server): add SET command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 14:40:46 -07:00
Leonardo de Moura
4bbabfe6d4
feat(shell/lean): add --permissive command line option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 14:01:59 -07:00
Soonho Kong
24220a5f9e
feat(emacs): show synth information
2014-08-14 13:22:24 -07:00
Leonardo de Moura
8afd433f34
feat(frontends/lean/parser): allow parser to continue even if there are errors importing files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 11:28:44 -07:00
Leonardo de Moura
0d97fff280
feat(library/module): include name of corrupted .olean file
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 11:28:44 -07:00
Leonardo de Moura
d1c645977d
fix(frontends/lean/info_manager): add missing method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 11:28:44 -07:00
Soonho Kong
99e77db8ad
feat(emacs/lean-flycheck): override flycheck-try-parse-error-with-pattern
...
For lean-mode, we override flycheck-try-parse-error-with-pattern to
increase column number by 1. It uses defadvice.
2014-08-14 11:21:09 -07:00
Leonardo de Moura
be8ee8b3c0
feat(frontends/lean): add information about synthesized placeholders, closes #39
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 10:37:24 -07:00
Leonardo de Moura
28b7d87f1f
feat(frontends/lean/pp): pretty print numerals
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 09:12:22 -07:00
Leonardo de Moura
ebbca0d613
perf(library/num): avoid exception
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 09:12:22 -07:00
Leonardo de Moura
19537b72ee
feat(frontends/lean/elaborator): generate type information for placeholders
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 09:12:22 -07:00
Soonho Kong
a0a73463cc
feat(emacs/lean-server.el): add lean-server-{kill,restart}-process
...
[skip ci]
2014-08-14 08:56:46 -07:00
Soonho Kong
c19bcad845
fix(emacs): add and use lean-string-join
2014-08-14 08:42:52 -07:00
Leonardo de Moura
ced0ed0eca
fix(emacs): add missing 'require'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-14 08:21:42 -07:00
Soonho Kong
243cf2abb0
feat(emacs): show overload information
2014-08-14 07:23:15 -07:00
Leonardo de Moura
75be034d3d
fix(frontends/lean/server): crash when INFO is invoked before VISIT/LOAD
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-13 18:31:47 -07:00
Leonardo de Moura
d30854829d
refactor(frontends/lean): rename elaborator_env to elaborator_context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-13 17:06:48 -07:00
Soonho Kong
28d23390a6
feat(emacs): implement lean-show-type
2014-08-13 17:02:49 -07:00
Soonho Kong
d2ef577a14
feat(emacs/lean-flycheck): customize checker name and options
2014-08-13 15:07:12 -07:00
Soonho Kong
3cd381b0f7
fix(emacs): remove lean-get-this-if-true-or-that
2014-08-13 15:07:12 -07:00
Leonardo de Moura
e5a36467dd
fix(frontends/lean/scanner): wrong column information produced by scanner
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-13 12:32:37 -07:00
Leonardo de Moura
631e2395a3
refactor(frontends/lean/elaborator): add elaborator_env class
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 18:43:56 -07:00
Leonardo de Moura
2f48552f06
fix(frontends/lean/server): disable cache, when a definition is reused from the cache, we loose type information, fixes #35
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
2869d9059f
feat(frontends/lean): change 'proof-qed' semantics: no backtracking
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
b32d801116
refactor(frontends/lean/elaborator): remove unnecessary field: m_subst
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
c5aea3eba7
refactor(frontends/lean/elaborator): remove m_accumulated and eager metavariable instantiation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
60ab6d3bd8
feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
562926e7ad
refactor(kernel/instantiate): add functions instantiate_value_univ_params and instantiate_type_univ_params
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Soonho Kong
0ca0ccb77d
feat(frontend/lean/server.cpp): add "-- BEGININFO" header
2014-08-12 17:29:58 -07:00
Leonardo de Moura
d47d326cef
fix(library/unifier): bug in mk_imitiation_arg
...
Remove bogus constraint
cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax));
This constraint is incorrect because 'type' may contain local constants that are not in 'locals'.
We just rely on
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax));
When maux is assigned, the system will inforce that its type (which is based on maux_type) must be type correct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-11 15:44:23 -07:00
Leonardo de Moura
cb8185f016
feat(frontends/lean): add '#erase_cache' command (for debugging purposes)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-11 13:55:29 -07:00
Leonardo de Moura
faf2795a7b
feat(frontends/lean/server): add VISIT and CHECK commands
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-11 10:40:18 -07:00
Leonardo de Moura
71583ba9c8
feat(frontends/lean/server): use definitions_cache in the server object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 20:02:50 -07:00
Leonardo de Moura
34f0dedf46
feat(frontends/lean/server): add 'INSERT' and 'REMOVE' commands to lean 'server', make sure all commands use the same convention for numbering lines, update server.org
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 19:57:24 -07:00
Leonardo de Moura
f319d084d4
feat(library/Makefile.common): use new --cache/-c option at Makefile.common
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 11:20:08 -07:00
Leonardo de Moura
f896771987
refactor(library/tactic/expr_to_tactic): use annotations for implementing 'by'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 11:16:46 -07:00
Leonardo de Moura
9d4c073618
feat(frontends/lean): add option --cache
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 11:04:16 -07:00
Leonardo de Moura
21b151bc98
chore(shell/lean): rename shortname for --luahook option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 10:00:04 -07:00
Leonardo de Moura
dc503e6e3d
feat(library): add definitions_cache datastructure for implementing .clean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 09:53:13 -07:00
Leonardo de Moura
19daefaec5
fix(util/script_state): weird crash with Lua 5.1
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 23:13:30 -07:00
Leonardo de Moura
8ad0949269
fix(kernel/environment): initialization problem on OSX
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 16:14:35 -07:00
Leonardo de Moura
ee9be2837b
refactor(library/unifier): remove redundant code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 15:04:34 -07:00
Leonardo de Moura
4bcde576b8
perf(kernel/abstract): improve mk_binding performance
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 14:14:14 -07:00
Leonardo de Moura
4986226e41
fix(kernel/converter): missing delay_check case
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 08:07:41 -07:00
Leonardo de Moura
0af55beb56
perf(library/unifier): improve flex_rigid performance
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-09 08:07:15 -07:00
Leonardo de Moura
9d13f634f3
refactor(library/unifier): group flex_rigid case related methods in a functional object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-08 16:44:59 -07:00
Leonardo de Moura
49070895d1
perf(library/unifier): improve 'assign' method, keep old version
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 22:29:56 -07:00
Leonardo de Moura
24e8dca014
feat(library/explicit): allow 'as-is', 'explicit' and 'implicit' annotations to be saved in .olean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 19:13:48 -07:00
Leonardo de Moura
969afa8245
perf(library/unifier): improve check_imitation performance
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 18:28:23 -07:00
Leonardo de Moura
70c0eda9fc
feat(frontends/lean): make sure all scopes are closed in the end of the module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 17:08:59 -07:00
Leonardo de Moura
1a67e69678
feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:59:08 -07:00
Leonardo de Moura
2486c483cf
chore(kernel/error_msgs): change type mismatch error messages, closes #33
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:18:40 -07:00
Leonardo de Moura
9e6c5695be
fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:09:45 -07:00
Soonho Kong
88ef5d68f9
feat(emacs): add lean-flycheck-turn-on/off/toggle
2014-08-07 14:03:08 -07:00
Soonho Kong
b684af5cdb
feat(emacs): provide an option to disable lean-flycheck
2014-08-07 14:03:08 -07:00
Soonho Kong
209ecfd792
feat(emacs/lean-setting.el): add lean-rule-color custom-var
2014-08-07 14:03:08 -07:00
Soonho Kong
b6b40bb4ab
feat(emacs): use optional package when required
2014-08-07 11:59:59 -07:00
Soonho Kong
5ecc872278
fix(emacs): use cl-case, require cl-lib
2014-08-07 11:59:59 -07:00
Soonho Kong
07e188acdb
feat(emacs/README.md): add instr. for MELPA; add whitespace-cleanup-mode
2014-08-07 11:59:59 -07:00
Soonho Kong
a2867b3d06
feat(emacs/README.md): add README.md
2014-08-07 09:59:15 -07:00
Soonho Kong
f523c25c52
feat(emacs/lean-mode.el): use whitespace-cleanup-mode to fci-mode
2014-08-07 09:59:15 -07:00
Soonho Kong
f9f8c09143
refactor(emacs/lean-mode.el): clean up, add license
2014-08-07 09:59:15 -07:00
Soonho Kong
61f3897b0d
feat(emacs/lean-util.el): add lean-util.el
2014-08-07 09:59:15 -07:00
Soonho Kong
164eab5574
feat(emacs/lean-settings.el): add customization-settings file
2014-08-07 09:59:15 -07:00
Soonho Kong
977ccc4631
feat(emacs/lean-flycheck.el): add lean-flycheck.el
2014-08-07 09:59:15 -07:00
Leonardo de Moura
9a6df02683
fix(util/name): avoid assertion violation when reading numeric names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 08:32:43 -07:00
Leonardo de Moura
6d6c62461f
chore(library/kernel_serializer): add assertions for invalid uses of anonymous names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 08:32:32 -07:00
Leonardo de Moura
955d7d2659
fix(library/aliases): namespace and constant have the same name, and 'using' produces the 'empty' alias
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 08:32:21 -07:00
Leonardo de Moura
4ad7e709aa
feat(frontends/lean): default for inductive types, closes #32
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 07:52:37 -07:00
Leonardo de Moura
b56233cbe3
fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 23:15:05 -07:00
Leonardo de Moura
c6f3232f81
feat(frontends/lean): provide 'partial' type information even when there are type errors
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 21:56:57 -07:00
Leonardo de Moura
1cbf40a5d2
fix(frontends/lean): remove duplicate info entries, fix bug in save_overload
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 21:23:37 -07:00
Leonardo de Moura
0af4a67881
feat(frontends/lean): save type information after elaboration, remove --flyinfo option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 19:35:26 -07:00
Leonardo de Moura
0276f4c1c0
feat(frontends/lean): store 'overload' information, remove #setline
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 19:13:09 -07:00
Leonardo de Moura
1ba9a92df2
feat(frontends/lean/parser): save snapshots
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 18:31:53 -07:00
Leonardo de Moura
9b765a2a06
chore(frontends/lean): fix style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 18:10:33 -07:00
Leonardo de Moura
1a725574b1
refactor(frontends/lean): add 'server' module as a replacement for 'interactive'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 18:07:04 -07:00
Leonardo de Moura
2c3737bcc6
feat(frontends/lean): add info_manager
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-06 15:25:28 -07:00
Leonardo de Moura
da616f69ea
perf(library/unifier): do not explore branches that will trigger type errors
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 20:16:16 -07:00
Leonardo de Moura
bbc4380a52
fix(library/unifier): bug exposed by recent changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 19:02:30 -07:00
Leonardo de Moura
069f217215
fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 17:21:21 -07:00
Leonardo de Moura
d14cbfd7e9
refactor(frontends/lean/elaborator): local context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 16:25:54 -07:00
Leonardo de Moura
9cc2015caa
feat(library/unifier): better error message for invalid local context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5
feat(library/match): add 'local' backtracking
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51
feat(library/match): add basic match_plugin that just invokes whnf before failing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 08:37:03 -07:00