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

354 commits

Author SHA1 Message Date
Leonardo de Moura
1dc9f9a7d8 chore: remove old names 2020-02-28 10:53:42 -08:00
Leonardo de Moura
4a05a2568a chore: add new primitive names 2020-02-28 10:53:41 -08:00
Leonardo de Moura
1f8bfa0c11 chore: rename maxsharing.cpp => sharecommon.cpp 2020-02-28 10:53:41 -08:00
Leonardo de Moura
966e5bc60d perf: remove "filler" fields 
See previous commit.
 2020-02-27 10:02:26 -08:00
Leonardo de Moura
e5d824a748 feat: initialize last word 
Motivation: trying to get rid of explicit "filler" fields because
they slow down modules such as `RBMap`.
 2020-02-27 10:02:26 -08:00
Leonardo de Moura
657f3792b1 feat: maxsharing scalar arrays 2020-02-25 18:08:49 -08:00
Leonardo de Moura
131f2d202e chore: ignore closures at maxsharing 
Closures may capture huge objects that user may be unaware.
For example, any closure created by the interpreter contains
a reference to the `Environment`.

@dselsam @kha I don't see many applications for maximizing sharing in
values captured by closures. If we want this feature, we should at
least wrap the `Environment` and `Decl` using external objects
at `mk_stub_closure` at `ir_interpreter.cpp`.
 2020-02-25 17:13:05 -08:00
Leonardo de Moura
1653e75b6b feat: maxsharing for arrays and strings 2020-02-25 16:15:26 -08:00
Leonardo de Moura
46e8d193ca feat: maxsharing for constructors 2020-02-25 15:43:10 -08:00
Leonardo de Moura
d8ed4165b0 chore: remove cnstr_get_scalar and cnstr_set_scalar 2020-02-25 13:28:23 -08:00
Leonardo de Moura
74d08e47e5 chore: style 2020-02-24 21:04:48 -08:00
Leonardo de Moura
dae1a3172e fix: maxsharing hash and eq, and expand skeleton 2020-02-24 21:00:01 -08:00
Leonardo de Moura
fdc76934f5 feat: max_sharing_fn skeleton 2020-02-24 19:50:37 -08:00
Leonardo de Moura
f84e1c2fbd feat: add dummy implementation of MaxSharing primitives 2020-02-24 19:30:53 -08:00
Leonardo de Moura
46fd5ed929 feat: maxSharing primitives 2020-02-24 19:23:45 -08:00
Leonardo de Moura
d6a7e9a308 chore: remove mutquot primitives 2020-02-24 14:28:32 -08:00
Leonardo de Moura
a897f7e7f3 chore: style nonsense 2020-02-06 17:06:36 -08:00
Leonardo de Moura
224fe05d51 feat: reset memory 2020-02-06 16:56:25 -08:00
Leonardo de Moura
469562d524 feat: maximize sharing at compact 2020-02-06 16:39:20 -08:00
Leonardo de Moura
9eef6851be chore: track number of objects 2020-02-06 14:58:20 -08:00
Leonardo de Moura
660571ab38 fix: closes #109 
Fixed myself after wasting time wondering whether a segfault was
coming from today.

cc @cipher1024
 2020-02-05 09:16:33 -08:00
Leonardo de Moura
eacff1a448 feat: implement withPtrEq and withPtrAddr 2020-02-04 17:48:11 -08:00
Leonardo de Moura
38e6961003 feat: MutQuot by implementedBy 2020-02-04 16:51:08 -08:00
Leonardo de Moura
ac88b46299 feat: MutQuot primitives 2020-02-04 15:56:20 -08:00
Leonardo de Moura
3d0bfcd36a fix: assertion violation 2020-01-31 08:25:59 -08:00
Sebastian Ullrich
2509b3913a Revert "feat: add std streams" 
This reverts commit 7575a32035.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
0be2424910 Revert "feat: override standard streams" 
This reverts commit bd87ea5d5e.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
b760692a26 Revert "fix: thread local storage of std streams" 
This reverts commit 961861ceab.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
58313a050a Revert "fix: #eval redirection of stdout" 
This reverts commit 123577126c.
 2020-01-25 16:32:06 +01:00
Sebastian Ullrich
ad29568051 Revert "fix: redirect" 
This reverts commit addbb8dd67.
 2020-01-25 16:32:06 +01:00
Leonardo de Moura
addbb8dd67 fix: redirect 
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
  old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
  decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
  with `O`, but `H'` RC is not decremented.
 2020-01-23 15:58:34 -08:00
Simon Hudon
123577126c fix: #eval redirection of stdout 2020-01-23 15:44:49 -08:00
Leonardo de Moura
67fb63c9fd feat: use mpz_pow_ui to implement Nat.pow 2020-01-21 09:16:38 -08:00
Simon Hudon
961861ceab fix: thread local storage of std streams 2020-01-19 17:23:24 -08:00
Simon Hudon
bd87ea5d5e feat: override standard streams 2020-01-19 17:23:12 -08:00
Simon Hudon
7575a32035 feat: add std streams 
This reverts commit 021ce21d5f70c2efcc58a0588ed6dc4999be6a33.
 2020-01-19 17:22:58 -08:00
Simon Hudon
6d8927da10 fix: little details 2020-01-12 08:02:48 -08:00
Simon Hudon
92c8773137 feat: file IO using handles 2020-01-12 08:02:48 -08:00
Leonardo de Moura
48578c9743 chore: remove hacks 2020-01-08 21:09:17 -08:00
Leonardo de Moura
981e35b6da chore: style 2020-01-08 21:09:17 -08:00
Leonardo de Moura
4550e75dcb chore: temporary hack for solving staging issue 2020-01-08 21:09:17 -08:00
Leonardo de Moura
01c5b0710c feat: pointer equality for IO.ref 2020-01-08 21:09:17 -08:00
Sebastian Ullrich
f171404530 fix: "superficial" leaks to shut up lsan 2019-12-22 17:23:51 -08:00
Sebastian Ullrich
3b37737c8a fix: leaks 2019-12-22 15:09:19 -08:00
Leonardo de Moura
74f48414f1 feat: add option --exitOnPanic (short version -e) 
Lean does not exit on panic anymore.
The old behavior (`std::exit(1)`) produces a horrible debugging
experience for the elaborator since all trace messages are lost.
The new command line option restores the old behavior.

cc @Kha @dselsam
 2019-12-19 09:24:37 -08:00
Leonardo de Moura
54e5ca0c7b fix: lean_nat_abs 
It must not assume a nonnegative big integer is a big nat.
 2019-12-14 08:08:41 -08:00
Sebastian Ullrich
ae3b3bb825 chore: remove cygwin support 2019-11-12 08:28:58 -08:00
Sebastian Ullrich
d8bb4df96f chore: revert "chore: add std::cout.flush" 
This reverts commit a43a225013.
 2019-11-06 10:13:39 -08:00
Leonardo de Moura
00af75accf chore: style 
fix nonsense
 2019-10-29 14:50:22 -07:00
Leonardo de Moura
4b7b95cd76 fix: missing file 
LEAN_SMALL_ALLOCATOR is defined at `config.h`
 2019-10-29 14:48:02 -07:00