feat: warn on local changes to dependency & related fixes

[tydeu]

Closes leanprover/lake#167.

[Kha]

Nice!

[Kha]

Now that I took a closer look at the code, I'm interested: what's with the inline/noinline changes? Surely hasNoDiff can't be a hot function?

[tydeu]

@Kha

Now that I took a closer look at the code, I'm interested: what's with the inline/noinline changes?

This is an unrelated tweak. I have noticed the new compiler (trace.Compiler.result) often inlines constant definitions (which will result in them being duplicated across multiple files), so I have gotten into the habit of ensuring that constant definitions are tagged noinline to avoid this (when the new compiler is activated). Is that right or have I misunderstood something?

A similar problem also occurs in the old compiler for abbrev constant definitions. For example, a constant SyntaxNodeKind like identKind in a definition will be inlined and then be extracted as a new closed term, meaning the `ident constant gets duplicated across all uses rather than just using the one in core. Thus, they should instead be @[noinline, reducible] def instead of abbrev.

Actually, I think I might go test a bench of that core change to see if my assumptions on savings are true.

[Kha]

I have noticed the new compiler (trace.Compiler.result) often inlines constant definitions (which will result in them being duplicated across multiple files), so I have gotten into the habit of ensuring that constant definitions are tagged noinline to avoid this (when the new compiler is activated).

I don't understand, is the new compiler becoming a compile-time bottleneck due to this? We should not optimize our code for run time under a compiler that's not even in use yet.

[tydeu]

@Kha It makes no difference practically because the old compiler does not inline these definitions either way, but @[noinline] does ensure this behavior remains constant. However, if you think this is bad style, I am happy to avoid it in the future.

[Kha]

I think so, yes. Optimizing for a future compiler seems like an especially egregious case of premature optimization to me.