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

196 commits

Author SHA1 Message Date
Leonardo de Moura
d0358810a7 feat: add lean_set_panic_messages 2021-06-29 14:30:56 -07:00
Leonardo de Moura
5ac2e14173 chore: add Hashable that uses UInt64 2021-06-02 07:47:41 -07:00
Leonardo de Moura
c566ad97a4 chore: prepare to use UInt64 hash codes 2021-06-02 06:51:18 -07:00
Sebastian Ullrich
7b128b308b fix: leak in lean_mk_array 2021-05-07 18:20:32 +02:00
Leonardo de Moura
104b51471c chore: fix warning 2021-04-22 20:38:57 -07:00
Leonardo de Moura
df665bc219 chore: remove leftover 2021-04-22 20:34:52 -07:00
Sebastian Ullrich
8895ed47e5 refactor: clean up Thunk 
Fixes a bug in the native implementation of `Thunk.bind` by deleting it
 2021-04-22 20:29:08 -07:00
Leonardo de Moura
393adadf9a chore: leftovers 2021-04-07 10:26:05 -07:00
Leonardo de Moura
9901898258 feat: add Nat.gcd 
This commit also fix some theorem names to new naming convention.
 2021-03-07 18:47:02 -08:00
Leonardo de Moura
709eaf6873 chore: use lean_internal_panic 2021-03-04 15:46:33 -08:00
Joe Hendrix
9bd60c7519 feat: Nat/Fin/UInt instances of bitwise classes 2021-03-04 15:42:43 -08:00
Leonardo de Moura
130a087ecf feat: Lean 3 french single quote notation 2021-03-04 09:43:59 -08:00
Leonardo de Moura
bbed4aed50 chore: remove old code 2021-03-04 07:54:21 -08:00
Leonardo de Moura
51200c916e chore: make explicit user and internal panics 2021-03-04 07:37:33 -08:00
Leonardo de Moura
09ad6cc50a fix: fixes #306 fixes #307 2021-02-06 12:31:51 -08:00
Leonardo de Moura
10a10b38d8 fix: fixes #303 2021-02-05 07:53:18 -08:00
Leonardo de Moura
22a7a9e313 fix: missing lean_inc 2021-01-31 12:07:24 -08:00
Leonardo de Moura
f9ebfb466f fix: missing lean_inc 2021-01-31 11:18:57 -08:00
Leonardo de Moura
36e70e9a08 fix: Int.mod implementation in the runtime 2021-01-31 08:50:06 -08:00
Leonardo de Moura
3fa1f355eb fix: mod implementation 2021-01-31 08:19:32 -08:00
Leonardo de Moura
b3703739af chore: internal panic meesage 2021-01-13 10:26:25 -08:00
Leonardo de Moura
f6e5b13591 feat: "implement" sorry using panic 2021-01-13 09:43:25 -08:00
Sebastian Ullrich
5aab1cadc0 chore: remove debug print 2021-01-02 22:00:30 +01:00
Sebastian Ullrich
4a262fbc5b fix: remove auto-cancellation of IO tasks 
Chained tasks were never auto-canceled, so let's be explicit everywhere
 2020-12-30 17:03:09 +01:00
Sebastian Ullrich
91dac6ccff fix: race condition in Task.bind 2020-12-30 17:01:05 +01:00
Leonardo de Moura
c71eebde8c chore: remove util/buffer.h dependency from runtime 2020-12-14 18:07:28 -08:00
Leonardo de Moura
bbafaf8805 fix: Array.mk and Array.data externs 2020-12-13 11:10:01 -08:00
Leonardo de Moura
6a41d04827 fix: missing panics 2020-12-08 10:36:53 -08:00
Leonardo de Moura
b95c4788c1 refactor: OfDecimal ==> OfScientific 
`decimalLit` ==> `scientificLit`
 2020-12-03 08:08:19 -08:00
Leonardo de Moura
d1f4d4f57e feat: scientific notation 2020-12-03 07:49:20 -08:00
Leonardo de Moura
962cffbaaa feat: add lean_float_of_decimal using GMP 2020-12-03 06:15:18 -08:00
Sebastian Ullrich
a22d234e93 fix: Thunk.get: mark result as MT before storing it in the task object 2020-11-29 18:59:39 +01:00
Sebastian Ullrich
3e09184a39 fix: String.mk, String.toList 2020-10-16 09:42:59 +02:00
Sebastian Ullrich
8b62665788 chore: print dbg* output to stderr 2020-10-12 10:01:29 +02:00
Sebastian Ullrich
c83529810d fix: avoid deadlock on freeing task-carrying task 2020-10-11 17:43:28 +02:00
Sebastian Ullrich
ab6b6ac3ba feat: add dedicated task priority 2020-09-29 08:01:10 -07:00
Sebastian Ullrich
562c7ed5ce feat: expose task priorities 2020-09-29 08:01:10 -07:00
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