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

80 commits

Author SHA1 Message Date
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
Leonardo de Moura
5572d7f3ec perf(kernel,library/module): enable expr caching when deserializing .olean files 2016-12-16 18:33:46 -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
381b2edaf7 feat(library/vm/vm): store .olean file name at vm_decl's 2016-11-11 16:19:19 -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
3212d9c83a fix(library/module): store .olean file where inductive datatype was defined 2016-11-02 16:07:36 -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
e18370585d fix(frontends/lean/server): fix relative dependency lookups 2016-10-30 08:42:05 +08:00
Gabriel Ebner
ec0aa6d248 refactor(*): integrate emscripten build 2016-10-16 14:41:35 -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
9ef3ebbd5b refactor(*): delete HoTT support 2016-09-27 16:33:39 -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
155df48665 feat(library): remove decl_stats 
We are not using (and will not use) this module in the blast proof procedures
 2016-01-02 13:00:43 -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
5a48a2cebe feat(library/app_builder): add mk_sorry method 2015-11-08 14:05:02 -08:00
Leonardo de Moura
d64b410bbd feat(library): add declaration statistics 2015-11-08 14:04:56 -08:00
Leonardo de Moura
7bc8673786 feat(library/module): efficient inductive_reader 
Do not check imported inductive declarations when trust level is greater than 0.
 2015-08-15 14:48:49 -07:00
Leonardo de Moura
e80d9685e5 refactor(kernel/inductive): add certified_inductive_decl object 
We will use this object to implement a more efficient import procedure
 2015-08-15 13:26:38 -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
d1f13d2871 perf(library/module): skip checksum if trust level is very high 2015-08-14 18:23:12 -07:00
Leonardo de Moura
849b99d244 perf(library/module): use block read 2015-08-14 17:56:21 -07:00
Leonardo de Moura
308af87b69 feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -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
cf7e60e5a6 refactor(kernel): remove "opaque" field from kernel declarations 
see issue #576
 2015-05-08 16:06:16 -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
Leonardo de Moura
8241863abe feat(kernel/hits): add two builtin HITs: type_quotient and trunc 2015-04-23 15:32:31 -07:00
Leonardo de Moura
b960e123b1 feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
Leonardo de Moura
7d827a14c9 feat(library/module): expand 'failed to import' error message 
see issue #448
 2015-02-27 08:00:30 -08:00
Leonardo de Moura
752b54085b refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used 
Now, we unfold untrusted macros outside of the Lean kernel.
 2015-01-20 12:36:56 -08:00
Leonardo de Moura
8ab775bd6f feat(*): distinguish between logical and runtime exceptions. 
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
 2015-01-15 16:54:55 -08:00
Leonardo de Moura
8cfb3ae687 fix(library/module): bug in import_module 2014-10-18 21:03:22 -07:00
Leonardo de Moura
a30232b99a fix(library/module): race condition on m_imported 2014-10-14 15:19:50 -07:00
Leonardo de Moura
7231aa0d73 fix(library/module): allow multiple calls to import_modules with the same modules 
The idea is to store a set of already imported files.
This feature is useful when using the import_modules API directly (e.g.,
from javascript).
 2014-10-14 08:13:41 -07:00
Soonho Kong
2cf6cf19c0 feat(src): add LEAN_VERSION_PATCH 2014-10-07 12:30:38 -07:00
Leonardo de Moura
0d6d746d98 feat(frontends/lean): check modification time of imported files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-29 15:17:27 -07:00
Leonardo de Moura
531046626a refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
Leonardo de Moura
1fbb554a16 feat(library/module): provide predicate module::is_definition 2014-09-17 16:32:00 -07:00
Leonardo de Moura
4cf3d32e0c chore(*): create alias for std::pair 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
3d8477f7de fix(library/module): ignore multiple declarations of 'sorry', fixes #59 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-17 15:55:58 -07:00
Leonardo de Moura
0d97fff280 feat(library/module): include name of corrupted .olean file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 11:28:44 -07:00
Leonardo de Moura
2dca68e645 chore(util/list): add inline functions for commonly used patterns in list processing code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 13:51:38 -07:00
Leonardo de Moura
4b030c5d5f feat(library/module): relative module path 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 19:47:55 -07:00
Leonardo de Moura
de657e8df0 fix(util/rc): reference counter memory_order flags 
See discussion at
http://www.chaoticmind.net/~hcb/projects/boost.atomic/doc/atomic/usage_examples.html#boost_atomic.usage_examples.example_reference_counters
http://stackoverflow.com/questions/10268737/c11-atomics-and-intrusive-shared-pointer-reference-count

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-21 08:23:01 -07:00