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

546 commits

Author SHA1 Message Date
Leonardo de Moura
0002d8bd04 chore: missing #ifdef LEAN_USE_GMP 2021-11-29 11:35:13 -08:00
Leonardo de Moura
6396f3b2c1 chore: simplify mpz.h 
Add basic support for `LEAN_USE_GMP=OFF`.
 2021-11-29 11:11:49 -08:00
Sebastian Ullrich
d4683e0169 chore: clean up LEAN_EXTRA_FLAGS 2021-11-20 11:04:39 +01:00
Gabriel Ebner
6475e3d5cc fix: add missing LEAN_EXPORT 2021-11-18 11:14:26 +01:00
Sebastian Ullrich
0a40269fcb fix: build with mingw-clang64 clang 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
Mac
eb5852448e
feat: generalize IO task functions to BaseIO := EIO Empty (#744) 
* feat: generalize `asTask`/`bindTask`/`mapTask` to `EIO`

* feat: generalize task functions to the `EIO Empty` monad

* chore: fix test + correct doc

* feat: further generalize task functions to `RealM := EIO Empty`

* chore: `RealM`/Task API touch-ups

* refactor: `abbrev RealM` -> `def BaseIO`

* chore: remame args / remove `EIO.toBaseIO_` as per code review

* refactor: use `BaseIO` at `checkCanceled`/`getNumHeartbeats`

* chore: fix `lean_io_bind_task_fn` signature error
 2021-11-04 15:37:55 -07:00
Sebastian Ullrich
b5e7b2ab6e feat: Lean.githash 2021-11-04 15:29:48 -07:00
Leonardo de Moura
352391bfcb chore: remove mpz_get_d dependency 2021-10-26 12:40:20 -07:00
Leonardo de Moura
c25758e314 chore: remove mpz dead code 2021-10-26 12:28:33 -07:00
Leonardo de Moura
6d0fa6da7c chore: remove mpz dead code 2021-10-26 12:05:19 -07:00
Leonardo de Moura
fa9c5ad21a chore: remove mpq 2021-10-26 11:56:37 -07:00
Gabriel Ebner
61e0eab23f refactor: reimplement ofScientific for floats 2021-10-26 11:51:30 -07:00
Leonardo de Moura
0a3a8d2d3d feat: add mpn module 
This is the Z3 bignum module.
 2021-10-25 15:57:19 -07:00
Gabriel Ebner
ee2804d278 fix: use unsigned char in hash_str 
char has different signedness on various architectures (signed on amd64,
unsigned on aarch64).  oleans are then not architecture-independent
since they contain hashes (e.g. in mkStr).
 2021-10-21 22:08:49 +02:00
Chris Lovett
f57e61fead
chore: remove manual shell scripting for compiling libleanrt 2021-10-15 08:08:31 +02:00
Sebastian Ullrich
89d6c70273 fix: macOS build 2021-10-08 18:34:28 +02:00
Leonardo de Moura
106adb09b9 fix: simplify allocator 
Do not move segments between heaps.
We found yet another bug due to this "feature".
The crash is reported here:
https://gist.github.com/semorrison/490496060bbcfa8ea635f3d7be1ac824

@Kha summarized the "root of the evil" as:
using per-heap import lists while segments can be exchanged between heaps doesn't seem compatible.

This is the second bug due to this design decision.
We had fixed one here:
2283ebc5e9/src/runtime/alloc.cpp (L257-L269)

This commit fixes both issues by removing the segment exchange feature.
 2021-10-05 16:58:20 -07:00
Sebastian Ullrich
816dc1895f perf: reuse idle thread in favor of spawning new one 2021-09-25 07:34:12 -07:00
Sebastian Ullrich
70f99ab655 chore: placate GCC 2021-09-23 16:31:41 +02:00
Sebastian Ullrich
6eca75ddbd fix: include exported declarations in defining file 2021-09-20 18:41:46 +02:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Sebastian Ullrich
a7b044b80b chore: CI: build macOS without nix-shell 
GH Actions already comes with most dependencies and it seems to avoid an
issue with Zig libc++ compilation (because of OSX_DEPLOYMENT_TARGET?)
 2021-09-16 21:33:56 +02:00
Sebastian Ullrich
08c2c31fcd feat: IO.FS.removeDir(All) 2021-09-16 07:01:37 -07:00
Sebastian Ullrich
cd7968ba6a chore: IO.FS.removeFile: include path in error messages 2021-09-16 07:01:37 -07:00
Leonardo de Moura
218b9c87b0 feat: expose APIs for creating IO.Error objects 2021-09-11 17:14:43 -07:00
Leonardo de Moura
ca6941ab39 chore: rename lean_mpz_value 2021-09-11 17:00:47 -07:00
Leonardo de Moura
f9bc4b9b3a feat: add missing APIs 2021-09-11 15:39:11 -07:00
Leonardo de Moura
075ba63a8b feat: add LEAN_ABORT_ON_PANIC 2021-09-09 04:49:16 -07:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Sebastian Ullrich
82c97d34fa chore: specify accurate dependencies for leanshared 2021-08-20 09:42:05 -07:00
Sebastian Ullrich
5f4b1b1d44 Revert "Revert "feat: reintroduce libleanshared, link lean & leanpkg against it"" 
This reverts commit ccbc9d00db.
 2021-08-20 09:42:05 -07:00
Sebastian Ullrich
ccbc9d00db Revert "feat: reintroduce libleanshared, link lean & leanpkg against it" 2021-08-20 15:39:00 +02:00
Sebastian Ullrich
98b3e4b0ec chore: fix leanrt compilation flags 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
c867376a82 perf: generate separate libleanrt.a with local-exec TLS model for static linking 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
b7d723c982 refactor: compile runtime/ into new static library leanrt 2021-08-18 13:54:52 +02:00
Sebastian Ullrich
754286dc6d fix: compile flags for libleanruntime.bc 2021-08-18 13:54:52 +02: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
14b611af96 refactor: move buffer.h and *_ref.h files to runtime 2021-08-16 15:39:38 -07:00
Sebastian Ullrich
3c91c9e874 feat: try memory-mapping .olean files on Windows 2021-08-04 16:40:57 +02:00
Sebastian Ullrich
fbdcaab009 feat: show number of mmap-ed modules in --stats 2021-08-04 16:40:57 +02:00
Sebastian Ullrich
05abdf7848 perf: move root address of compacted region to the front 
for true zero-cost loading
 2021-08-04 16:40:57 +02:00
Sebastian Ullrich
4766ee0b5e feat: try to mmap() .olean files on Linux & macOS 2021-08-04 16:40:57 +02:00
Sebastian Ullrich
4d8da44f50 feat: allow specifying virtual base address for compacted region 2021-08-04 16:40:57 +02:00
Sebastian Ullrich
e25edf893c fix: mark MPZ objects in compacted regions as persistent 2021-07-27 16:35:42 +02:00
Leonardo de Moura
b986bde639 fix: IO.Error.alreadyExists may have an optional file name 
We got an assertion violation yesterday at `leanpkg` at
```cpp
  case EEXIST: case EINPROGRESS: case EISCONN:
        lean_assert(fname == nullptr);   // <<<<<<< HERE
        return lean_mk_io_error_already_exists(errnum, details);
```
 2021-07-27 07:00:06 -07:00
Sebastian Ullrich
450293e64a feat: zero-copy GMP deserialization 2021-07-26 07:11:05 -07:00
Wojciech Nawrocki
66258b012b chore: fix windows build 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
102236fdd9 chore: leftover comment 2021-07-24 10:45:28 +02:00