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

622 commits

Author SHA1 Message Date
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
Sebastian Ullrich
1d403dffee chore: bin_lean should build bin_lean_stage0 first 2019-12-09 13:06:21 +01:00
Sebastian Ullrich
6195c31a04 chore: remove stdlib_ tests 2019-12-07 21:51:59 +01:00
Sebastian Ullrich
e98fdc4db6 chore: check-stage3 target for checking (eventually) deterministic bootstrap 2019-12-07 21:02:13 +01:00
Sebastian Ullrich
d5f30ddb83 fix: update-stage0 2019-11-27 05:53:22 -08:00
Sebastian Ullrich
98b83e96cb chore: do not build bin_lean_stage2 by default 2019-11-27 05:53:22 -08:00
Sebastian Ullrich
682ad9f605 feat: stage 2 and 3 builds 
While stage 1 is still the main build and the source of `bin/lean`, we now have optional targets
* lean_stage2, lean_stage3: build respective executable in `<build>/shell` from previous stage, compiling the stdlib
  from scratch
* bin_lean_stage2: copy `lean_stage2` to `bin/` (stage 3 should always be identical to stage 2)
 2019-11-27 05:53:22 -08: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
b21559b338 chore: move Makefile.in 2019-11-22 07:48:04 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -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
0571a1c913 chore: use paths instead of indices for stdlib tests 2019-11-20 08:07:28 -08:00
Leonardo de Moura
49f1f0dfe3 chore: apply required change after update-stage0 
cc @Kha
 2019-11-20 08:00:11 -08: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
Leonardo de Moura
eb52fbca10 chore: skip stdlib tests on Windows 2019-11-14 17:00:04 -08:00
Leonardo de Moura
bbe44a79f2 feat: add tests for compiling stdlib with stage1 
@Kha It seems to work. Not sure how robust it is. CMake is still very
mysterious to me :D
It is a partial test since I don't try to compile the files into .c.
I am not touching the compiler right now. So, it should be fine for now.

The command `ctest -j8 -R stdlib` also works.
 2019-11-13 20:55:08 -08:00
Sebastian Ullrich
04d5501eb2 chore: use proper nested make calls by hard-coding make as the build system 2019-11-13 08:13:21 -08:00
Sebastian Ullrich
60620360fc fix: Windows build 2019-11-12 13:07:12 +01:00
Sebastian Ullrich
91b68d8fa4 feat: cleanly separate bootstrap stages 2019-11-11 15:05:25 -08:00
Sebastian Ullrich
3e74159e01 fix: import errors using --json 2019-11-10 09:01:43 -08:00
Sebastian Ullrich
aa557a9d5a test: trivial linter test 2019-11-09 15:43:37 -08:00
Sebastian Ullrich
da69beac0a feat: add --plugin for loading shared libraries 2019-11-09 15:41:13 -08:00
Sebastian Ullrich
6912053fcc chore: always build stage 0 Lean binary, copy it to bin/lean_stage0 2019-10-28 18:11:44 -07:00
Leonardo de Moura
0714716477 fix: file and import names, tests and stage0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2019-10-04 17:04:02 -07:00
Sebastian Ullrich
3d53aaf5a7 chore(tests/compiler): ignore some tests for the interpreter 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
d5737d0713 test(shell/CMakeLists.txt): add compiler tests as interpreter tests 2019-09-12 18:22:02 +02:00