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

381 commits

Author SHA1 Message Date
Leonardo de Moura
e3b1ae514b fix: nontermination 
This issue was reported by Simon Winwood at Zulip.
Here is the message

The following code doesn't terminate (in a reasonable amount of time)
```
def large_nat : Nat := (9223372036854775807 : Nat)
```
$ time lean --o=large-nat.olean large-nat.lean
 2020-08-18 18:45:28 -07:00
Sebastian Ullrich
edeed7b849 chore: fix C++ warnings 2020-08-14 14:42:44 +02:00
Wojciech Nawrocki
55655869b7 feat: default to binary file mode on Windows 2020-08-13 09:21:35 -07:00
Sebastian Ullrich
c38f4fe837 feat: unsafe functions for freeing compacted regions 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
6404af6983 feat: IO.Prim.withIsolatedStreams 2020-06-16 10:41:42 -07:00
Sebastian Ullrich
f4c28fbe5f chore: remove unnecessary getByte/putByte IO primitives 2020-06-16 12:06:53 +02:00
Simon Hudon
a64e78b90b feat: add std streams 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2020-06-16 12:06:53 +02:00
Leonardo de Moura
2f1ec93289 chore: move runtime implementation to src/runtime 2020-05-22 14:35:16 -07:00
Leonardo de Moura
1a77ee4f89 chore: delete old runtime directory 2020-05-18 11:33:18 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Sebastian Ullrich
9fdcf6ea59 refactor: put all includes in include/lean/ 2020-05-18 11:00:26 -07:00
Sebastian Ullrich
10253e89ea chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
5d260c396f fix: macOS build 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
be79820a47 feat: add IO.currentDir 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
5107403d24 feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
Sebastian Ullrich
7899ab3761 feat: report stack overflows as such on Linux 
Port of the corresponding Rust code (Apache/MIT)
 2020-04-30 13:16:42 -07:00
Leonardo de Moura
e22af8d1ef feat: add FloatArray 
cc @dselsam
 2020-04-07 18:05:54 -07:00
Leonardo de Moura
8e84a8c9ec feat: Float from big numbers 2020-04-06 14:05:17 -07:00
Leonardo de Moura
acad6015c4 chore: add new primitives to object.h 2020-04-03 18:26:13 -07:00
Leonardo de Moura
64c3be44f8 fix: lean_unbox_float 2020-04-03 18:23:45 -07:00
Leonardo de Moura
8e952f3c36 chore: style 2020-04-03 17:48:06 -07:00
Leonardo de Moura
c236a179f2 feat: enable externs 2020-04-03 17:19:48 -07:00
Leonardo de Moura
71397aad36 feat: runtime primitives 2020-04-03 15:55:39 -07:00
Leonardo de Moura
098b0edbcb chore: remove dead code 2020-03-23 15:56:29 -07:00
Leonardo de Moura
2cc0f25bf5 feat: getLine at EOF should return empty string 
This is the same approach used in Rust, and it simplifies the code.
 2020-03-23 15:44:47 -07:00
Leonardo de Moura
b2bddb5606 chore: style 2020-03-23 14:06:02 -07:00
Leonardo de Moura
db914052ce fix: IO.getLine 2020-03-23 12:26:09 -07:00
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