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

89 commits

Author SHA1 Message Date
Sebastian Ullrich
f2d5470f19 feat: allow interpretation of constants initialized by native code 2022-03-07 10:59:49 +01:00
Sebastian Ullrich
c59f7a55cf fix: initialize precompiled modules 2022-01-20 18:55:57 +01:00
Gabriel Ebner
ab276a5ae3 chore: show declaration with sorry in #eval 2022-01-17 13:18:22 -08:00
Sebastian Ullrich
fdd939fc40 fix: accidental memory leak in last commit 2021-12-21 19:43:02 +01:00
Sebastian Ullrich
3318f1fb05 feat: record declaration name in interpretation profile 2021-12-21 19:04:58 +01:00
Gabriel Ebner
e65f3fe810 fix: use redirected stderr for tout() 2021-12-16 10:23:05 -08:00
Joshua Seaton
a9317760e7
chore: update IR interpreter enum hygiene 
This change addresses -Wreturn type and -Wimplicit-fallthrough
infractions in the IR interpreter. Moreover, default switch cases on
enum classes are removed to leverage compiler complaints of missing
cases, which ensures that all related switch logic gets thoughtfully
extended when the enums are extended themselves.
 2021-11-28 10:29:08 +01:00
Leonardo de Moura
352391bfcb chore: remove mpz_get_d dependency 2021-10-26 12:40:20 -07:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Sebastian Ullrich
5f4b1b1d44 Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it"" 
This reverts commit ccbc9d00db.
 2021-08-20 09:42:05 -07:00
Sebastian Ullrich
ccbc9d00db Revert "feat: reintroduce libleanshared, link lean & leanpkg against it" 2021-08-20 15:39:00 +02:00
Sebastian Ullrich
58d6f3b817 fix: search all loaded modules for symbols on Windows 2021-08-18 13:54:52 +02:00
Leonardo de Moura
14b611af96 refactor: move buffer.h and *_ref.h files to runtime 2021-08-16 15:39:38 -07:00
Sebastian Ullrich
917eb4d081 chore: collect stdlib compilation flags in new header 2021-08-12 07:51:50 -07:00
Sebastian Ullrich
e1703bf1ae fix: main return value on 32-bit 
Resolves #594
 2021-08-03 11:00:10 -07:00
Wojciech Nawrocki
b7cd68a91e feat: complain more verbosely 2021-06-06 15:34:44 +02:00
Leonardo de Moura
cf5adbd4fe chore: increase LEAN_MAX_SMALL_OBJECT_SIZE and simplify code 2021-01-30 10:58:34 -08:00
Leonardo de Moura
d71aab5dc4 fix: allow bigger ctor objects 
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
 2021-01-29 18:23:38 -08:00
Leonardo de Moura
31680c1255 fix: do not evaluate code containing sorry 
closes #277
 2021-01-26 15:01:53 -08:00
Sebastian Ullrich
79abd5fec6 chore: remove C++ messages 2021-01-12 09:51:14 -08:00
Sebastian Ullrich
a6c319a25c chore: remove message_builder from time_task 2021-01-12 09:51:14 -08:00
Sebastian Ullrich
0ddc932052 fix: interpreter cache leak by simplifying it after all 2020-12-18 17:06:35 +01:00
Sebastian Ullrich
dcfef05c8e perf: reuse interpreter caches a bit more 2020-12-17 23:18:43 +01:00
Sebastian Ullrich
22bb2fbd06 perf: reuse thread-local interpreter 2020-12-17 23:18:43 +01:00
Sebastian Ullrich
af7e44f017 fix: interpreter: make sure to retain options after switching threads 2020-12-17 23:18:43 +01:00
Sebastian Ullrich
f649f24014 fix: compilation on Windows 2020-11-29 14:08:53 +01:00
Sebastian Ullrich
c0f94c902e fix: memory leak in interpreter 2020-11-29 14:08:53 +01:00
Sebastian Ullrich
99383d97e1 feat: measure interpreter time & fix enabling interpreter traces 2020-11-28 17:36:20 +01:00
Sebastian Ullrich
7964b727e5 chore: improve error message 2020-10-22 21:40:58 +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
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
Sebastian Ullrich
e946aa9135 fix: interpreter thread-unsafety 2020-09-14 17:57:33 +02: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
e971c8dd7a feat: support Float in the interpreter 
/cc @leodemoura @dselsam
 2020-04-05 10:50:30 +02: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
021d906542 fix: remove filler fields (part 2) 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
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
Sebastian Ullrich
47f3d54acb fix: interpreter: do not consume values in explicit unbox instructions 2020-02-06 09:36:19 -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