lean --export problems with #999

Stream: PR reviews

[Scott Morrison]

@Keeley Hoek and I have been having trouble with #999. lean --make and leanpkg test both work fine, but lean --recursive --export=mathlib.txt src/ says:

<unknown>:1:1: error: invalid object declaration, environment already has an object named 'tactic.mk_congr_arg_using_dsimp'

We've both checked, and there's just one such definition!

Does anyone know how to diagnose a problem like this?

[Simon Hudon]

And it's not generated through meta programming?

[Scott Morrison]

Nope, it's perfectly normal definition:

meta def mk_congr_arg_using_dsimp (G W : expr) (u : list name) : tactic expr :=
do s ← simp_lemmas.mk_default,
   t ← infer_type G,
   t' ← s.dsimplify u t {fail_if_unchanged := ff},
   definev `_mk_congr_arg_aux t' G,
   to_expr ```(congr_arg _mk_congr_arg_aux %%W)

[Mario Carneiro]

I assume you tried changing the name?

[Scott Morrison]

... let me try that now. :facepalm:

[Keeley Hoek]

@Mario Carneiro still fails :(

[Mario Carneiro]

my next test would be to take a hatchet to sections of mathlib to see what files are necessary to get the error

[Mario Carneiro]

Have you managed to repro the problem locally?

[Keeley Hoek]

yes

[Simon Hudon]

What's the conclusion?

[Keeley Hoek]

We have to chop mathlib into tiny little pieces to find out what's wrong

[Scott Morrison]

It seems that it was reporting the wrong error. There was a duplicate definition, but not the one that was being reported.