soonhokong
/
lean
/
693
/
1
76%
master: 76%
master: 76%
|
Ran
|
Files
198
|
Run time
–
|
Badge
Embed ▾
README BADGES
|
coverage: 91.009% (-0.2%) from 91.173%
push
travis-ci
leodemourafeat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed The modifications started at commit 1852c8694 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as: [x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈ ?M::22 x a After the changes, only very simple constraints are generated. The most complicated one is: [] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
17298 of 19007 relevant lines covered (91.01%)
292094.47 hits per line
Source Files on job 693.1 (CMAKE_CXX_COMPILER=g++-4.8 CMAKE_BUILD_TYPE=Debug TESTCOV=ON PUSH_TO_CDASH=TRUE TCMALLOC=OFF LUA=52)
| Coverage | ∆ | File | Lines | Relevant | Covered | Missed | Hits/Line |
|---|