Commit graph

129 commits

Author SHA1 Message Date
Leonardo de Moura
405e57eb2d refactor(kernel/formatter): add formatter_factory, and simplify formatter interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 18:32:00 +01:00
Leonardo de Moura
2ef7b9be2f feat(frontends/lean): add basic pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 01:12:36 -07:00
Leonardo de Moura
e445515f2b refactor(kernel): move standard and hott kernel instantiations to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 10:31:27 -07:00
Leonardo de Moura
abe12b0631 fix(shell/lean): only save .olean file if there are no errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:04:18 -07:00
Leonardo de Moura
cf28981f45 feat(tests/lean/run): add test_single script that sets the LEAN_PATH
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 07:47:46 -07:00
Leonardo de Moura
65c63e146f feat(frontends/lean): add display_deps function, and --deps command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 18:35:18 -07:00
Leonardo de Moura
3ea24c0f32 fix(library/kernel_bindings): set_environment and set_io_state objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:36:47 -07:00
Leonardo de Moura
b9a7cc41ef feat(shell): use system_import for lua files provided in the command line (i.e., their code will be available for all threads)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:04:09 -07:00
Leonardo de Moura
1378fa5cbb refactor(util/script_state): remove support for threads and communication channels from the Lua API, the goal is to keep is simple, and use one Lua state object per thread
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 21:56:45 -07:00
Leonardo de Moura
73b7a44c84 fix(shell/CMakeFiles): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:55:16 -07:00
Leonardo de Moura
a964ceb0e2 feat(frontends/lean): add 'import' command, add command line option for setting number of threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:37:46 -07:00
Leonardo de Moura
79d32b768d feat(shell): add '--hott' command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 15:50:27 -07:00
Leonardo de Moura
9931033554 feat(shell/lean): remove --olean option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 10:50:35 -07:00
Leonardo de Moura
891a3fb48b feat(frontends/lean): add command block reader with snapshot and resume
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 14:13:32 -07:00
Leonardo de Moura
5fee6fd140 feat(shell/lean): add '-o' command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 08:10:43 -07:00
Leonardo de Moura
cffbae3667 test(tests/lean/run): add new test group, where we just execute Lean (and don't check output)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 21:07:23 -07:00
Leonardo de Moura
05edbe00ad chore(shell): re-activate .lean tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:36:42 -07:00
Leonardo de Moura
2e8ebb6d9e feat(frontends/lean/parser): add 'parse_commands' and 'parse_script'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:32:07 -07:00
Leonardo de Moura
0f894f4618 chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 17:47:53 -07:00
Leonardo de Moura
045a83153c doc(lua): update Lua API documentation, and reactivate doc tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 08:09:54 -07:00
Leonardo de Moura
bb9830f10c test(shell): add command line tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:53:04 -07:00
Leonardo de Moura
813eba6b3a chore(build): add Lua thread tests to test suite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:53:36 -07:00
Leonardo de Moura
3e222e2f22 refactor(kernel/formatter): add environment as an extra argument to the formatter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-30 10:28:07 -07:00
Leonardo de Moura
f7e705badb refactor(library/kernel_bindings): reactive some of the kernel Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 11:52:09 -07:00
Leonardo de Moura
a6116e3156 test(lua): reactivate some of the Lua unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 10:36:57 -07:00
Leonardo de Moura
af927ecb7a refactor(frontends/lua): reactivate some of the Lua extensions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 17:57:39 -07:00
Leonardo de Moura
2a59beee0a feat(shell): reactivate lean shell, only Lua frontend is working
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 17:49:23 -07:00
Leonardo de Moura
d79e9af210 fix(frontends/lean): help msg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-18 09:31:30 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 16:54:21 -08:00
Leonardo de Moura
35bacf95fc feat(shell): provide the default environment when parsing Lua files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:21:14 -08:00
Leonardo de Moura
582569b793 feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 16:46:53 -08:00
Leonardo de Moura
5fb718c03a fix(build): broken dependencies between lean executable and .olean, *_decls.cpp and *_decls.h files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-10 10:58:35 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 15:31:58 -08:00
Leonardo de Moura
8c41b4e899 feat(build): run tests using -t
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 14:12:32 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:01:27 -08:00
Leonardo de Moura
2cd2527d9f refactor(shell): move read-eval-loop script to repl.lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 16:56:22 -08:00
Leonardo de Moura
9d6bd7501c feat(doc/lean): include lean documentation scripts in the test set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:16:47 -08:00
Leonardo de Moura
ecc5d1bc3a refactor(kernel): move printer to library, cleanup io_state interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 13:37:50 -08:00
Leonardo de Moura
0592261847 refactor(kernel/io_state): move io_state_stream to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 13:14:21 -08:00
Leonardo de Moura
7d18e9b32e refactor(frontends/lean/parser): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 04:37:21 -08:00
Leonardo de Moura
ecd62a1783 refactor(builtin/basic): rename basic.lean to kernel.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:46:03 -08:00
Leonardo de Moura
72761f14e4 refactor(library/io_state): move to the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:20:23 -08:00
Leonardo de Moura
8ff919ef2a chore(build): remove dead dependency
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:49:22 -08:00
Leonardo de Moura
6633dff46f fix(build): githash generation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:41:28 -08:00
Leonardo de Moura
f7889511f9 fix(build): cycle triggered by githash.h dependencies
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 12:47:25 -08:00
Leonardo de Moura
9fdf2a3f55 feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules
"Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip
type checking when importing these files.
TODO: add a check-sum.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:43:53 -08:00
Leonardo de Moura
411ebbc3c1 refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:04:49 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 19:20:04 -08:00
Leonardo de Moura
aee1c6d3f3 feat(kernel): export/import (.olean) binary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 17:31:35 -08:00
Leonardo de Moura
99f9478d93 feat(build): cpack support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 16:18:51 -08:00