Move set definitions to a new file #9737

Stream: PR reviews

[Yury G. Kudryashov]

In #9737 I move definitions like Set.preimage to a new file so that later we can change some imports from Set.Basic to Set.Defs. What names should I put in the header?

Also, we may want to merge this file with Init/Set later.

[Yury G. Kudryashov]

I'll fix the other issues together with adding the header to avoid another rebuild of the whole library.

[Yury G. Kudryashov]

It's ready for review now.

[Wrenna Robson]

Looks fine to me. Left a couple of comments. Try running leaff on it?

[Yury G. Kudryashov]

Where can I find instructions on running leaff?

[Alex J. Best]

The simplest way is to make a new branch and merge the leaff branch into it

[Alex J. Best]

The leaff branch being alexjbest/leaff, if you push this leaff will print the diff to the actions summary view (you don't need to open a PR for the new branch to see the output)

[Alex J. Best]

https://github.com/alexjbest/leaff?tab=readme-ov-file#usage is how to run it directly

[Yury G. Kudryashov]

Thank you! I'll try to run it directly, then use the "merge" trick if it fails.

[Yury G. Kudryashov]

I see lots of "type changed", most probably because I added notation class instances before the boolean algebra instance.

[Yury G. Kudryashov]

I'll make the same change on master, then compare.

[Yury G. Kudryashov]

A similar PR: #9750

[Yury G. Kudryashov]

What does

collision when hashing for [Trait.name, Trait.value], all bets are off HasCompl.recOn (HasCompl.casesOn, true)

mean?

[Yury G. Kudryashov]

It reports about 200 differences between a2fd24f606 and 7c0bd74547. Can it be because I changed Type u to Type* here and there?

[Alex J. Best]

Yury G. Kudryashov said:

What does

collision when hashing for [Trait.name, Trait.value], all bets are off HasCompl.recOn (HasCompl.casesOn, true)

mean?

This is not your fault, it basically means that HasCompl.recOn and HasCompl.casesOn have the same type exactly, but this shouldn't affect anything (I'll remove these warnings when I'm happy everything works)

[Alex J. Best]

Hmm I'm not sure about type u and type*, possibly that could be a difference. As I mentioned in my talk I'd like to differentiate a bit more between things that changed for technical reasons, and things that really are different

[Yury G. Kudryashov]

Also, what does "proof changed for Bot.bot" mean? Bot.bot is not a theorem.

[Alex J. Best]

It means the value of the def changed in that case (it is a todo to display this better)

[Yury G. Kudryashov]

I'll sync Type u vs Type* and see if there are any differences remain.

[Yury G. Kudryashov]

I tried to sync Type u vs Type* but it didn't help. Probably, Type* generates a semi-random name or id and it's different in 2 branches.

[Yury G. Kudryashov]

Is there any way to actually inspect the differences?

[Yury G. Kudryashov]

So, I suggest that we aren't waiting for a clean leaff output in #9737 and #9750

[Wrenna Robson]

I agree, but I suggested running it because it should catch any major issues like dropped theorems, I think?

[Alex J. Best]

Yury G. Kudryashov said:

Is there any way to actually inspect the differences?

Not yet, but this is planned too, and has been highly requested indeed.