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

1017 commits

Author SHA1 Message Date
Sebastian Ullrich
7964b727e5 chore: improve error message 2020-10-22 21:40:58 +02:00
Sebastian Ullrich
ecece59cc3 fix: tracing the compiler from the new frontend 2020-10-22 14:50:26 +02:00
Sebastian Ullrich
4e74e36331 feat: run initializers on import 
Also, refuse to evaluate an `[init]` decl in the same module (since we don't know whether the initialization is
backtrackable) and always use native symbol of a `[builtinInit]` decl
 2020-10-22 11:59:55 +02:00
Sebastian Ullrich
86fe95898d fix: don't try to interpret [builtinInit] constants 2020-10-22 11:59:55 +02:00
Sebastian Ullrich
b06f8311e8 fix: avoid using native code during bootstrap 2020-10-21 11:21:56 +02:00
Sebastian Ullrich
438b3351dd feat: add interpreter.prefer_native option 2020-10-21 11:21:56 +02:00
Leonardo de Moura
e54a207986 refactor: provide Options to lean_eval_const 
add `ImportM` monad for `addImportedFn`

cc @Kha
 2020-10-19 10:21:38 -07:00
Leonardo de Moura
863cffde34 feat: elaborated borrowed annotations 2020-10-16 15:17:58 -07:00
Leonardo de Moura
827625a377 perf: add temporary hack for performance issue 
The compiler frontend implemented in C++ is eagerly inlining local
functions. The new test would take an absurd amount of time without
the new hack.
We remove this hack when we re-implement the compiler frontend in Lean.
 2020-10-15 13:37:29 -07:00
Sebastian Ullrich
c3c037b4de fix: fixup a few automatic fixes 2020-10-11 17:43:28 +02:00
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
8383177c96 fix: nonoptimal specialization 
@Kha Here is the fix for the problem I told you this morning.
Please, take a look at `specialize.cpp` and see whether it makes sense.
 2020-09-24 12:40:28 -07:00
Sebastian Ullrich
e946aa9135 fix: interpreter thread-unsafety 2020-09-14 17:57:33 +02:00
Leonardo de Moura
217b7fc2b8 feat: improve extern arity calculation 2020-08-31 16:29:27 -07:00
Leonardo de Moura
ca1982441f feat: add support for to be added ST 
`ST` will be `EIO Empty`
 2020-08-20 13:45:58 -07:00
Leonardo de Moura
8349c72686 feat: add support for EIO 2020-08-20 12:48:39 -07:00
Leonardo de Moura
e301d57b36 chore: fix comment 2020-08-10 08:39:22 -07:00
Leonardo de Moura
9ddac04b40 fix: support for literals when compiling noConfusion 2020-08-05 10:17:51 -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
ec9f4b579d chore: improve precision of compilation time profiling 2020-04-24 15:11:36 +02:00
Leonardo de Moura
bc57faff08 fix: ensure compiler representation invariants are preserved 2020-04-23 13:54:14 -07:00
Leonardo de Moura
e22af8d1ef feat: add FloatArray 
cc @dselsam
 2020-04-07 18:05:54 -07:00
Sebastian Ullrich
e971c8dd7a feat: support Float in the interpreter 
/cc @leodemoura @dselsam
 2020-04-05 10:50:30 +02:00
Leonardo de Moura
485034bbba fix: bug at ir.cpp 2020-04-03 17:39:28 -07:00
Leonardo de Moura
0e2ebd36ff feat: make sure Float is in WHNF 2020-04-03 17:07:29 -07:00
Leonardo de Moura
60d84660e6 feat: add support for Float in the compiler 2020-04-03 16:39:29 -07:00
Sebastian Ullrich
d7170df527 feat: interpreter: print stacktrace on stack overflow 2020-03-14 15:08:03 -07:00
Sebastian Ullrich
e30717a85a fix: interpreter::call_boxed on unboxed constants 2020-03-14 15:04:38 -07:00
Leonardo de Moura
271b753f30 feat: optimization for Bool+Decidable code 2020-02-27 16:59:18 -08:00
Leonardo de Moura
021d906542 fix: remove filler fields (part 2) 2020-02-27 10:02:26 -08:00
Leonardo de Moura
966e5bc60d perf: remove "filler" fields 
See previous commit.
 2020-02-27 10:02:26 -08:00
Leonardo de Moura
1fb7a3a208 fix: position of first Bool field 2020-02-25 14:05:53 -08:00
Leonardo de Moura
9095f3caa0 chore: update stage0 2020-02-25 13:53:08 -08:00
Leonardo de Moura
7496296c1e fix: "filler" fields 2020-02-25 13:49:18 -08:00
Leonardo de Moura
6a19069021 feat: add "filler" fields 2020-02-25 13:49:11 -08:00
Leonardo de Moura
1305824b03 chore: add get_bool_field helper function 
Motivation: help us to adjust the code when we modify the position of
scalar fields.
 2020-02-25 13:43:06 -08:00
Leonardo de Moura
148c0324c4 fix: do not extract closed terms from join point applications 2020-02-15 15:43:24 -08:00
Leonardo de Moura
0cf226220c fix: remove incorrect assertion 
Note that `get_cases_on_minors_range` is now parametric on `m_before_erasure`:
`get_cases_on_minors_range(env(), const_name(fn), m_before_erasure)`
 2020-02-13 18:26:12 -08:00
Sebastian Ullrich
47f3d54acb fix: interpreter: do not consume values in explicit unbox instructions 2020-02-06 09:36:19 -08:00
Leonardo de Moura
38e6961003 feat: MutQuot by implementedBy 2020-02-04 16:51:08 -08:00
Leonardo de Moura
850b1c90a0 feat: mark as irrelevant functions that return types 2020-02-04 15:55:21 -08:00
Leonardo de Moura
8628b52b21 feat: missing support for Empty.rec 2020-01-03 18:23:52 -08:00
Sebastian Ullrich
2791cdf326 fix: interpreter::call_boxed: support under-application 
/cc @leodemoura
 2020-01-01 21:15:05 +01:00
Leonardo de Moura
73e114c6a2 chore: remove unnecessary argument 2020-01-01 09:19:00 -08:00
Sebastian Ullrich
b439de68a5 feat: support nested interpreter executions and make sure closures are run in compatible environments 
/cc @leodemoura
 2019-12-31 00:07:45 +01:00
Leonardo de Moura
28a4859832 feat: expose evalConst 
@Kha Could you please check `lean_eval_const`?
 2019-12-30 11:41:36 -08:00
Sebastian Ullrich
a2d668ec99 fix: leaks 2019-12-22 17:24:57 -08:00
Sebastian Ullrich
3b37737c8a fix: leaks 2019-12-22 15:09:19 -08:00
Sebastian Ullrich
948b0bf1f1 fix: interpreter::call_boxed: support over-application 
MetaHasEval instances were not fully eta-expanded
 2019-12-05 13:21:08 +01:00