tydeu
c79c7c89b3
feat: IO.Process.getPID & IO.FS.Mode.writeNew
2023-08-08 16:23:43 -04:00
Mario Carneiro
dd313c6894
feat: add IO.FS.rename
2023-07-22 23:21:32 +02:00
Scott Morrison
60b8fdd8d6
feat: use nat_pow in the kernel
2023-07-10 09:01:14 -07:00
Sebastian Ullrich
9901804a49
feat: SpawnArgs.setsid, Child.kill
2023-07-05 23:42:53 +02:00
Mario Carneiro
bb8cc08de8
chore: compact objects in post-order
2023-06-26 08:35:19 -07:00
Olivier Taïbi
9aeae67708
fix: advance pointer into array when generating random bytes
...
otherwise if we have more than one chunk then the first one is overwritten
over and over, and the end of the array is not really random
2023-04-06 11:32:12 +02:00
Sebastian Ullrich
15c146b382
feat: proper I/O errors from getLine
2023-03-10 16:27:56 +01:00
Sebastian Ullrich
51e77d152c
fix: do not inherit file handles across process creation
2023-03-10 16:27:56 +01:00
Sebastian Ullrich
113de7cca1
refactor: move from fopen to open
2023-03-10 16:27:56 +01:00
Gabriel Ebner
f4d005e86d
chore: only build small allocator if enabled
...
This prevents us from calling alloc/dealloc if LEAN_SMALL_ALLOCATOR is
disabled.
2023-01-24 11:37:43 -08:00
Gabriel Ebner
3deef5d32a
fix: mpz: honor LEAN_SMALL_ALLOCATOR
2023-01-24 11:37:43 -08:00
Gabriel Ebner
345aa6f835
chore: put throws in separate function for debugger
2023-01-23 09:27:09 -08:00
Tobias Grosser
d74d4230b7
fix: avoid warning by dropping '#pragma once'
...
Before this change, we would see the warning:
"#pragma once in main file"
2023-01-04 09:42:40 +01: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
Leonardo de Moura
e5681ac141
feat: replace mixHash implementation
...
We are now using part of the murmur hash like Scala.
For additional information and context, see
https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313114719
2022-11-30 17:03:58 -08:00
Siddharth Bhat
dfb5548cab
fix: update libleanrt.bc, rename to lean.h.bc
...
This adds `lean.h.bc`, a LLVM bitcode file of the Lean
runtime that is to be inlined. This is programatically generated.
1. This differs from the previous `libleanrt.ll`, since it produces an
LLVM bitcode file, versus a textual IR file. The bitcode file
is faster to parse and build an in-memory LLVM module from.
2. We build `lean.h.bc` by adding it as a target to `shell`,
which ensures that it is always built.
3. We eschew the need for:
```cpp
```
which causes breakage in the build, since changing the meaning of
`static` messes with definitions in the C++ headers.
Instead, we build `lean.h.bc` by copying everything in
`src/include/lean/lean.h`, renaming `inline` to
`__attribute__(alwaysinline)` [which forces LLVM to generate
`alwaysinline` annotations], then running the `-O3` pass pipeline
to get reasonably optimised IR, and will be perfectly inlined
when linked into the generated LLVM code by
`src/Lean/Compiler/IR/EmitLLVM.lean`.
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-11-28 16:20:12 +01:00
Sebastian Ullrich
3f9ba30424
fix: integer overflows
2022-11-15 07:37:54 -08:00
Leonardo de Moura
5eaa0fa2df
chore: leftovers
2022-11-09 17:03:08 -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
Sebastian Ullrich
9f2182fdd9
chore: update script/apply.lean semantics
2022-11-07 19:47:04 -08:00
Leonardo de Moura
dc750d143e
chore: remove test/optimization that is essentially dead code
2022-10-27 16:45:50 -07:00
awson
d5063c8fa7
fix: environment leak on Windows
2022-10-19 19:34:43 -07:00
Gabriel Ebner
7c552380da
feat: Mutex, Condvar
2022-09-05 08:52:46 -07:00
Gabriel Ebner
c2f1e01b3b
feat: Promise
2022-09-05 08:52:46 -07:00
Mario Carneiro
6a7ccb5797
refactor: generalize ShareCommon to a typeclass ( #1537 )
2022-08-29 09:34:38 -07:00
Sebastian Ullrich
b010805000
fix: Handle.read at EOF
2022-08-26 20:55:09 -07:00
Sebastian Ullrich
af7f5aa2a0
feat: dbgStackTrace
2022-08-26 20:52:51 -07:00
Andrés Goens
fa22507e8e
feat: blocking behavior on EOF for getLine ( #1479 )
2022-08-21 16:27:48 +02:00
Mario Carneiro
9de477ecf9
feat: add more float functions
2022-08-12 13:12:59 -07:00
Mario Carneiro
94f85ae649
fix: don't show NaN sign info in Float.toString
2022-08-12 08:21:47 -07:00
Leonardo de Moura
f9f074dbf5
chore: remove dead code
2022-08-06 20:20:50 -07:00
Leonardo de Moura
386b0a75bc
fix: bug at lean_nat_mod
...
fixes at #1433
2022-08-06 08:07:25 -07:00
Leonardo de Moura
949dddbf63
fix: lean_float_array_data
2022-07-24 17:05:28 -07:00
Leonardo de Moura
757171db1f
feat: add String.get! and s[i]! notation for String
2022-07-03 14:59:44 -07:00
Leonardo de Moura
e8935d996b
chore: String.get?, String.getOp?, and remove String.getOp
2022-07-02 09:59:04 -07:00
Sebastian Ullrich
c8fb72195b
feat: print panic backtraces on Linux
2022-06-29 16:29:35 +02:00
Leonardo de Moura
8d9428261e
chore: remove Fix.lean
...
see #1208
2022-06-16 15:30:47 -07:00
Sebastian Ullrich
eb170d1f43
fix: compiled string literals containing null bytes
2022-05-17 09:24:34 -07:00
Gabriel Ebner
88e26b75b0
fix: actually abort with LEAN_ABORT_ON_PANIC
...
The previous null-pointer dereference was UB and therefore optimized
away.
2022-05-03 09:42:45 -07:00
Sebastian Ullrich
78bf398830
fix: avoid signal-unsafe fprintf in stack overflow handler
2022-04-29 15:55:11 +02:00
Jannis Limperg
5ff8f64255
feat: add IO.monoNanosNow
2022-04-11 12:16:20 +02:00
Jannis Limperg
6459ccc43c
fix: prevent overflow in lean_io_mono_ms_now
2022-04-11 12:16:20 +02:00
Sebastian Ullrich
7460878e05
chore: define WIN32_LEAN_AND_MEAN
2022-04-06 09:38:19 +02:00
Leonardo de Moura
2bd04285f8
fix : #1087
...
This commit is using the easy fix described at issue #1087 .
Hopefully the performance overhead is small.
closes #1087
2022-03-30 18:48:02 -07:00
Sebastian Ullrich
0d03c6e319
chore: revise non-GMP interface
2022-03-16 17:32:51 -07:00
Gabriel Ebner
412691c958
feat: support LEAN_NUM_THREADS environment variable
2021-12-21 17:01:08 +01:00
Sebastian Ullrich
b732484663
fix: do not consider worker threads as idle during startup
...
Without this change, enqueuing multiple tasks before the first worker
was started led to only a single worker being created. Now the first
increment and decrement happen under the task manager mutex, so
effectively the worker is never idle until it is out of tasks.
2021-12-21 12:01:23 +01:00
