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

315 commits

Author SHA1 Message Date
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
Leonardo de Moura
356a4fafcd chore(library/compiler): remove old code 
@kha I am removing the old IR compiler. If there is a disaster with
the new one implemented in Lean, I will put it back.
 2019-05-27 21:28:22 -07:00
Leonardo de Moura
5d04027050 chore(tests/playground): scripts for using old IR compiler 2019-05-23 18:33:29 -07:00
Leonardo de Moura
f72d54c2a0 chore(shell/lean): set new IR compiler as the default 2019-05-23 18:27:41 -07:00
Sebastian Ullrich
29623cd2c5 fix(shell/lean): --cpp on stand-alone files 2019-05-22 23:23:30 +02:00
Leonardo de Moura
3ffe0e22c8 feat(shel/lean): add temporary option for testing new IR compiler code emitter 2019-05-20 10:19:09 -07:00
Leonardo de Moura
aa138fe686 chore(*): get_obj_arg => to_obj_arg 2019-05-16 14:42:02 -07:00
Leonardo de Moura
9d9f546ad8 refactor(util/sexpr): move options and option_declarations to util 2019-05-16 14:37:24 -07:00
Leonardo de Moura
9c4da289b2 refactor(util/sexpr/options): options as a Lean object 2019-05-16 14:27:44 -07:00
Leonardo de Moura
31d4fa9f71 chore(util/sexpr/options): shrink options API 
Motivation: move to the Lean implementation
 2019-05-16 14:08:11 -07:00
Sebastian Ullrich
7a19f246e6 fix(shell/lean): re-add missing short-only option 2019-05-16 10:27:18 +02:00
Leonardo de Moura
77768c504e feat(shell/lean): import time stats 2019-05-15 17:16:19 -07:00
Leonardo de Moura
3193e91aff feat(library/init/lean/environment): add Environment.displayStats and --stats command line argument 2019-05-15 11:01:25 -07:00
Leonardo de Moura
67d14705b0 chore(library/module): simplify write_module 2019-05-14 08:08:09 -07:00
Leonardo de Moura
22d2848d21 chore(library/module): store search_path in a global variable 
Remark: I will use it to expose the following primitive in Lean
```
constant findOLean : Name -> IO String
```
 2019-05-14 07:49:00 -07:00
Leonardo de Moura
358b731581 chore(library/module): simplify import_modules 
Remark: `lean.cpp` is a total mess at this point. It contains
leftovers from the Lean2 and Lean3 designs, and hacks for supporting
the Lean4 transition.
 2019-05-14 07:26:50 -07:00
Leonardo de Moura
99e3cdc01b chore(frontends/lean): delete lean_environment 2019-05-13 13:05:04 -07:00
Leonardo de Moura
fd487d8db7 chore(*): remove old VM 2019-05-08 15:15:44 -07:00
Sebastian Ullrich
7c0912d41c refactor(frontends/lean/lean_environment): move environment parts out of lean_elaborator.cpp 2019-03-25 16:12:14 +01:00
Leonardo de Moura
3d52298c69 chore(util/sexpr): preparing to port options to Lean 2019-03-22 13:58:16 -07:00
Sebastian Ullrich
5f7a63b34b feat(shell/lean): accept stand-alone files as input 
@leodemoura
 2019-03-22 14:05:10 +01:00
Leonardo de Moura
d45da2d5ba fix(shell/lean): check whether output file was created or not 2019-03-18 12:44:28 -07:00
Leonardo de Moura
9984d28bb2 fix(library/init/lean/frontend): make sure new frontend works with new io monad 2019-03-16 18:24:53 -07:00