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

650 commits

Author SHA1 Message Date
Leonardo de Moura
4f109e23c2 feat: return syntax object representing the whole file 2020-10-21 07:55:59 -07:00
Sebastian Ullrich
438b3351dd feat: add interpreter.prefer_native option 2020-10-21 11:21:56 +02:00
Leonardo de Moura
e54a207986 refactor: provide Options to lean_eval_const 
add `ImportM` monad for `addImportedFn`

cc @Kha
 2020-10-19 10:21:38 -07:00
Leonardo de Moura
ef01053d58 fix: set mainModuleName in the new frontend 2020-10-15 15:30:03 -07:00
Leonardo de Moura
4f78142ed6 fix: add temporary hack 
@Kha This was my first unrecoverable bug. I had to backtrack
approx. 10 commits when I noticed this bug and I couldn't build the
system anymore.
 2020-10-14 17:28:34 -07:00
Leonardo de Moura
36220b785e feat: make new frontend compatible with lean4-mode 2020-10-14 13:20:01 -07:00
Leonardo de Moura
6047d7c2b6 feat: quick and dirty #lang annotation 2020-10-14 13:20:01 -07:00
Sebastian Ullrich
67684db0c3 chore: delete more CMake cruft 2020-10-14 19:08:06 +02:00
Sebastian Ullrich
c54d51b0c9 chore: go back to previous bootstrapping scheme where the stage N+1 stdlib is created using the stage N compiler 2020-09-24 18:57:53 +02:00
Sebastian Ullrich
308b4fc421 chore: always remake leanmake tests 2020-09-24 18:57:53 +02:00
Sebastian Ullrich
bdea7c7b14 feat: lean: initialize task manager from -j flag 2020-09-14 17:57:33 +02:00
Wojciech Nawrocki
098c7af1b6 feat: server tests 2020-08-31 06:50:01 -07:00
Sebastian Ullrich
6f7a557e5a feat: add --root flag to set package root directory 2020-08-06 09:21:52 -07:00
Sebastian Ullrich
fb02fbb867 fix: freeing Environments in tests 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
c38f4fe837 feat: unsafe functions for freeing compacted regions 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
0f6b9f5c94 chore: clean up stage 0 executable build 
Previously we were building identical libInit/Std/Lean.a from the same stage0/stdlib sources. Now we simply link
everything right into libleancpp.a, again.
 2020-07-03 19:26:00 +02:00
Sebastian Ullrich
46065a9b3b feat: leanmake: auto-detect PKG 2020-06-13 15:22:01 +02:00
Leonardo de Moura
f7818757ef chore: add Lean package to CMakeLists.txt 2020-05-26 13:50:04 -07:00
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
ae3a433f9c chore: add Std to CMakeLists.txt 
@Kha did I miss anything?
 2020-05-22 11:19:14 -07:00
Sebastian Ullrich
f45fcb4898 test: add tests/compiler/foreign and doc/examples/compiler 2020-05-22 09:22:26 -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
78a3305764 chore: duplicate install file 2020-05-18 14:51:18 +02:00
Sebastian Ullrich
a6fbf3c20e refactor: make stages internally consistent by compiling the stageN lib with the stageN compiler, rename static libraries 
The old stage1 is now stage0.5, which at least suggests that it's not an entirely consistent stage in general
 2020-05-14 23:13:51 +02:00
Sebastian Ullrich
aa3bca1cf5 refactor: make Makefile reusable 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
342675181a fix: build 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
279746fa6a chore: change stage1-3 into homogeneous ExternalProjects from new top-level /CMakeLists.txt 
This ensures stage2+3 are full, standalone Lean installations
 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
10253e89ea chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
73b4cf329d fix: Windows build 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
5f1a052998 feat: replace --make with -o flag that takes an explicit .olean target file name 2020-05-14 14:47:54 +02:00
Sebastian Ullrich
872d5fc7ba feat: stop compiling Lean code as C++, remove --cpp option 
Since we don't use static initializers, really the only difference between using `clang` and `clang++` is the default
inclusion of the C++ standard library.
 2020-05-14 14:45:33 +02:00
Sebastian Ullrich
053d4bab1c chore: factor out and unify common test behavior; retrieve lean from PATH 
`./test_single.sh foo.lean yes` is now `./test_single.sh -i foo.lean`
 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
bc40796729 chore: remove fail/ tests 
Checking for *any* failure is never a good idea. Use `$f.expected.ret` instead.
 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
a5382f45ff chore: stop normalizing the input path in error messages 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
76a97ea4fc feat: infer module name from cwd instead of LEAN_PATH, also make build system less specific to Init/ 2020-05-14 14:38:52 +02:00
Sebastian Ullrich
e7920bcdb5 chore: remove test special case 2020-05-04 11:11:11 +02:00
Sebastian Ullrich
ea85f3a318 fix: make install... 2020-03-11 15:20:56 +01:00
Sebastian Ullrich
1b5ace4c39 chore: profile C code generation time 2020-03-06 17:20:25 +01:00
Leonardo de Moura
796fff26d2 fix: check_optarg 2020-02-29 07:25:30 -08:00
Leonardo de Moura
5ff62ebf06 feat: check user given path 2020-02-05 09:42:26 -08:00
Leonardo de Moura
9993eb9b2b fix: increase scope of try 
Motivation: avoid "libc++abi.dylib: terminating with uncaught
exception of type lean::exception ..."
 2020-02-05 09:27:54 -08:00
Simon Hudon
92c8773137 feat: file IO using handles 2020-01-12 08:02:48 -08:00
Leonardo de Moura
6c474a1eb6 test: add tests/lean/newfrontend 
cc @Kha
 2020-01-06 14:07:22 -08:00
Leonardo de Moura
9f2172e65e feat: use new frontend when option --new-frontend is provided 2020-01-06 14:02:58 -08:00
Leonardo de Moura
3fb3b34762 chore: disable test 2020-01-06 13:42:29 -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
Sebastian Ullrich
f183ea6fae chore: reenable test 
/cc @leodemoura
 2019-12-14 12:09:04 +01:00
Leonardo de Moura
6ee5aa5276 chore: disable test 
@Kha I will try to figure out why it is broken later.
 2019-12-13 17:54:40 -08:00
Sebastian Ullrich
0c9f01ac18 fix: truly separate stage2/3 builds by copying all sources 2019-12-11 09:45:01 -08:00
Sebastian Ullrich
5e1fd62ae4 fix: --make without argument should not segfault 2019-12-10 16:37:18 +01:00