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

159 commits

Author SHA1 Message Date
Sebastian Ullrich
fce8ca304b fix: reintroduce code that cancels all remaining tasks on task manager shutdown 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
63d60e6564 fix: more robust m_keep_alive implementation not reliant on RC 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
e8a1f36d0c fix: prevent storing ST closure in MT task 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
b214b27557 fix: prevent storing ST value in MT task object 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
a1c17ade3a fix: use-after-free in keep-alive tasks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
ac56a9e79f fix: run tasks to completion on task_manager shutdown to prevent leaks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
fc4428f621 fix: mark Task closures as MT 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
469a822cc6 chore: checkInterrupted ~> checkCanceled, requestInterrupt ~> cancel 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
77cbaa752c fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
1782352af1 feat: optionally run tasks even when already cancelled 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
00f176de8d fix: Windows debug build 2020-08-30 14:28:56 -07:00
Sebastian Ullrich
110ae4b571 feat: replace OS-specific stream redirection with pure-Lean Stream redirection 
This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
 2020-08-28 10:04:32 -07:00
Sebastian Ullrich
56fda835be feat: add ByteArray <-> String conversions 2020-08-28 10:04:32 -07:00
Sebastian Ullrich
dbebff3a2d feat: ByteArray.copySlice 2020-08-28 10:04:32 -07:00
Leonardo de Moura
2f1ec93289 chore: move runtime implementation to src/runtime 2020-05-22 14:35:16 -07:00
Leonardo de Moura
1a77ee4f89 chore: delete old runtime directory 2020-05-18 11:33:18 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Leonardo de Moura
e22af8d1ef feat: add FloatArray 
cc @dselsam
 2020-04-07 18:05:54 -07:00
Leonardo de Moura
8e84a8c9ec feat: Float from big numbers 2020-04-06 14:05:17 -07:00
Leonardo de Moura
8e952f3c36 chore: style 2020-04-03 17:48:06 -07:00
Leonardo de Moura
c236a179f2 feat: enable externs 2020-04-03 17:19:48 -07:00
Leonardo de Moura
71397aad36 feat: runtime primitives 2020-04-03 15:55:39 -07:00
Leonardo de Moura
3d0bfcd36a fix: assertion violation 2020-01-31 08:25:59 -08:00
Leonardo de Moura
67fb63c9fd feat: use mpz_pow_ui to implement Nat.pow 2020-01-21 09:16:38 -08:00
Sebastian Ullrich
f171404530 fix: "superficial" leaks to shut up lsan 2019-12-22 17:23:51 -08:00
Sebastian Ullrich
3b37737c8a fix: leaks 2019-12-22 15:09:19 -08:00
Leonardo de Moura
74f48414f1 feat: add option --exitOnPanic (short version -e) 
Lean does not exit on panic anymore.
The old behavior (`std::exit(1)`) produces a horrible debugging
experience for the elaborator since all trace messages are lost.
The new command line option restores the old behavior.

cc @Kha @dselsam
 2019-12-19 09:24:37 -08:00
Leonardo de Moura
54e5ca0c7b fix: lean_nat_abs 
It must not assume a nonnegative big integer is a big nat.
 2019-12-14 08:08:41 -08:00
Sebastian Ullrich
90b91760aa fix: SMALL_ALLOCATOR=OFF 2019-10-29 13:41:16 -07:00
Sebastian Ullrich
58dd7346e4 fix: build with SMALL_ALLOCATOR=OFF 2019-10-29 17:07:42 +01:00
Leonardo de Moura
411f397654 refactor(library/init/data/list): new name convention for List functions 
cc @dselsam @kha
 2019-10-01 15:15:02 -07:00
Leonardo de Moura
3d7a7c7e91 feat(library/init/util): add panic primitive 2019-09-30 16:23:18 -07:00
Leonardo de Moura
a4b860b92a fix(runtime): missing Array.data primitive 2019-09-19 10:27:10 -07:00
Leonardo de Moura
a7d616605a fix(runtime/lean): missing primitive 2019-09-19 09:54:03 -07:00
Leonardo de Moura
dc82c5cc70 chore(runtime/object): fix compilation error in debug mode on OSX 2019-08-28 15:43:21 -03:00
Leonardo de Moura
f40617d8dd feat(CMakeLists, runtime): add CHECK_RC_OVERFLOW cmake option 2019-08-28 15:35:46 -03:00
Leonardo de Moura
a944d158a3 feat(CMakeLists.txt): add SMALL_RC cmake option 
When used with `COMPRESSED_OBJECT_HEADER`, Lean uses a compressed
object header where only 32-bits are reserved for the RC.
The motivation is performance, in our experiments, it is faster to
access a 32-bit counter than a 45-bit one.
With a smaller RC, we can use 8-bits for the memory kind information,
and speedup its access.
 2019-08-28 14:54:08 -03:00
Leonardo de Moura
cb1680e096 chore(runtime/object): use same idiom we used at del_core 2019-08-24 12:02:09 -07:00
Leonardo de Moura
9d09325d1e fix(runtime): ensure we can disable LEAN_SMALL_ALLOCATOR 2019-08-24 11:18:07 -07:00
Leonardo de Moura
86c2c32810 fix(runtime/object): memory leak 2019-08-24 10:24:39 -07:00
Leonardo de Moura
fb4e2daf74 fix(runtime/object): debug build 2019-08-24 09:51:37 -07:00
Leonardo de Moura
720c3ca3e4 fix(runtime): size_t issue OSX vs Linux 2019-08-24 09:30:12 -07:00
Leonardo de Moura
140708fe8d chore(runtime): style 2019-08-24 07:40:56 -07:00
Leonardo de Moura
70f3537a29 feat(runtime): add lean_panic and variants 2019-08-24 07:40:39 -07:00
Leonardo de Moura
e7c8e66986 fix(runtime/object): remove incorrect assertions 
They are not true when LEAN_COMPRESSED_OBJECT_HEADER is defined.
 2019-08-24 07:40:38 -07:00
Leonardo de Moura
6553c5531c fix(runtime): bugs at compact.cpp and object size calculation 2019-08-24 07:40:38 -07:00
Leonardo de Moura
124c5da414 fix(runtime): disable compressed headers and fix bugs 2019-08-24 07:40:38 -07:00
Leonardo de Moura
3b762d4dc0 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Leonardo de Moura
dcd15f3424 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Sebastian Ullrich
2c12f9d0f6 chore(runtime/object): LEAN_FAKE_FREE: assert on double-free 2019-07-30 17:52:43 -07:00