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

603 commits

Author SHA1 Message Date
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
Sebastian Ullrich
1221bdd3c7 fix: use redirected stderr for timeit & allocprof 2021-12-16 06:38:35 -08:00
Sebastian Ullrich
87e860f871 perf: Array.push: move elements directly when source is unique 2021-12-16 06:37:37 -08:00
Sebastian Ullrich
3c9ea3b113 fix: wait on tasks before Lean program exit 2021-12-15 15:58:24 +01:00
tydeu
a3250dc44b feat: expose --load-dynlib functionality to Lean code 2021-12-15 08:26:48 +00:00
tydeu
d518ba7f08 feat: use BaseIO more in Init.System.IO 2021-12-14 09:33:52 +01:00
Sebastian Ullrich
0ade9ee39b fix: make IO.Process.Child.wait fallible 2021-12-13 15:12:48 +01:00
Gabriel Ebner
c7565c446a fix: casts on big-endian 2021-12-02 09:57:58 -08:00
Sebastian Ullrich
1ade96cfab fix: assertion with USE_GMP=OFF 2021-12-02 15:11:47 +01:00
Leonardo de Moura
5e9ebf044a fix: insert_mpz 2021-12-01 13:47:05 -08:00
Leonardo de Moura
92a5f8f18e fix: insert_mpz 2021-12-01 13:38:20 -08:00
Leonardo de Moura
988b316e3f feat: check "LEAN_ABORT_ON_PANIC" environment variable at lean_internal_panic 2021-12-01 13:38:20 -08:00
Leonardo de Moura
375de32bfb fix: fix_mpz 2021-12-01 13:38:19 -08:00
Leonardo de Moura
e9e40789c1 fix: mpz::power for USE_GMP=OFF 2021-11-30 17:57:33 -08:00
Leonardo de Moura
83d6eb1c72 fix: mpz::mul2k for USE_GMP=OFF 2021-11-30 17:19:16 -08:00