Sebastian Ullrich
ba1b6165e3
feat(frontends, shell): implement basic server 'info' command
2016-11-08 08:37:41 -08:00
Leonardo de Moura
9465f25f09
feat(library/vm): profiler for VM bytecode
2016-11-03 21:15:29 -07:00
Gabriel Ebner
47e6fd091f
refactor(frontends/lean): implement show goal function using exceptions
2016-10-21 15:42:29 -07:00
Sebastian Ullrich
f10d5e4d8c
fix(library/vm/vm_io): disable get_line in server mode
2016-10-19 10:02:58 -07:00
Gabriel Ebner
db766b2f5a
chore(shell/lean): fix coding style
2016-10-16 14:41:35 -07:00
Gabriel Ebner
ec0aa6d248
refactor(*): integrate emscripten build
2016-10-16 14:41:35 -07:00
Leonardo de Moura
541e9010e1
fix(shell/lean): disable initialize/finalize server when -DSERVER=OFF is used
2016-10-14 12:56:50 -07:00
Sebastian Ullrich
7e570d7777
feat(shell/server, emacs): bring back basic completion
2016-10-14 11:53:00 -07:00
Leonardo de Moura
936eb76466
feat(CMakeFiles): add -DSERVER=OFF cmake option
...
Motivation: we can disable lean-server and the json dependency when compiling lean.js.
2016-10-14 11:48:02 -07:00
Leonardo de Moura
0bb155a427
chore(*): remove .clean support
...
In Lean2, we used to cache elaborated definitions in .clean files. The
main goal was to optimize each flycheck invocation produced by Emacs.
The Lean3 definition package was not updating this cache. Moreover, it
is not necessary because the new compilation server subsumes it.
2016-10-13 19:58:58 -07:00
Leonardo de Moura
3162bac4e7
feat(shell/lean): disable assertion violation dialog in server mode
2016-10-13 18:56:10 -07:00
Gabriel Ebner
ba74530cc0
chore(*): remove legacy flycheck support
2016-10-13 18:49:10 -07:00
Gabriel Ebner
46eefdac89
feat(emacs/lean-server): support files in projects
2016-10-13 18:49:10 -07:00
Gabriel Ebner
d78a2171ec
feat(shell/server): first version of the compile server API
2016-10-13 18:49:10 -07:00
Gabriel Ebner
bd09d8febe
feat(shell/json): json-formatted error messages
2016-10-13 18:49:10 -07:00
Gabriel Ebner
66be9c31db
refactor(library/flycheck): use flycheck_message_stream instead of option
2016-10-13 18:49:10 -07:00
Gabriel Ebner
5acb722d46
refactor(library/flycheck,library/trace): convert trace output to messages independently of flycheck
2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2
refactor(*): structured message objects
2016-10-13 18:49:10 -07:00
Leonardo de Moura
9ef3ebbd5b
refactor(*): delete HoTT support
2016-09-27 16:33:39 -07:00
Leonardo de Moura
6d9a9b46f3
chore(frontends/lean): cleanup
2016-09-23 16:26:21 -07:00
Leonardo de Moura
b2e1e920a9
chore(frontends/lean,library,linja): remove .ilean files
2016-09-20 08:43:45 -07:00
Leonardo de Moura
a1d36b6c4d
chore(library): remove legacy_type_context
2016-09-19 21:31:21 -07:00
Leonardo de Moura
2a069a4d2a
chore(frontends/lean): remove server and info_manager
2016-09-19 18:44:03 -07:00
Leonardo de Moura
803c956d18
feat(util/sexpr/option_declarations): allow options to be registered after initialization
2016-08-19 16:58:30 -07:00
Daniel Selsam
e946ebc8fc
feat(frontends/smt2): new frontend for smt2 format
2016-07-29 10:44:43 -07:00
Leonardo de Moura
487a1e7f89
refactor(kernel): remove extension_context
...
We replaced it with abstract_type_context
2016-03-19 15:15:39 -07:00
Leonardo de Moura
eaac6ba721
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
2016-03-04 10:26:50 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Leonardo de Moura
b92416d66c
refactor(library/error_handling): move error_handling to library main dir
2015-12-29 15:31:40 -08:00
Leonardo de Moura
edad31a9b1
feat(shell/lean): use locking also for the index file
2015-12-12 21:50:08 -08:00
Leonardo de Moura
4dc3764a02
feat(util,library,shell): basic locking mechanism
...
We still have to test on Windows.
see issue #925
2015-12-12 21:26:13 -08:00
Leonardo de Moura
7eb1525ba5
feat(shell/lean): add option '--debug=tag' for activating conditional assertions in the command line in debug mode
2015-12-06 15:47:26 -08:00
Leonardo de Moura
f78e57fd52
feat(shell,frontends/lean): add command line option --dir
...
See #821
See #788
2015-11-19 08:34:23 -08:00
Leonardo de Moura
cc4f18c062
feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information
...
see issue #756
2015-07-30 10:18:03 -07:00
Leonardo de Moura
ad5d792a8e
feat(library,shell): add --export-all command line option
2015-07-28 15:54:44 -07:00
Leonardo de Moura
b4504357b2
fix(shell/lean): do not update cache file in query mode
...
query mode is "show goal" and "show hole" command line options
2015-07-27 19:00:36 -07:00
Leonardo de Moura
3fb16d6287
feat(frontends/lean): add "show hole" command line option
2015-07-27 18:42:57 -07:00
Leonardo de Moura
68370d5c8e
feat(frontends/lean): process "show goal" command line option
2015-07-27 17:44:43 -07:00
Leonardo de Moura
6da49b1d56
fix(shell/lean): fixes #710
2015-06-26 19:15:47 -07:00
Leonardo de Moura
a24b06254b
test(tests/shell): add unit test for emscripten_shell
2015-06-18 10:20:26 -07:00
Leonardo de Moura
a6fe4cbce6
refactor(shell): move emscripten_shell to a separate file
2015-06-18 09:53:23 -07:00
Leonardo de Moura
701b0ae66f
feat(library): export environment in textual format
...
closes #577
2015-05-04 18:05:00 -07:00
Leonardo de Moura
88023e9597
fix(shell/lean): missing 'break'
2015-04-27 14:23:01 -07:00
Leonardo de Moura
68383d49de
refactor(shell/lean): remove useless output
...
It was added for implementing the web version, and avoid the need to
simulate a file system in the web browser.
It turns out we decided to use a virtual file system.
2015-04-27 10:15:01 -07:00
Leonardo de Moura
68d4978953
feat(shell/lean): trap 'std::bad_alloc' and print nicer error message
...
See #489
2015-04-20 17:55:00 -07:00
Leonardo de Moura
26c914173c
feat(frontends/lean): add --profile option
2015-03-31 11:53:55 -07:00
Leonardo de Moura
9119c3f9fb
fix(shell/lean): uninitialized variable
2015-03-24 18:36:14 -07:00
Leonardo de Moura
1e13f383f6
feat(shell/lean): add --line, --col and --goal options for testing Emacs interface
2015-03-24 12:29:31 -07:00
Leonardo de Moura
f24d9e84fe
feat(frontends/lean): add option 'max_memory'
...
Default value is 512Mb
2015-03-06 13:56:20 -08:00
