Sebastian Ullrich
6b0e7e1f46
feat: synchronous execution of task continuations ( #3013 )
...
In the new snapshot design, we have a tree of `Task`s that represents
the asynchronously processed document structure. When transforming this
tree in response to a user edit, we want to quickly run through
reusable, already computed nodes of the tree synchronously and then
spawn new tasks for the new parts. The new flag allows us to do such
mixed sync/async tree transformations uniformly. This flag exists as
e.g.
[`ExecuteSynchronously`](https://learn.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskcontinuationoptions?view=net-8.0 )
in other runtimes.
2024-01-25 13:54:20 +00:00
Sebastian Ullrich
2beb948a3b
feat: System.Platform.target ( #3207 )
...
Makes the LLVM triple of the current platform available to Lean code
towards a solution for #2754 .
Defaults to the empty string if the compiler is not clang, which can
introduce some divergence between CI and local builds but should not be
noticeable in most cases and is not really possible to avoid.
2024-01-24 12:11:00 +00:00
Sebastian Ullrich
62dc8d7308
feat: Runtime.markMultiThreaded/Persistent
2023-11-14 17:33:04 +01:00
int-y1
ce4ae37c19
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
Alexander Bentkamp
7dc1618ca5
feat: Web Assembly Build ( #2599 )
...
Co-authored-by: Rujia Liu <rujialiu@user.noreply.github.com>
2023-10-04 09:04:20 +02:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie ( #2529 )
2023-09-20 13:22:37 +02:00
Mario Carneiro
fec3575aaf
fix: 0-arg functions in C need f(void)
2023-08-31 15:39:47 -04:00
Sebastian Ullrich
17602d9f28
chore: avoid "unused parameter" warnings in lean.h
2023-08-02 10:20:57 +02:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM ( #2363 )
2023-07-30 10:39:40 +02:00
Siddharth
b6eb780144
feat: LLVM backend ( #1837 )
2022-12-30 12:45:30 +01:00
Gabriel Ebner
681bbe5cf4
feat: ByteArray.hash
2022-12-01 20:18:14 -08:00
Gabriel Ebner
9b416667e7
chore: replace all hashes by murmurhash
2022-12-01 20:18:14 -08:00
Henrik Böving
24cc6eae6d
feat: log2 for Fin and UInts
2022-11-29 01:05:06 +01:00
Leonardo de Moura
4f07c46956
fix: bug at lean_string_utf8_get_fast
2022-11-09 16:58:20 -08:00
Leonardo de Moura
92c03c0050
perf: prepare do add String.next'
2022-11-09 12:00:31 -08:00
Leonardo de Moura
20eeb4202f
perf: fast String.get' without runtime bounds check
...
TODO: naming convention `String.get'` should be called `String.get`,
and we should rename the old `String.get`
2022-11-09 12:00:30 -08:00
Gabriel Ebner
c2f1e01b3b
feat: Promise
2022-09-05 08:52:46 -07:00
Mario Carneiro
9de477ecf9
feat: add more float functions
2022-08-12 13:12:59 -07:00
Mario Carneiro
d8c6c827fe
fix: use saturating casts in lean_float_to_uint8 to avoid UB
2022-08-11 13:30:22 -07:00
Leonardo de Moura
f9f074dbf5
chore: remove dead code
2022-08-06 20:20:50 -07:00
Sebastian Ullrich
eb170d1f43
fix: compiled string literals containing null bytes
2022-05-17 09:24:34 -07:00
Sebastian Ullrich
3c9ea3b113
fix: wait on tasks before Lean program exit
2021-12-15 15:58:24 +01:00
Sebastian Ullrich
d4683e0169
chore: clean up LEAN_EXTRA_FLAGS
2021-11-20 11:04:39 +01:00
Sebastian Ullrich
6ca944f453
chore: avoid C++ warning
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
75a0b43aed
feat: reimplement assert without system headers
2021-11-18 09:42:35 +01:00
Sebastian Ullrich
3a7fa704c3
refactor: avoid non-compiler headers in lean.h
2021-11-18 09:42:35 +01:00
Chris Lovett
d3da41bac6
chore: remove unused header from lean.h
2021-10-29 09:43:19 +02:00
Leonardo de Moura
352391bfcb
chore: remove mpz_get_d dependency
2021-10-26 12:40:20 -07:00
Gabriel Ebner
61e0eab23f
refactor: reimplement ofScientific for floats
2021-10-26 11:51:30 -07:00
Leonardo de Moura
998bec0dd3
feat: new byte/float array primitives
2021-10-18 16:54:56 -07:00
Siddharth
da4ad465d0
feat: un-inline float intrinsics into runtime. ( #694 )
...
* outline all intrinsics into the runtime.
This is necessary to support backends such as LLVM which do not emit C.
* fix style
2021-10-18 07:20:04 -07:00
Sebastian Ullrich
d506b8a5ed
feat: hide non-exported symbols on Unix
2021-09-22 23:02:39 +02:00
Sebastian Ullrich
60ffdd094c
fix: annotate lean.h functions with LEAN_SHARED
2021-09-20 18:41:46 +02:00
Sebastian Ullrich
35ffae6f54
feat: Windows: explicitly export Lean functions only
2021-09-20 18:41:46 +02:00
Leonardo de Moura
218b9c87b0
feat: expose APIs for creating IO.Error objects
2021-09-11 17:14:43 -07:00
Leonardo de Moura
f9bc4b9b3a
feat: add missing APIs
2021-09-11 15:39:11 -07:00
Leonardo de Moura
6ced2cdece
refactor: move lean_name_eq to runtime, add lean_name_hash in C
2021-08-16 16:13:55 -07:00
Leonardo de Moura
a019d8071f
chore: document simplified object header and remove obsolete cmake options
2021-07-20 10:42:28 -07:00
Leonardo de Moura
c59e72a77b
chore: cleaner lean_dec_ref, inline persistent object case
2021-07-20 10:42:28 -07:00
Leonardo de Moura
da66610fda
chore: cleanup
2021-07-20 10:42:28 -07:00
Leonardo de Moura
974caa97e6
chore: typo
2021-07-20 10:42:28 -07:00
Leonardo de Moura
489b28085f
feat: simpler and faster RC
2021-07-20 10:42:28 -07:00
Sebastian Ullrich
904cfd6fcb
perf: extract cold path in lean_alloc_small
2021-07-19 13:20:28 -07:00
Sebastian Ullrich
16fbbf98e9
perf: extract cold paths in lean_free_small and mark noinline
2021-07-19 13:20:28 -07:00
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
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
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
8afa96d6c8
fix: incorrect lean_dec, lean_nat_to_int consumes the argument
2021-03-07 12:57:58 -08:00
