max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11230 commits 1 branch 0 tags 5.3 GiB
Commit graph

8044 commits

Author SHA1 Message Date
Leonardo de Moura
dae1c9dac2 chore(CMakeLists): make sure we change the version number in a single place 2017-01-19 18:28:51 -08:00
Sebastian Ullrich
3f65690706 feat(emacs/lean-server): print out entire server response on error 2017-01-19 17:50:36 -08:00
Sebastian Ullrich
cc1553d901 fix(emacs/lean-server): dump response before trying to parse it 2017-01-19 17:50:36 -08:00
Sebastian Ullrich
4cba998de3 fix(CMakeLists): minimum g++ version is 4.9 2017-01-19 17:50:36 -08:00
Gabriel Ebner
ecdd17738d feat(emacs): add toggle for pending task highlight 2017-01-19 17:49:35 -08:00
Leonardo de Moura
d0a578c3db feat(library/init/meta/environment): add is_projection 2017-01-18 18:12:08 -08:00
Gabriel Ebner
bf20be51d5 chore(emacs/lean-server): put face into lean group for customization 2017-01-18 08:32:53 -08:00
Gabriel Ebner
be6b81db07 chore(emacs): remove lean-flycheck-use option 2017-01-18 08:32:53 -08:00
Gabriel Ebner
9b63ceff91 chore(emacs/lean-project): remove old project file contents 2017-01-18 08:32:53 -08:00
Gabriel Ebner
9530a7db1c chore(emacs): remove unused options 2017-01-18 08:32:53 -08:00
Leonardo de Moura
b309ef66d7 fix(library/equations_compiler/elim_match): fix #1318 2017-01-18 08:21:53 -08:00
Leonardo de Moura
694e6f47dc fix(library/init/meta/smt/ematch,library/tactic/simp_lemmas): trick for adding equations of a definition to a simp/hinst lemma set 
Before this commit, if we declared an equational lemma using 'def',
then it would not be correctly added to the simp/hinst lemma set.
The new test exposes the problem.
 2017-01-18 02:05:04 -08:00
Leonardo de Moura
c52be7e8c5 feat(frontends/lean,shell): autocompletion for ^. 
@kha, I added autocompletion for ^. I try to elaborate the expression
before ^. using the local context provided by the parser.

The autocompletion only works if the type for the expression before ^. can be
inferred. This is a big limitation because this information cannot be
obtained in many cases. Here are examples that do not work:

  meta def proof_for (e : expr) : smt_tactic expr :=
  do cc ← to_cc_state, cc^.proof_for e
                         --^ does not work here

If we annotate cc with its type, it works:

  meta def proof_for (e : expr) : smt_tactic expr :=
  do cc : cc_state ← to_cc_state, cc^.proof_for e
                                    --^ works

We don't have typing information on the equation lhs at
autocompletion time. So, the following will not work

   private meta def mk_smt_goals_for (cfg : smt_config)
        : list expr → list smt_goal → list expr → tactic (list smt_goal × list expr)
   | []        sr tr := return (sr^.reverse, tr^.reverse)
                                  --^ does not work since
   | (tg::tgs) sr tr := ...
 2017-01-17 19:27:59 -08:00
Gabriel Ebner
0d949e0da7 chore(library/module_mgr): explain exceptional case 2017-01-17 17:10:37 -08:00
Gabriel Ebner
c601b9c7bd fix(emacs/lean-server): set safe value of json-false in lean-server-send-command 2017-01-17 17:10:37 -08:00
Gabriel Ebner
8f9e57231a feat(emacs/lean-server): update messages and tasks immediately when server is finished 2017-01-17 17:10:37 -08:00
Gabriel Ebner
7daefedf05 chore(shell/server): remove hard limit on number of reported tasks 2017-01-17 17:10:37 -08:00
Gabriel Ebner
7d9c89b519 feat(emacs/lean-server): show skullbones as soon as server dies 2017-01-17 17:10:37 -08:00
Gabriel Ebner
a230c47178 feat(util/task_queue,emacs,*): highlight running tasks with different background color 2017-01-17 17:10:37 -08:00
Sebastian Ullrich
484bb67d44 fix(frontends/lean/tactic_notation): report state after tactic execution on , 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
6acc2cf8b7 fix(frontends/lean/notation_cmd): some position fixes 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
7b049e7d55 fix(shell/server): prevent empty prefix completion for declarations 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
59055fd5d0 feat(emacs): new and improved goal and next error buffers 2017-01-17 16:38:00 -08:00
Sebastian Ullrich
568862ea91 chore(emacs): remove unimplemented binding C-c C-p 2017-01-17 16:38:00 -08:00
Leonardo de Moura
3178f41cce fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied 
see #1316
 2017-01-17 16:33:19 -08:00
Gabriel Ebner
b4774e9ed1 fix(library/vm/vm): fix segfault in call_stack_fn 2017-01-17 16:00:01 -08:00
Gabriel Ebner
1a6629ce3b feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
Leonardo de Moura
7a210a9b62 chore(library/util): style 2017-01-16 22:59:17 -08:00
Leonardo de Moura
fc00275636 fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
70b7a35cfe fix(library/constructions/has_sizeof): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
1db1f8b229 feat(kernel/inductive/inductive): do not force recursive arguments to occur after non-recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
29b7001bff fix(library/equations_compiler/elim_match): avoid nasty inferred types in auxiliary declarations produced by the equation compiler 2017-01-16 22:55:12 -08:00
Leonardo de Moura
cce6e4d58c fix(library/equations_compiler/compiler): fix #1315 2017-01-16 20:01:25 -08:00
Leonardo de Moura
bfa48ff0c7 fix(frontends/lean/parser): position info when error is inside notation 2017-01-16 10:29:00 -08:00
Leonardo de Moura
eabbc5bb68 chore(library/module_mgr): comment unreachable_code assertion 
@gebner, could you please take a look a check whether there is a better fix.
 2017-01-15 23:18:44 +01:00
Leonardo de Moura
67226269b4 feat(library/tactic/simp_lemmas): convenient way of adding equational lemmas of a definition to a simp set 2017-01-14 22:16:16 -08:00
Leonardo de Moura
6246e6d72f fix(src/CMakeLists): -DSTATIC=ON option 
We are still getting a bunch of warnings because of dynamic_library.cpp.
I will fix this later.
 2017-01-14 08:23:51 -08:00
Leonardo de Moura
0a63133abe chore(.appveyor.yml): missing DLLs 2017-01-14 07:47:38 -08:00
Leonardo de Moura
6a5d3ed0e5 feat(library/vm/vm_string): use check_system to avoid stack overflow 2017-01-13 17:06:24 -08:00
Leonardo de Moura
05d86e49ca feat(library/init/meta/smt): add intros variants for smt_tactic 2017-01-13 16:13:37 -08:00
Leonardo de Moura
db646dda89 fix(library/tactic/smt/smt_state): forgot to set zeta option 2017-01-13 13:33:47 -08:00
Scott Morrison
6f8fc0fe06 fix(library/scoped_ext): typo in error message 2017-01-13 11:33:17 -08:00
Leonardo de Moura
52164d56b9 chore(tests/shell/shell): style 2017-01-13 07:39:06 -08:00
Leonardo de Moura
fbc5f7a5fa chore(util/lean_path): compilation warning 2017-01-13 07:36:24 -08:00
Sebastian Ullrich
e4ec1808f3 fix(util/lean_path): find_imports: .olean files and default modules 2017-01-13 07:34:54 -08:00
Sebastian Ullrich
b180c54c0e feat(shell): move lean.js to server mode 2017-01-13 07:34:54 -08:00
Sebastian Ullrich
222952d5b8 chore(frontends/lean/scanner): another CLion fix 2017-01-13 07:34:54 -08:00
Leonardo de Moura
c1ecaf4edd feat(library/tactic/smt/smt_state): do not apply intros automatically in begin[smt]...end blocks 2017-01-12 21:49:17 -08:00
Leonardo de Moura
30cea2dceb fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions. 
The new test exposes the problem.
 2017-01-12 18:38:31 -08:00
Gabriel Ebner
ab539971a6 fix(emacs/lean-flycheck): only update next-error-mode for current buffer 2017-01-12 13:51:43 -08:00