help with travis

Stream: general

[Scott Morrison]

Hmm, a strange error:

> lean --make .
> lean --make test
> lean --recursive --export=mathlib.txt
<unknown>:1:1: error: invalid object declaration, environment already has an object named 'category_theory.limits.category_theory.limits.has_limits._proof_1'

[Scott Morrison]

How come it doesn't complain with lean --make?

[Scott Morrison]

Is this that two files, which are never imported in the same place, have the same named definition? And this isn't detected until the last run of lean?

[Scott Morrison]

(Doesn't matter too much, there was an instance that should have been a def anyway, that should solve this.)

[Simon Hudon]

Is this that two files, which are never imported in the same place, have the same named definition? And this isn't detected until the last run of lean?

That's right