Sebastian Ullrich
2d9a16fd24
refactor(library/module_mgr): remove
2019-01-25 20:12:11 +01: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
43e57358af
refactor(library/module_mgr): minor refactorings
2018-09-11 13:55: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
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
ae18cee0ea
chore(library/module): remove pos_info tracking
...
We will use a completely different approach in Lean4
2018-08-27 15:55:57 -07:00
Leonardo de Moura
2ab2265d22
chore(library/module): remove dead APIs
2018-08-27 15:40:20 -07:00
Leonardo de Moura
dec166b387
chore(library/module): remove dead info
2018-08-27 15:35:10 -07:00
Leonardo de Moura
f3e99286bb
chore(kernel): remove certified_declaration
2018-08-22 12:11:34 -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
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
eab962bbc6
feat(kernel): add add_meta
2018-05-31 15:40:50 -07:00
Leonardo de Moura
cab6b39c76
refactor(library): remove sorry checking
...
We have to revise how we do this.
2018-05-31 15:20:39 -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
1ee945a31f
fix(library): store and validate Lean version of .olean files
...
Fixes #1770
2018-01-23 11:14:18 -08:00
Gabriel Ebner
4a6513e5f5
refactor(util/serializer,library/module): use basic_ostream::write for the olean code
2017-06-23 15:13:40 +02:00
Leonardo de Moura
24048c4258
fix(*): gcc 7 weird uninitialized warnings
...
I think most of them are incorrect.
I didn't find a workaround for the one at json.hpp.
So, I just disabled this warning at server.cpp
2017-05-31 18:05:03 -07:00
Gabriel Ebner
baa4c48f1f
refactor(util/lean_path): explicitly pass around search path
2017-05-01 14:11:38 -07:00
Gabriel Ebner
595cbb8fe9
refactor(*): task<T>, log_tree, cancellation_token
2017-03-23 08:57:52 +01:00
Leonardo de Moura
3d603ec28e
feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs
2017-02-08 17:41:44 -08:00
Gabriel Ebner
cbc0bb1f7c
feat(library/module): store whether we used sorry in olean
2017-02-05 16:35:32 +01:00
Gabriel Ebner
f6b8eb6821
feat(util/task_queue): lazy tasks
2017-01-04 16:30:22 -08:00
Gabriel Ebner
15157bdf0b
feat(frontends/lean/parser): keep going after failed imports
2016-12-23 10:53:47 +01:00
Gabriel Ebner
0550d2a6ac
refactor(library/module): import all modules in a single call
2016-12-20 10:15:19 -08:00
Gabriel Ebner
370d69de3f
refactor(library/module): interface to get task dependencies for modifications
2016-12-20 10:15:19 -08:00
Gabriel Ebner
a2bc967fac
feat(library/module): reuse pre-imported init module
2016-12-20 10:15:19 -08:00
Gabriel Ebner
a26e2c9108
feat(library/module): intermediary data structure for environment modifications
2016-12-20 10:15:19 -08:00
Gabriel Ebner
a972c13ce9
refactor(library/task_queue): move task queue to util
2016-12-12 10:01:34 -05:00
Leonardo de Moura
d40e97b4bc
chore(*): compilation errors, fix style, fix warnings
2016-11-29 11:35:01 -08:00
Gabriel Ebner
3ecfddcbd5
fix(*): fix build
2016-11-29 11:12:43 -08:00
Gabriel Ebner
385ea13688
feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction
2016-11-29 11:12:43 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
d6000416f8
feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information
...
We will use this information in the debugger.
2016-11-09 16:51:48 -08:00
Leonardo de Moura
6173d95d18
feat(library/module,frontends/lean): store line/column number information
2016-11-02 16:55:21 -07:00
Leonardo de Moura
cea572a167
feat(library/module): store .olean file name for imported declarations
2016-11-02 15:37:33 -07:00
Leonardo de Moura
3958d8485a
chore(library/module): remove dead code
2016-11-02 15:02:49 -07:00
Gabriel Ebner
b14a0c43ff
feat(frontends/lean/parser,library/module): warn if imported modules are out-of-date
2016-10-13 18:49:10 -07:00
Leonardo de Moura
572751c56e
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
...
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
2016-09-29 17:56:35 -07:00
Leonardo de Moura
932d14241b
chore(kernel): remove support for mutually inductive datatypes from the kernel
2016-09-10 17:39:17 -07:00
Leonardo de Moura
6c934229f7
feat(kernel,library/module): only module reader can add declarations without type-checking them
2015-08-14 18:37:17 -07:00
Leonardo de Moura
f8e2f68ce0
feat(frontends/lean): add 'wait' command
...
This commit also fixes several problems with -j option (parallel
compilation). The .olean files were not missing data when -j was used
see issue #576
2015-05-08 20:05:21 -07:00
Leonardo de Moura
57ea660963
refactor(*): start process for eliminating of opaque definitions from the kernel
...
see issue #576
2015-05-08 16:06:04 -07:00
Leonardo de Moura
701b0ae66f
feat(library): export environment in textual format
...
closes #577
2015-05-04 18:05:00 -07:00
