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

491 commits

Author SHA1 Message Date
Sebastian Ullrich
7d82149231 feat(shell/lean): bring back --deps option 2018-10-19 09:52:01 +02:00
Sebastian Ullrich
95c469f8c4 fix(library/module_mgr,shell/lean): catch all errors from parsing 2018-09-25 12:14:03 -07:00
Sebastian Ullrich
896b45239e feat(library/module_mgr,shell/lean): abort on import with errors 2018-09-20 15:46:47 -07:00
Leonardo de Moura
1be71cf725 chore(shell/lean): fix unused variable warning 2018-09-12 16:51:59 -07:00
Sebastian Ullrich
75b2b09c08 feat(library/module_mgr): 'trace.import' trace class 2018-09-12 09:14:58 -07:00
Sebastian Ullrich
62671c8b6f fix(shell/lean): Flycheck doesn't ignore stderr 2018-09-12 08:29:21 -07:00
Sebastian Ullrich
52d4cc10ad feat(shell/lean,lean4-mode/lean4-flycheck): use stdin for communication 
no more `flycheck_` files
 2018-09-11 16:35:25 -07:00
Sebastian Ullrich
af99f153f8 refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
716de48078 chore(library/module): remove loaded_module.m_env 
It was used by `--run` only, which I guess will change quite a bit anyway
 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
904d7c4a88 chore(*): remove old task API and task queues 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af55cb13e7 fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6 refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
b3c44ec56e chore(shell/{server,lean_js}): remove 2018-09-08 18:37:58 -07:00
Leonardo de Moura
81a694e73c chore(frontends/lean): remove dead code 2018-09-08 15:44:49 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
78f4edaf57 chore(frontends/lean): remove info_manager and interactive modules 2018-09-04 17:22:16 -07:00
Leonardo de Moura
82095cc018 refactor(kernel): split declaration into declaration and constant_info 
This is just another step towards the design described at commit 16598391a07d4a
 2018-08-22 17:53:11 -07:00
Leonardo de Moura
9d35d31529 refactor(kernel): merge constant_assumption and axiom 2018-08-01 09:57:47 -07:00
Leonardo de Moura
9626ad919c chore(library/export): remove text export module 
This can be implemented in Lean.
 2018-06-08 13:36:36 -07:00
Leonardo de Moura
45da5872e6 chore(checker): remove leanchecker 2018-06-07 16:28:54 -07:00
Leonardo de Moura
2a79da1ab6 refactor(kernel): move formatting stuff out of the kernel 2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
ac0352b584 refactor(kernel): remove quotitent normalizer extension 
The `quot` type is now implemented in the kernel.
We will do the same thing for inductives.
We will not support normalizer extensions anymore in Lean4.
It doesn't make sense since we settled with 2 extensions: quotients and
inductives. Moreover, any new extension would require substantial
changes (e.g., code generator).
The normalizer_extension feature was useful when we were experimenting
with different kernel flavors.
 2018-06-01 10:52:17 -07:00
Leonardo de Moura
3c1ccc9b74 refactor(kernel): use m_meta instead of m_trusted 2018-05-31 11:18:00 -07:00
Leonardo de Moura
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
0556412f8d refactor(*): add runtime folder 
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
 2018-05-14 14:23:56 -07:00
Sebastian Ullrich
2b1e207e02 chore(shell/CMakeLists): disable leanpkg tests 2018-04-12 13:54:49 +02:00
Leonardo de Moura
6234c60aae chore(*): disable test suite 2018-04-10 12:56:55 -07:00
Leonardo de Moura
b14d69b1d7 chore(*): remove converter, ac_tactics, hole_commands, rbtree/rbmap proofs, bitvec 2018-04-10 12:25:51 -07:00
Sebastian Ullrich
340e056dee chore(shell/CMakeLists): copy mpir.dll when building with MSVC 
Also simplify code a bit
 2018-03-08 10:30:47 -08:00
Sebastian Ullrich
854475808d chore(shell/CMakeLists): make bin/lean a proper target 
This ensures that it will be re-copied when removed, which is a quick way of
switching between debug and release builds.
 2018-03-08 10:30:38 -08:00
Sebastian Ullrich
191d1e7321 chore(shell/server): sync_output command for debugging 2018-03-08 10:06:09 -08:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Sebastian Ullrich
f247363305 feat(library/time_task): print cumulative times on --profile 2018-02-19 09:13:24 -08:00
Leonardo de Moura
3771748b4c chore(library/native): remove dead code 
The deleted code was not finished, and we are going to add a new IR
and compiler.
 2018-02-07 17:29:25 -08:00
Nuno Lopes
a69541ab67 fix(msvc): crashes in getopt and read_dir 2018-02-06 10:11:10 -08:00
Nuno Lopes
36f19f1d6e fix(msvc): fix a few more compilation errors 2018-02-06 10:11:10 -08:00
Nuno Lopes
93374bb2bc fix(msvc): add a simple getopt() implementation 2018-02-06 10:11:10 -08:00
Nuno Lopes
7f920d9d37 fix(build): regression in linux build 2018-02-06 10:11:10 -08:00
Sebastian Ullrich
fe2e95def3 fix(library/module_mgr): Revert "feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode" 
This reverts commit 18c2e3739a.
The change introduced a bug where a .olean file may have been saved even if
the corresponding module had produced errors during processing, as long as these
errors were not part of the current region of interest.
 2018-02-05 14:36:27 +01:00
Leonardo de Moura
1e626e382f chore(frontends/smt2): remove SMT2 frontend 2018-01-24 15:21:52 -08:00
Leonardo de Moura
0d83a74b26 fix(library/io,tests/lean): io monad command line arguments, and tests 2018-01-23 15:24:41 -08:00
Leonardo de Moura
0ad5497462 refactor(library/io): make io easier to extend and use 2018-01-23 15:03:31 -08:00
Sebastian Ullrich
18c2e3739a feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode 
Note, currently there is no way for a dirty file to become non-dirty again
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
67fc899d0d feat(shell/server): sync: default "content" to file content 
This mostly simplifies debugging and testing
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
e8c057f1de refactor(library/module_mgr): simplify module loading code 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
1ee945a31f fix(library): store and validate Lean version of .olean files 
Fixes #1770
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
37e2f085e4 chore(shell/CMakeLists): leanpkg integration tests 2017-12-30 19:31:55 +01:00
Sebastian Ullrich
adc0d250fc fix(shell/lean): show progress messages only when stdout is a terminal 2017-12-30 17:39:53 +01:00
Gabriel Ebner
8837ce0f31 fix(shell/lean): add missing newline 2017-08-29 16:40:04 +02:00