4219
96%
master: 85%

Ran 09 Dec 2018 05:06PM UTC

Jobs 2

Files 0

Run time –

Badge

Embed ▾

pending completion

Build # 4219

Build Type

push

travis-ci

Committed by

leodemoura

Commit Message

feat(frontends/lean): force user to use `meta` keyword on meta inductive/structure/class

Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.

Run Details

Jobs

ID	Job ID	Ran	Files	Coverage
7	4219.7 (CMAKE_CXX_COMPILER=clang++-3.4 CMAKE_BUILD_TYPE=Release TCMALLOC=OFF PUSH_TO_CDASH=TRUE)	09 Dec 2018 05:06PM UTC	0		Travis Job 4219.7
8	4219.8 (CMAKE_CXX_COMPILER=g++-4.9 CMAKE_BUILD_TYPE=Release TCMALLOC=OFF UPLOAD=linux PUSH_TO_CDASH=TRUE CONSERVE_MEMORY=ON)	09 Dec 2018 05:10PM UTC	0		Travis Job 4219.8

Source Files on build 4219

Detailed source file information is not available for this build.

leanprover / lean / 4219
96%
master: 85%

README BADGES
x

Markdown

Textile

RDoc

HTML

Rst

Jobs

Source Files on build 4219

leanprover / lean / 4219 96% master: 85%

README BADGES x

Markdown

Textile

RDoc

HTML

Rst

Jobs

Source Files on build 4219

leanprover / lean / 4219
96%
master: 85%

README BADGES
x