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

337 commits

Author SHA1 Message Date
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
bdea7c7b14 feat: lean: initialize task manager from -j flag 2020-09-14 17:57:33 +02: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
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -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
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
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
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
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
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
5e1fd62ae4 fix: --make without argument should not segfault 2019-12-10 16:37:18 +01:00
Sebastian Ullrich
2ad21d0f4c feat: have --make take an optional .olean filename argument 
Not documented since it is mostly useful for internal builds of further bootstrap stages
 2019-11-27 05:53:22 -08:00
Leonardo de Moura
4adacf1413 chore: src/init ==> src/initialize 2019-11-22 04:59:13 -08:00
Sebastian Ullrich
f6973be5e3 refactor: replace C++ import parser with Lean one 
imports are now completely opaque to C++
 2019-11-21 15:52:01 +01:00
Sebastian Ullrich
44d5eddf16 chore: remove support for relative imports 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
33ce758126 feat: assume A in --plugin A.so is package name and use it to synthesize initializer symbol name 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
3dcd4febd9 feat: make LEAN_PATH a mapping from package names to root dirs, remove C++ impl 2019-11-20 16:39:53 +01:00
Sebastian Ullrich
3e74159e01 fix: import errors using --json 2019-11-10 09:01:43 -08:00
Sebastian Ullrich
da69beac0a feat: add --plugin for loading shared libraries 2019-11-09 15:41:13 -08:00
Sebastian Ullrich
795359ee49 feat(shell/lean): re-add --run flag 2019-09-12 18:22:02 +02:00
Leonardo de Moura
f697381410 feat(shell/lean.cpp): use C backend for --cpp option 2019-08-24 07:40:56 -07:00
Leonardo de Moura
6d6cb14f9e feat(library/init/lean/compiler/ir/emitc,shell/lean): add --c=<filename> option 2019-08-20 10:13:40 -07:00
Leonardo de Moura
b2693962bd chore(library/init/lean): export as C functions 2019-08-17 07:30:07 -07:00
Joe Hendrix
37ff241467 feat(CMakeLists): Add option to link in LLVM. 
This updates cmake and Lean to link against the LLVM libraries.
 2019-07-31 18:21:49 -07:00
Leonardo de Moura
1016309d1f feat(library/init/lean/path): always add builtin search path 
We also add "." (i.e., current directory) if `LEAN_PATH` is not defined.
Users may still override stdlib since we add the builtin search path in the end.

@dselsam You should now be able to compile your project without setting `LEAN_PATH`

cc @kha
 2019-07-31 18:13:17 -07:00
Leonardo de Moura
ff6b868440 chore(library/module): remove dead code 2019-07-27 19:03:07 -07:00
Leonardo de Moura
943f6cbd55 chore(library/module): use module_name_of_file in Lean 2019-07-27 18:59:54 -07:00
Leonardo de Moura
fda2cd23ec chore(shell/lean): use find_lean_file in Lean 2019-07-27 18:38:27 -07:00
Leonardo de Moura
dea1e52c96 feat(shell/lean): initialize searchPath implemented in Lean 2019-07-26 16:15:38 -07:00
Sebastian Ullrich
53a26b94ff chore(util/lean_path): remove leanpkg.path support 
Because Lean 4 will not compile dependencies by itself, there is not much of a
point in it resolving them by itself either. The build tool that ensures that
all dependencies have been built should call `lean` with the `LEAN_PATH`
environment variable set accordingly.
 2019-07-25 17:46:40 -07:00
Leonardo de Moura
f0899b381d feat(library/init/lean/parser/module): add displayStx param 2019-07-17 19:09:15 -07:00
Leonardo de Moura
12346d344a feat(shell/lean): invoke new parser when --new-frontend is used 2019-07-15 13:57:05 -07:00
Sebastian Ullrich
826a5ee16b chore(shell/lean): profile initialization time 2019-07-05 16:21:48 +02:00
Leonardo de Moura
70a1589817 refactor(library/init/lean): move extern.lean to compiler subdirectory 2019-06-25 08:59:55 -07:00
Leonardo de Moura
b2ae4c51af chore(shell/lean): cleanup 2019-06-07 14:52:16 -07:00
Leonardo de Moura
fc4abbd6c3 chore(shell/lean): compilation warning 2019-06-06 10:42:39 -07:00
Leonardo de Moura
55626ba60d chore(library/init/lean): disable new frontend for now 
We are going to start making drastic changes in the parser,
elaborator, attributes, etc. Examples:
- No View objects. I am going to implement match_syntax.
- No RecT in the parser. I am going to implement parser extensions
using an approach similar to the one I used to implement environment
extensions.
- No Parsec. I will use an approach similar to the one used in the
experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser

It is easier to perform these changes with the new frontend disabled.
I will slowly re-active it as I apply the changes.

cc @kha
 2019-06-05 15:26:43 -07:00
Leonardo de Moura
cd73105dff refactor(kernel/environment,library/private,library/init/lean/environment): move main module name to header 2019-06-03 09:14:23 -07:00