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

11609 commits

Author SHA1 Message Date
Leonardo de Moura
64adc4c798 feat(library/metavar_context): use MetavarContext implemented in Lean 2019-08-10 08:03:13 -07:00
Leonardo de Moura
aeae37eb81 feat(library/init/lean/metavarcontext): missing functions 2019-08-09 21:04:34 -07:00
Leonardo de Moura
99d4b33559 feat(library/metavar_context): metavar_decl as Lean object 2019-08-09 20:38:59 -07:00
Leonardo de Moura
5dd3b67a75 feat(library/metavar_context): delayed_assignment as Lean object 2019-08-09 20:30:52 -07:00
Leonardo de Moura
d924aab766 feat(library/init/lean/metavarcontext): export functions to C++ 2019-08-09 20:09:11 -07:00
Leonardo de Moura
d1671ffcea chore(library): remove dead code 2019-08-09 16:08:51 -07:00
Leonardo de Moura
b8cd88a827 chore(library/init): delete dead files 2019-08-09 10:35:38 -07:00
Sebastian Ullrich
de5c7cbff0 fix(shell/CMakeLists): bin_lean_stage0 should not be part of the default target as it conflicts with bin_lean 
/cc @leodemoura
 2019-08-09 16:43:19 +02:00
Leonardo de Moura
4aed3e51b5 chore(stage0): update 2019-08-09 07:40:54 -07:00
Sebastian Ullrich
3ed67138d5 chore(*): update equation syntax in files and old parser 
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
 2019-08-09 11:11:34 +02:00
Leonardo de Moura
30fc07014e chore(stage0): update 2019-08-07 17:46:48 -07:00
Leonardo de Moura
bf2a365501 chore(library/compiler/compiler): remove dead code 2019-08-07 17:24:07 -07:00
Leonardo de Moura
748e272dcb chore(stage0): update 2019-08-07 17:20:40 -07:00
Leonardo de Moura
73f96730bb feat(library/init/lean,kernel): add KernelException, addDecl and compileDecl 
This commit also refines the type of `addAndCompile`.
We also add `ElabException.kernel` constructor for kernel exceptions.
 2019-08-07 17:15:40 -07:00
Leonardo de Moura
d707026cd8 feat(library/local_context): ensure local_context is just a wrapper for LocalContext 
This is a temporary hack. After we eliminate the old elaborator,
we will delete the C++ class `local_context`.
In Lean4, we will not have two different kinds of local context:
`local_ctx` and `local_context`.
 2019-08-07 13:11:08 -07:00
Leonardo de Moura
8ac58a66f8 chore(library/abstract_type_context): remove unnecessary virtual method only used at old pp.cpp 2019-08-07 12:05:10 -07:00
Leonardo de Moura
fcba361bdf chore(stage0): update 2019-08-07 11:56:17 -07:00
Leonardo de Moura
ae97cfdd68 feat(kernel/local_ctx): use LocalContext 2019-08-07 11:50:20 -07:00
Leonardo de Moura
3967496ac9 chore(library/init/lean/default): make sure new modules are initialized 2019-08-07 07:14:09 -07:00
Leonardo de Moura
7a2ac23497 chore(library/init/lean/localcontext): export functions 2019-08-06 18:14:03 -07:00
Leonardo de Moura
bad3f8e77e chore(kernel/local_ctx): use new representation defined at localcontext.lean 2019-08-06 10:47:50 -07:00
Leonardo de Moura
2343260ca5 chore(stage0): update 2019-08-06 10:39:02 -07:00
Leonardo de Moura
b27f215b9a chore(library/local_context): simplify pp 2019-08-06 10:27:10 -07:00
Leonardo de Moura
f1eaebba31 fix(library/compiler/csimp): bug at float_cases_on 
The scope of the expr2ctor cache updates was incorrect.
This bug affects code of the form
```
let x := C.cases_on y ...; K[x]
```
when we try to float the `cases_on` application, and the continuation
`K[x]` contains another `cases_on` application with major `y`.
The new test exposes the bug.
This commit also fixes the case where the continuation `K[x]` projects `y`.

Fixes #26
 2019-08-05 13:23:27 -07:00
Leonardo de Moura
99e90f0410 chore(library/compiler): add trace.compiler.simp_float_cases option 2019-08-05 13:13:18 -07:00
Leonardo de Moura
215a3ac8fd chore(library/tactic/clear_tactic): remove dead code 2019-08-05 08:58:59 -07:00
Leonardo de Moura
1b426db5d9 chore(stage0): update 2019-08-04 13:25:25 -07:00
Leonardo de Moura
34024256ab chore(library/init/lean/expr): simplify Expr.mvar constructor 2019-08-04 13:24:27 -07:00
Leonardo de Moura
4181f35546 chore(stage0): update 2019-08-04 09:30:52 -07:00
Leonardo de Moura
8a8b45b6e0 chore(stage0): update 2019-08-04 08:41:19 -07:00
Leonardo de Moura
1ef23950a4 chore(library/init/lean/expr): expose temporary legacy constructor 2019-08-04 08:03:09 -07:00
Leonardo de Moura
41d8cd9eb9 chore(kernel/expr): remove depth and weight fields 
These fields were rarely used, but they were used in the hash code
calculation. So, we may see a negative performance impact.
There is also a positive performance impact since `Expr` consumes less
memory, and it is faster to allocate them.
 2019-08-03 11:05:01 -07:00
Leonardo de Moura
7f142ac7e3 chore(kernel/expr): hide get_weight and get_depth 2019-08-03 10:57:30 -07:00
Leonardo de Moura
d2f169a211 chore(library/init/lean/parser/parser): remove unnecessary unsafe code 2019-08-02 14:32:47 -07:00
Leonardo de Moura
1be9ee97be chore(stage0): update 2019-08-02 14:26:22 -07:00
Leonardo de Moura
9e53db95ba chore(CMakeLists): set default to OFF 
@joehendrix I changed the default to `LLVM=OFF` for now to avoid
disrupting existing projects. It will become `LLVM=ON` after we have
tested it more, and have the JIT integrated.

@kha Could you please set a new Azure pipeline job for `LLVM=ON`?
 2019-08-01 10:15:43 -07:00
Joe Hendrix
a113832342 chore(CMakeLists): Typo 2019-07-31 18:21:49 -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
b221b09ad5 chore(library/init, frontends/lean): ensure old and new parser use the same command for initializing quotient module 2019-07-31 17:07:05 -07:00
Leonardo de Moura
b0c84874ba chore(runtime/compact): add additional comments 2019-07-30 17:58:15 -07:00
Sebastian Ullrich
55104ad0c6 chore(library/compiler/csimp): remove wrong assertion 2019-07-30 17:52:43 -07:00
Sebastian Ullrich
2c12f9d0f6 chore(runtime/object): LEAN_FAKE_FREE: assert on double-free 2019-07-30 17:52:43 -07:00
Sebastian Ullrich
d09c512784 chore(library/module): lsan: ignore module objects 2019-07-30 17:52:43 -07:00
Sebastian Ullrich
20b6502aaf fix(runtime/compact): badly aligned "field" in terminator 2019-07-30 17:52:43 -07:00
Leonardo de Moura
2f5b2b2409 feat(library/init/lean/path): add realPathNormalized 2019-07-28 20:52:41 -07:00
Leonardo de Moura
4b10f09baf chore(stage0): update 2019-07-28 20:13:01 -07:00
Leonardo de Moura
6cf8571e37 feat(library/init/system/platform): add System.Platform.isOSX 2019-07-28 19:49:40 -07:00
Leonardo de Moura
17e5f0b719 chore(stage0): update 2019-07-28 09:54:57 -07:00
Leonardo de Moura
fb14110b22 fix(library/compiler/llnf): sort scalar fields by size to avoid UB 2019-07-28 09:53:53 -07:00