Sebastian Ullrich
e5a9820830
chore: fix test
2021-01-27 15:04:59 +01:00
Sebastian Ullrich
7e521f0105
chore: remove remaining #lang lean4 in tests
2021-01-27 14:45:31 +01:00
Leonardo de Moura
3de97ddc27
feat: run linters in the new frontend
2020-10-23 14:04:28 -07:00
Leonardo de Moura
dbbacb3bfd
chore: remove comment from Linter
...
Old frontend is just providing `Syntax.missing`
2020-06-17 21:28:03 -07:00
Leonardo de Moura
17b6957f6c
chore: fix tests
2020-05-26 15:05:01 -07: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
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
Simon Hudon
92c8773137
feat: file IO using handles
2020-01-12 08:02:48 -08:00
Sebastian Ullrich
3cce06ca78
chore: add tests/plugin/.gitignore
2019-12-05 13:21:08 +01:00
Leonardo de Moura
cff6a1d117
chore: fix tests
2019-11-22 08:03:22 -08: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
1f601708e4
fix: print messages to stderr
...
This ensures that errors during dependency resolution in the Makefile actually show up
2019-11-10 09:01:43 -08:00
Sebastian Ullrich
aa557a9d5a
test: trivial linter test
2019-11-09 15:43:37 -08:00
