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

105 commits

Author SHA1 Message Date
Sebastian Ullrich
7718795178 fix: mark Lean objects in C++ globals reachable from the new frontend as persistent 
sed -Ei 's/(g_\w+)\s*= new (name|expr|format|level|string_ref)\W.*;/\0\n    mark_persistent(\1->raw());/' src/kernel/**/*.cpp src/util/**/*.cpp src/library/**/*.cpp
 2020-10-11 17:43:28 +02:00
Leonardo de Moura
fb5440a074 fix: new frontend does not eagerly simplify universe level expressions 
Remark: even if we change the new frontend to simplify all universe
level expressions, we should not rely on this property in the kernel.
Reason: users may still create terms without this property.

Remark: this bug was preventing the kernel from accepting valid declarations.
 2020-07-24 15:45:01 -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
3980194fbf chore: more assertions and old code 2019-11-19 12:55:02 +01:00
Sebastian Ullrich
11809d23a9 chore: remove outdated assertion 
/cc @leodemoura
 2019-11-19 10:56:35 +01:00
Leonardo de Moura
b78ac59523 refactor: Level fully implemented in Lean 2019-11-17 08:24:09 -08:00
Leonardo de Moura
8c7f514a9d feat: expose instantiateLevelParams 2019-10-31 20:12:08 -07:00
Leonardo de Moura
14afe50384 chore: fix extern Level primitive names 2019-10-24 19:09:37 -07:00
Leonardo de Moura
025e9d32ef feat: update functions for universe levels, use C version of Level.hasParam and Level.hasMVar 2019-10-24 19:04:01 -07:00
Leonardo de Moura
9baf91e641 feat: add Level.isEquiv 2019-10-21 10:56:59 -07:00
Leonardo de Moura
a507145eb1 feat(library/init/lean/level): add instance : HasBeq Level 2019-10-01 09:47:44 -07:00
Leonardo de Moura
3afa4f7ab0 chore(util/safe_arith): remove dead code 2019-06-07 09:52:31 -07:00
Leonardo de Moura
818f2f2d4a chore(kernel): remove old #include 2019-03-06 06:56:16 -08:00
Leonardo de Moura
811a480d77 feat(kernel/expr): low level API for expr 2019-02-13 14:59:18 -08:00
Leonardo de Moura
71f5290567 feat(kernel): expose level primitives 2019-02-13 10:37:13 -08:00
Leonardo de Moura
4627929a83 refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI 2019-02-13 08:27:23 -08:00
Leonardo de Moura
bd38fc530f refactor(kernel/level): low level API for level 2019-02-07 15:04:12 -08:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Leonardo de Moura
4863ca071a chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
Leonardo de Moura
dd03747d22 chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
Leonardo de Moura
96ff6b1718 feat(util/object_ref): add helper functions 2018-08-27 16:28:37 -07:00
Leonardo de Moura
bc57c66ae3 refactor(kernel/level): naming consistency 2018-06-22 10:29:56 -07:00
Leonardo de Moura
14d62ab12d chore(runtime/serializer): compilation warning 2018-05-29 08:04:42 -07:00
Leonardo de Moura
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
4af1f31877 feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels 2018-05-23 14:48:22 -07:00
Leonardo de Moura
306c300226 refactor(kernel/level): implement level on top of object 2018-05-23 09:54:46 -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
Leonardo de Moura
efb9fb0802 chore(kernel): remove opportunistic hash consing support 
It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.
 2018-04-12 16:43:10 -07:00
Leonardo de Moura
ec1a490a15 chore(*): annotate candidates for thread local cache reset 2018-02-01 14:59:37 -08:00
Gabriel Ebner
42288198db fix(kernel/expr): disable caching by default 2017-03-23 08:57:56 +01:00
Leonardo de Moura
d37fd17725 fix(kernel/level): potential compiler specific behavior 2017-03-11 18:30:28 -08: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
Leonardo de Moura
5572d7f3ec perf(kernel,library/module): enable expr caching when deserializing .olean files 2016-12-16 18:33:46 -08:00
Leonardo de Moura
52ef17284a fix(kernel/expr, kernel/level): if caching is enabled during finalization, these modules would register a finalizer after finalization of the main thread 
The deleted lines were not really needed. They were added before we had
the thread finalization code.
 2016-12-01 10:16:05 -08:00
Leonardo de Moura
769da9c95a fix(library/unifier): missing occurs check 2015-12-04 09:14:55 -08:00
Leonardo de Moura
a446c54b87 fix(tests/kernel/max_sharing): max_sharing on OSX 2015-10-03 12:12:21 -07:00
Leonardo de Moura
cb2f93ee6a fix(kernel/expr,kernel/level): performance problem 
The method unordered_set::clear takes time O(n) where n is the number of
buckets in the hashtable used to implement the set.
Moreover, it does not reduce the number of buckets to 0.
That is, it keeps `n` empty buckets.

This creates performance problems if the number of buckets gets really
huge at one point.
The tst6 at tests/kernel/expr.cpp demonstrates the problem
 2015-09-30 17:25:13 -07:00
Leonardo de Moura
57035d3162 feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more 2015-09-30 13:31:42 -07:00
Leonardo de Moura
3626bd83bf refactor(util/sexpr/format): remove format constructors using std::initializer_list 
For some reason lean.js (Lean compiled using emscripten) crashes when
this kind of constructor is used.
 2015-06-20 14:02:18 -07:00
Leonardo de Moura
e81d9c9184 perf(kernel/level): apply two simple normalization rules at mk_max 
They are variations of:
max l1 (max l1 l2) == (max l1 l2)
 2014-11-16 18:16:57 -08:00
Leonardo de Moura
67de3b06f3 feat(kernel/level): improve universe level pretty printer 
Example: produce `l+2` instead of `succ (succ l)`.
 2014-11-14 14:51:03 -08:00
Leonardo de Moura
ffffabad95 feat(kernel/level): improve is_geq procedure for universe levels 
Now, it also returns true for

          (succ^k1 a)  =?=  k2

where k1 >= k2
 2014-11-14 14:20:35 -08:00
Leonardo de Moura
93e0599a0f feat(kernel/level): add missing normalization rule 2014-10-08 22:23:19 -07:00
Leonardo de Moura
98e66586e9 feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit 2014-10-02 14:29:51 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
fbf13994d8 refactor(*): use + for concatenating format objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 09:35:25 -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
1a6d0784f2 feat(kernel/level): improve universe level normalization procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:49:41 +01:00
Leonardo de Moura
12d89ea0b9 fix(kernel/level): is_geq predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:18:41 +01:00