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

262 commits

Author SHA1 Message Date
Gabriel Ebner
46eefdac89 feat(emacs/lean-server): support files in projects 2016-10-13 18:49:10 -07:00
Gabriel Ebner
9c520e3096 feat(shell/server): use parser snapshots 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
2969d8a8c6 chore(shell/CMakeLists): remove old tests 2016-09-19 18:44:03 -07:00
Leonardo de Moura
24f1cb2726 chore(frontends/lean): new_elaborator is now the default 2016-09-19 16:34:06 -07:00
Leonardo de Moura
29b35ef12d chore(tests/lean/hott): delete old HoTT tests 2016-09-17 12:26:11 -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
4f8db64e23 refactor(simplifier): many fixes, extensions, and tests 
fix(simplifier): missing simp rule in prop simplifier
fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
 2016-08-19 14:57:03 -07:00
Leonardo de Moura
f3dbd0c69a chore(library): disable stdlib but init and systems folder 2016-08-11 18:42:10 -07:00
Leonardo de Moura
dc44edfd41 feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
Daniel Selsam
79e5e80dae test(frontends/smt2): basic tests for parser and elaborator 2016-07-29 10:44:44 -07:00
Daniel Selsam
e946ebc8fc feat(frontends/smt2): new frontend for smt2 format 2016-07-29 10:44:43 -07:00
Leonardo de Moura
0ef4bea86b chore(tests/lean): disable tests 2016-06-10 18:29:41 -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
9d0dfb8404 refactor(frontends/lean): remove calc_proof_elaborator 2016-03-03 17:22:45 -08:00
Leonardo de Moura
4a43e33d45 chore(*): disable big chunk of the standard library and tests 2016-03-03 13:43:08 -08:00
Leonardo de Moura
f0158ba20c chore(CMakeLists): disable HoTT library and tests 2016-03-03 12:51:10 -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
6df31d3406 refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading 2015-11-08 14:04:56 -08:00
Soonho Kong
a25b43f1e8 feat: do not generate leanstatic.a in EMSCRIPTEN build 2015-11-03 18:22:05 -05:00
Leonardo de Moura
2b52198702 fix(library/unfold_macros): fixes #806 2015-08-18 17:46:47 -07:00
Leonardo de Moura
498afc1e6f feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07: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
ed41a01a51 fix(frontends/lean/elaborator): fixes #755 2015-07-29 16:41:30 -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
cfa9412f96 fix(frontends/lean): "show goal" localization, add "position", support "by tactic" 2015-07-28 12:48:12 -07:00
Leonardo de Moura
08b23d8b4f test(tests/lean/extra): add test for "show goal" feature 2015-07-27 21:03:16 -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
a99c44b644 fix(CMakeLists.txt): disable problematic tests on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-07-20 08:14:31 -07:00
Leonardo de Moura
6da49b1d56 fix(shell/lean): fixes #710 2015-06-26 19:15:47 -07:00
Leonardo de Moura
42c236eb2e chore(shell/emscripten): fix style 2015-06-18 10:23:49 -07:00
Leonardo de Moura
a24b06254b test(tests/shell): add unit test for emscripten_shell 2015-06-18 10:20:26 -07:00