Leonardo de Moura
7bffcf776b
chore(library/mt_task_queue, library/task_queue): style
2016-12-08 09:26:22 -08:00
Daniel Selsam
6120f8cc9f
fix(src/library/tactic/simplify): relaxed_whnf when checking if fn is dependent
2016-12-08 07:41:42 -08:00
Leonardo de Moura
7b63d6566f
fix(util/dynamic_library): throwing exception inside destructor may crash application
2016-12-08 07:16:43 -08:00
Gabriel Ebner
5ee7076ae9
fix(emacs): update readme
2016-12-08 07:14:55 -08:00
Gabriel Ebner
60f0f30c5c
fix(tests/shared/thread): fix single-threaded build
2016-12-08 07:13:48 -08:00
Gabriel Ebner
bd69544663
fix(emacs/lean-server): start server in the directory of the file
2016-12-06 17:45:12 -08:00
Leonardo de Moura
58768940e3
chore(shell/server): std::make_unique is a C++14 feature
...
I got a compilation error
2016-12-06 17:22:24 -08:00
Gabriel Ebner
45d0525e52
feat(shell,emacs): new lean server protocol
2016-12-06 17:14:29 -08:00
Gabriel Ebner
61b70a71ce
refactor(shell/server): move auto-completion code to a separate file
2016-12-06 17:14:29 -08:00
Gabriel Ebner
ddf103a48d
feat(shell/server): support multiple files
2016-12-06 17:14:29 -08:00
Leonardo de Moura
278e960a6b
feat(library/type_context): add support for offset constraints in the unifier
...
see discussion at #1226
2016-12-06 16:51:00 -08:00
Leonardo de Moura
4ef901abb4
chore(src/util/dynamic_library): fix style warning
2016-12-06 15:25:41 -08:00
Leonardo de Moura
5c2d87ef87
fix(library/native_compiler/native_compiler): compilation error
2016-12-06 13:16:56 -08:00
Leonardo de Moura
9aa77bfdb0
feat(library/util): add mk_nat
2016-12-06 00:16:31 -08:00
Leonardo de Moura
72ce00d3d0
fix(library/type_context): assertion violation at unification hints
2016-12-06 00:16:31 -08:00
Leonardo de Moura
ef6d6075bb
fix(library/native_compiler/native_compiler): add -ldl option
2016-12-05 17:33:34 -08:00
Leonardo de Moura
6684cd40ea
fix(util/dynamic_library): Windows issue
2016-12-05 17:16:48 -08:00
Leonardo de Moura
a4218c4313
fix(shared/init): shared library initialization
2016-12-05 16:48:29 -08:00
Leonardo de Moura
378856fdb9
chore(*): comment native compiler tests
...
They do not work in all platforms.
2016-12-05 16:42:40 -08:00
Leonardo de Moura
e59515df5f
chore(*): fix style
2016-12-05 16:39:58 -08:00
Jared Roesch
e65d90ac79
feat(*): C++ code generator
...
in progress move of Lean.native to init
2016-12-05 16:11:41 -08:00
Gabriel Ebner
d5372e770f
fix(shell/lean): wait for all tasks to finish
2016-12-05 13:26:00 -08:00
Gabriel Ebner
e07cdcb063
fix(shell/lean): nicer error message for file not found
2016-12-05 13:26:00 -08:00
Gabriel Ebner
6bfbb79d6e
fix(shell/lean): add missing colon to 'A' option
2016-12-05 13:26:00 -08:00
Leonardo de Moura
f96d35dc1c
fix(library/aux_definition,frontends/lean/definition_cmds): unfold macros at trust level 0
2016-12-05 13:08:12 -08:00
Gabriel Ebner
570d905282
chore(util/thread): do not import chrono twice
2016-12-05 12:57:15 -05:00
Gabriel Ebner
b3b8330909
fix(CMakeLists): disable automatic thread finalization in single-threaded builds
2016-12-05 12:57:14 -05:00
Leonardo de Moura
c77a987b4d
feat(util/thread): handle thread creation/join failure on Windows
2016-12-05 09:53:41 -08:00
Leonardo de Moura
612cde33b6
feat(util/thread): lthread for Windows
2016-12-05 09:42:21 -08:00
Leonardo de Moura
f9a0029a47
chore(tests/util/thread): enable test on OSX
2016-12-05 09:24:17 -08:00
Leonardo de Moura
80d247eaff
fix(src/util): make sure thread stack size is > LEAN_STACK_BUFFER_SPACE
2016-12-03 12:05:01 -08:00
Leonardo de Moura
8e64665259
chore(src/CMakeLists): remove support for optional Boost
2016-12-03 11:34:58 -08:00
Leonardo de Moura
a9d3f36f76
feat(util/thread,library/mt_task_queue): add lthread
2016-12-03 11:29:22 -08:00
Leonardo de Moura
aea8fd943e
fix(library/mt_task_queue): save stack info at thread starting
...
We need this information to get accurate stack information.
2016-12-02 20:01:32 -08:00
Gabriel Ebner
bbbc790cfc
feat(.travis.yml): add codecov
2016-12-02 17:01:58 -08:00
Gabriel Ebner
eea7475e57
refactor(.travis.yml): simplify travis config
2016-12-02 17:01:58 -08:00
Gabriel Ebner
7db2b8d014
fix(library/vm/vm): do not segfault in single-threaded builds
2016-12-02 16:51:10 -08:00
Gabriel Ebner
92f07720f2
refactor(emacs/load-lean): install emacs dependencies directly from (M)ELPA
2016-12-02 16:50:50 -08:00
Gabriel Ebner
9ecac28061
feat(CMakeLists,util/thread): fix build with boost
2016-12-02 16:50:03 -08:00
Gabriel Ebner
c8a821afd1
fix(library/module_mgr): do not create olean files for modules with errors
2016-12-02 16:48:18 -08:00
Leonardo de Moura
e11fd8820a
refactor(library/init): create init.data folder
2016-12-02 14:23:06 -08:00
Leonardo de Moura
e237109434
fix(frontends/lean/tactic_notation): do not store position information for auxiliary terms introduced by the interactive mode
...
The idea is to prevent unwanted type information at lean-mode.
For example, before this commit, we would get "list.nil : ..." type
info whenever we hovered over the "end" of a "begin...end" block.
2016-12-02 09:53:24 -08:00
Gabriel Ebner
851b64dbbd
feat(library/module_mgr): gracefully handle non-existing imports
2016-12-02 08:47:59 -08:00
Gabriel Ebner
26f0325e9b
fix(shell/server): do not fail if module parsing throws an exception
2016-12-02 08:47:46 -08:00
Gabriel Ebner
a3daaee2e0
fix(library/mt_task_queue): reverse dependencies may already be queued
...
When we check whether the dependencies for a task have already been
evaluated and then accordingly move the task from waiting to queued, we
do not remove it from the reverse dependency lists it appears in.
2016-12-01 17:43:53 -08:00
Leonardo de Moura
e1a90fbe89
fix(frontends/lean/tactic_notation): fixes #1207
2016-12-01 17:16:22 -08:00
Leonardo de Moura
8defd9ac39
fix(frontends/lean/elaborator): compilation warning with clang
2016-12-01 16:10:07 -08:00
Leonardo de Moura
79d87138f0
feat(util/memory): simplify memory tracking code
2016-12-01 16:07:46 -08:00
Leonardo de Moura
10f51156b2
chore(CMakeLists): remove obsolete option
2016-12-01 14:07:56 -08:00
Gabriel Ebner
cc9f52ade6
refactor(library/mt_task_queue): more precise task_result_states
...
The task result state now distinguishes created/waiting/queued, which is
useful for debugging. mt_task_queue now also correctly waits for all
tasks during destruction.
2016-12-01 11:06:08 -08:00
