Instance files

Stream: general

[Yaël Dillies]

Can we please stop creating concrete type-specific files? This just calls for weird import loops.

[Kevin Buzzard]

Don't we have files containing all instances for punit and pi? Won't it just be the same as those? Oh I see -- the issue is that you want it to be a monoid so you need to import it early, but then you want it to be a totally ordered normed vector space so you need to import a load of stuff before it :-/

[Yaël Dillies]

Eric, I mean files like algebra.punit_instances

[Eric Wieser]

But file#algebra/group/pi is fine, right?

[Yaël Dillies]

Meh, not really either.

[Yaël Dillies]

Not everything fits in a file, so we also have file#data/pi/algebra

[Eric Wieser]

That file is different, it's data-only without any algebraic heirarchy

[Yaël Dillies]

has_one and friends are in the algebraic hierarchy.

[Yaël Dillies]

But I agree that somehow pi and prodare less of a problem than type synonyms.

[Eric Wieser]

That's just notation, I wouldn't consider those algebraic

[Eric Wieser]

In the interest of unblocking things, I think order/ulift.lean and algebra/order/ulift.lean are close enough to the status quo

[Eric Wieser]

We also have algebra/order/pi as a data point in favor of that

[Yaël Dillies]

Why not just dropping the instances in the corresponding files? This is no harder.

[Eric Wieser]

Why not follow the pattern of pi and prod and keep the files smaller?

[Yaël Dillies]

... because it's type synonym

[Eric Wieser]

So?

[Eric Wieser]

I think you're thinking of order_dual, which is a very important type synonym because you use it to prove everything along the way

[Eric Wieser]

ulift you don't use for anything until a leaf file

[Yaël Dillies]

I want to destroy those type synonym instances files, so I don't want another one to pop up.

[Kevin Buzzard]

@Johan Commelin this is why ulift nat isn't a partial order -- apparently there are subtleties ;-)

[Yaël Dillies]

Classes can be defined arbitrarily low in the instance hierarchy, and all the prod/pi files have to decide of an arbitrary cutting point.

[Eric Wieser]

Yael, can you pick one of your messages to split this thread, and I'll use my mod powers to clean up the rest?

[Yaël Dillies]

In particular, the order folder is very flat, so there's little opportunity to have several .ulift files, as we do under algebra. (algebra.group.pi, algebra.order.pi)

[Eric Wieser]

(assuming you think splitting the thread makes sense)

[Eric Wieser]

Yaël Dillies said:

I want to destroy those type synonym instances files, so I don't want another one to pop up.

ulift isn't a type synonym :upside_down:

[Yaël Dillies]

Got me there!

[Yaël Dillies]

:open_mouth: I moved other people's messages as well? Where is this unexpected strength coming from?

[Eric Wieser]

You can move everyone below yours, just not piecewise. I've moved the stragglers back

[Yaël Dillies]

I've thought about how to organize order. in subfolders, but no trend emerges to my eyes yet.

[Eric Wieser]

Yaël Dillies said:

In particular, the order folder is very flat, so there's little opportunity to have several .ulift files, as we do under algebra. (algebra.group.pi, algebra.order.pi)

Ah, perhaps I wasn't clear. I think we should treat ulift the same way we already treat pi and prod; that is, if we have a separate prod file then make a separate ulift file, and if the prod instance is inline in another file, then put the ulift instance next to it.

[Eric Wieser]

I think docs#pi.preorder is inlined in a larger file, so the ulift one should be too.

[Yaël Dillies]

So no order.ulift file

[Yaël Dillies]

That sounds more reasonable already

[Eric Wieser]

Yes, only because there seems to be no precedent for that in order/

[Eric Wieser]

Yaël Dillies said:

I want to destroy those type synonym instances files, so I don't want another one to pop up.

But I don't think this is necessarily a good idea in general

[Yaël Dillies]

@Scott Morrison had to tweak the import tree elsewhere because of algebra.punit_instances

[Yaël Dillies]

This to me is already a sign that we should move away from those files.

[Eric Wieser]

Yaël Dillies said:

Classes can be defined arbitrarily low in the instance hierarchy, and all the prod/pi files have to decide of an arbitrary cutting point.

The whole game of the import graph is to decide arbitrary cutting points, you have to cut the entire DAG into smaller DAGs and then put them in some topological order.

[Eric Wieser]

punit_instances is bad; it doesn't follow the pattern of pi and prod

[Yaël Dillies]

Ah, so you would prescribe splitting it up into algebra.group.punit and others?

[Yaël Dillies]

(also, this thread belongs in #general but I didn't manage to move it there)

[Anne Baanen]

I think the pattern of splitting algebra.punit_instances into algebra.group.punit, algebra.gcd_monoid.punit, etc. is generally a good idea, although I'm not so convinced by the argument of "we should follow the established pattern". For me the most important rule of thumb for organizing declarations over files is that the imports of a file should not be too much bigger than the dependencies of any declaration in that file. This way, if a declaration is logically accessible at a low point in the declaration hierarchy, it can also be imported at a low point in the import hierarchy. We don't get artificial cyclic dependencies and we don't need to recompile many intermediate files to modify two declarations in sync.

In particular, the definition of docs#punit.comm_group depends only on punit and comm_group; punit is defined in core and comm_group in algebra.group.defs so the imports for the file that punit.comm_group is defined in should not be much more than algebra.group.defs itself.

For the question of whether to name the file containing this declaration something like algebra.group.punit or something like data.punit.group, I agree that the most important quality is the ability to find it easily, so precedent would guide us towards algebra.group.punit.

[Anne Baanen]

(Of course the real solution is to do away with this outdated notion of files altogether and just have a database of content-addressable declarations.)

[Kyle Miller]

I've seen a software project that kept numbered files, each importing the last, and you just inserted things where they were supposed to be. (I suppose that's not so different from metamath's set.mm if you think about how that gigantic file is ultimately stored across multiple blocks in physical storage)

[Reid Barton]

Maybe the comm_group punit instance can go with the definition of comm_group?

[Eric Wieser]

although I'm not so convinced by the argument of "we should follow the established pattern"

If we don't do this, then every few months we establish a different pattern and things become worse

[Yaël Dillies]

Yes Reid, that's what I'm arguing for.

[Eric Wieser]

If we don't like the established pattern, we should change it globally, rather than establishing a parallel pattern (edit: https://xkcd.com/927/)

[Reid Barton]

I mean literally after it in the same file, not in a new file algebra.group.punit

[Eric Wieser]

The same argument goes for prod and pi too, right?

[Reid Barton]

Yes, I assume so

[Eric Wieser]

algebra/group/defs is 800 lines long; what do we gain by adding these 170 lines to it?

[Eric Wieser]

Isn't the whole point of a defs file to contain just the defs, and not actually any instances?

[Yaël Dillies]

It can be in algebra.group.basic, sure.