instance for exact functor

Stream: mathlib4

[Nailin Guan]

I met the following situation:
forModuleCat.RestrictScalars we have it is left/right adjoint when the universe is of the form max _ _ one is the universe of the ring.
However, for only exactness, it is true for arbitrary universe, the problem here is that when trying to synthize Limits.PreservesFiniteLimits and Limits.PreservesFiniteColimits, it tried to synth adjoint first.
I want to stop it and use the instance I wrote, what should I do?

[Nailin Guan]

Currently I raised the priority of the instance I wrote to high, but it can't be a private instance any more.

[Nailin Guan]

This only appeared in the recent 300 commits, do anyone know what caused this? (This may hint a bad instance design)

[Yaël Dillies]

Naive suggestion: Can you bisect?

[Nailin Guan]

Sorry, what do you mean by bisect?

[Yaël Dillies]

You know that you get the problem commit on commit N, but not on commit N - 300. Do you get it on commit N - 150 ?

[Nailin Guan]

OK, let me try.

[Alfredo Moreira-Rosa]

Just in case, don't do it manually, there is a git tool for that. docs: https://git-scm.com/docs/git-bisect

[Nailin Guan]

I think I may got the problem wrong? It is somehow related to private instance? Is it different from the old one in module system? But it works on 12.18, very strange.

[Nailin Guan]

Alfredo Moreira-Rosa 說：

Just in case, don't do it manually, there is a git tool for that. docs: https://git-scm.com/docs/git-bisect

Sorry that I still not know how to use it, I'll try tomorrow. I currently tried to debug dircetly, but found nothing.

[Alfredo Moreira-Rosa]

If you are working directly on mathlib, you need to start by doing (on a terminal, command line):

git bisect start
git bisect bad
git bisect good <commit or tag where it was still good>

After that, git choose the middle commit between those.
You need to rebuild Mathlib (can take a lot of time) :

lake build

if build fails (because git choose a commit version that don't build, do :

git bisect skip
lake build

Then if build pass, test your feature. if your test still fails, do

git bisect bad

else

git bisect good

it will continue checking out a new commit.
repeat the process (rebuild mathlib, test, mark good or bad) until git tells you it found the culprit commit. (for 300 commits that's at most 8 times).
So it's not an easy process. Because you will need to rebuild mathlib.

[Aaron Liu]

Alfredo Moreira-Rosa said:

You need to rebuild Mathlib (can take a lot of time) :

lake build

Shouldn't lake exe cache get work for this?

[Aaron Liu]

if you don't want to wait hours for mathlib to build

[Alfredo Moreira-Rosa]

I'm not sure there exists a cache for each commit, but i may be wrong, never tried.

[Kevin Buzzard]

Sure there's a cache for each commit