Zulip Chat Archive

Stream: PR reviews

Topic: lean --export problems with #999


view this post on Zulip Scott Morrison (May 17 2019 at 01:31):

@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?

view this post on Zulip Simon Hudon (May 17 2019 at 02:39):

And it's not generated through meta programming?

view this post on Zulip Scott Morrison (May 17 2019 at 04:57):

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)

view this post on Zulip Mario Carneiro (May 17 2019 at 04:58):

I assume you tried changing the name?

view this post on Zulip Scott Morrison (May 17 2019 at 05:00):

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

view this post on Zulip Keeley Hoek (May 17 2019 at 06:14):

@Mario Carneiro still fails :(

view this post on Zulip Mario Carneiro (May 17 2019 at 06:15):

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

view this post on Zulip Mario Carneiro (May 17 2019 at 06:15):

Have you managed to repro the problem locally?

view this post on Zulip Keeley Hoek (May 17 2019 at 06:16):

yes

view this post on Zulip Simon Hudon (May 17 2019 at 17:07):

What's the conclusion?

view this post on Zulip Keeley Hoek (May 18 2019 at 00:11):

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

view this post on Zulip Scott Morrison (May 18 2019 at 01:41):

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


Last updated: May 09 2021 at 12:14 UTC