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

180 commits

Author SHA1 Message Date
Sebastian Ullrich
c88784ef9d refactor: consistent io_result_mk* naming 
/cc @leodemoura
 2020-08-31 11:08:57 +02:00
Sebastian Ullrich
c38f4fe837 feat: unsafe functions for freeing compacted regions 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
ebd72d200f fix: alloc/free mismatch detected by asan 2020-07-10 07:42:26 -07:00
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Sebastian Ullrich
f6973be5e3 refactor: replace C++ import parser with Lean one 
imports are now completely opaque to C++
 2019-11-21 15:52:01 +01:00
Sebastian Ullrich
3dcd4febd9 feat: make LEAN_PATH a mapping from package names to root dirs, remove C++ impl 2019-11-20 16:39:53 +01:00
Leonardo de Moura
30571f12d4 chore: adjust runtime to new EState 2019-10-21 17:05:16 -07:00
Leonardo de Moura
dcd15f3424 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Leonardo de Moura
a5c97e21bf chore(library/init/lean): export as C functions 2019-08-16 20:15:30 -07:00
Sebastian Ullrich
d09c512784 chore(library/module): lsan: ignore module objects 2019-07-30 17:52:43 -07:00
Leonardo de Moura
ff6b868440 chore(library/module): remove dead code 2019-07-27 19:03:07 -07:00
Sebastian Ullrich
7b18bc94fd fix(library/module): make sure header length preserves alignment 2019-07-26 12:39:35 -07:00
Sebastian Ullrich
53a26b94ff chore(util/lean_path): remove leanpkg.path support 
Because Lean 4 will not compile dependencies by itself, there is not much of a
point in it resolving them by itself either. The build tool that ensures that
all dependencies have been built should call `lean` with the `LEAN_PATH`
environment variable set accordingly.
 2019-07-25 17:46:40 -07:00
Leonardo de Moura
cf8daf4b24 feat(library/init/lean/elaborator): process header 
TODO:
- improve/fix `setSearchPath`
- add `IO.getEnv`
- add support for relative imports at `absolutizeModuleName`
 2019-07-24 07:37:33 -07:00
Leonardo de Moura
fd29b7e45d feat(util/io): add helper functions for consuming IO results in C++ 2019-06-05 13:53:38 -07:00
Leonardo de Moura
aa138fe686 chore(*): get_obj_arg => to_obj_arg 2019-05-16 14:42:02 -07:00
Leonardo de Moura
5df0b05cc7 chore(library/init/lean/environment): remove get_modifications_core 2019-05-14 11:26:04 -07:00
Leonardo de Moura
7696c28fe1 feat(library/module): module manager in Lean is alive 2019-05-14 11:10:49 -07:00
Leonardo de Moura
642c4c59bd feat(library/init/lean/environment): support for serializing/performing legacy modification objects 2019-05-14 10:08:31 -07:00
Leonardo de Moura
67d14705b0 chore(library/module): simplify write_module 2019-05-14 08:08:09 -07:00
Leonardo de Moura
427852d759 feat(library/init/lean/environment): add findOLean 2019-05-14 08:02:26 -07:00
Leonardo de Moura
e616def866 chore(library/module): remove dead declaration 2019-05-14 07:53:44 -07:00
Leonardo de Moura
22d2848d21 chore(library/module): store search_path in a global variable 
Remark: I will use it to expose the following primitive in Lean
```
constant findOLean : Name -> IO String
```
 2019-05-14 07:49:00 -07:00
Leonardo de Moura
1a610607b1 chore(library/module): remove old comment 2019-05-14 07:37:20 -07:00
Leonardo de Moura
358b731581 chore(library/module): simplify import_modules 
Remark: `lean.cpp` is a total mess at this point. It contains
leftovers from the Lean2 and Lean3 designs, and hacks for supporting
the Lean4 transition.
 2019-05-14 07:26:50 -07:00
Leonardo de Moura
9596fae665 chore(library/module): remove import errors 2019-05-14 07:13:50 -07:00
Leonardo de Moura
53ec9ee181 chore(*): style 2019-05-14 07:08:58 -07:00
Leonardo de Moura
5844913102 feat(library/module, library/init/lean/environment): add primitives for reading/writing files as compacted regions 2019-05-13 17:26:28 -07:00
Leonardo de Moura
40f9704540 chore(library/init/lean/environment): add placeholders for writing/reading .olean files 2019-05-13 15:48:23 -07:00
Leonardo de Moura
31d140adab refactor(library/module): use Lean modification list environment extension 2019-05-13 15:26:28 -07:00
Leonardo de Moura
3b3e50d315 chore(library/module): std::shared_ptr<modification> ==> modification* 
Remark: this commit introduce memory leaks, but this is just an
intermediate step to get modification objects in Lean.
Recall that, we will eventually remove modification objects from Lean.
 2019-05-13 15:05:21 -07:00
Leonardo de Moura
2e3604e80a chore(library/module): remove unnecessary field module_ext::m_imported 2019-05-13 14:34:03 -07:00
Leonardo de Moura
edb4d76ecd feat(kernel/environment): environment as a Lean object 2019-05-13 12:41:33 -07:00
Leonardo de Moura
06390337c6 chore(library/module): fix linker error 2019-05-11 17:08:58 -07:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Sebastian Ullrich
2d9a16fd24 refactor(library/module_mgr): remove 2019-01-25 20:12:11 +01:00
Leonardo de Moura
e0bb21ba0b chore(library): remove noncomputable module 2018-10-22 09:39:03 -07:00
Leonardo de Moura
77e3c18cb0 feat(library/module): noncomputable keyword is now used only to disable code generation 
We do not try to check whether code generation will succeed or not for
some declaration. In the future, we should probably rename it to
`nocode` or something similar.

cc @kha
 2018-10-22 09:35:05 -07:00
Sebastian Ullrich
15d11cc483 feat(library/module_mgr): profile .olean serialization/deserialization 2018-09-20 13:54:17 -07:00
Leonardo de Moura
5d455bf10a chore(library/compiler): skip type checking for _cstage1 declarations 
This is a temporary hack for speeding up build time.
 2018-09-17 14:45:04 -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
38208802c6 refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous 2018-09-11 13:55:25 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
101886ffae feat(kernel): proper constant_info and declaration objects for quot type 2018-08-28 13:46:31 -07:00
Leonardo de Moura
161431e995 feat(kernel): implement new mutual_definition declaration object 
This commit also removes the old `environment::add_meta` hackish method.
 2018-08-28 10:30:44 -07:00
Leonardo de Moura
cdb2824d86 fix(library/module): debug build 2018-08-28 08:09:57 -07:00
Leonardo de Moura
776c977742 refactor(kernel): continue constant_info/declaration refactoring 2018-08-27 17:23:26 -07:00