Zulip Chat Archive
Stream: mathlib4
Topic: Importing Data.String.Basic
Chris Hughes (Jan 06 2023 at 18:57):
Data.String.Basic is pretty difficult to port right now. The main dependency on this file is a has_repr
for multisets which uses the definition of le
as well as some difficult to prove properties of le
to show the repr
is well defined on the quotient. There are some other repr
s that depend on this as well. There are three solutions to this. We could move le
to Data.String.Defs
and make the repr instane a meta
instance, we could move the repr
s to seperate files or we could wait until Data.String.Basic
is ported before porting Data.Multiset.Sort
.
/poll What should we do?
Move has_repr instance into seperate files
Move le into string.defs and make the instances meta
Port Data.String.Basic before doing anything else
Something else
Arien Malec (Jan 06 2023 at 19:38):
Isn't this in the category of "everything interesting wants to be in Std anyway"?
Chris Hughes (Jan 06 2023 at 19:51):
I think definitions about strings are of interest to a lot of people and theorems about strings are of interest to almost no-one.
Arien Malec (Jan 06 2023 at 19:54):
I think proving core APIs are correct is good for API consumers generally but not for mathlib outside of, dunno, FSA etc.
Eric Wieser (Jan 06 2023 at 20:27):
Polls have to be all by themselves in a post
Henrik Böving (Jan 06 2023 at 20:32):
Chris Hughes said:
I think definitions about strings are of interest to a lot of people and theorems about strings are of interest to almost no-one.
I mean if we eventually end up writing parser libraries or something with formal guarantees theorems of strings could end up being very interesting I guess.
Heather Macbeth (Jan 06 2023 at 20:34):
I think we should take Chris' first option: move multiset.has_repr
out of data.multiset.sort
into a new file data.multiset.string
(or similar). There's no need to block the mathematical development of multisets on the theory of strings.
Eric Wieser (Jan 06 2023 at 20:39):
Can we do something even easier, which is just comment out the declaration with a porting comment?
Eric Wieser (Jan 06 2023 at 20:43):
One other thing to note; the current has_repr
instance is actually pretty stupid:
import data.multiset.sort
#eval ({1, 2, 11, 12} : multiset nat) -- {1, 11, 12, 2}
I would claim that no one wants to see the elements in that order
Chris Hughes (Jan 06 2023 at 20:46):
It mucks up the output of Port status if we don't port it.
Eric Wieser (Jan 06 2023 at 20:47):
How so?
Eric Wieser (Jan 06 2023 at 20:48):
#port-status is only an approximation; the final pass of "did we really port everything" is going to come from asking mathport to look for unaligned declarations
Chris Hughes (Jan 06 2023 at 20:49):
Well won't it only show the files that have all of their dependencies on mathlib3 ported, so if we never port Data.String.Basic
all of its dependencies won't show unless we change mathlib3.
Eric Wieser (Jan 06 2023 at 20:50):
Are you sure it cares about transitive dependencies and not direct dependencies?
Heather Macbeth (Jan 06 2023 at 20:51):
I think it only cares about direct dependencies, we've encountered this before.
Eric Wieser (Jan 06 2023 at 20:51):
Because if it's the former, there are only two such files to worry about, and you are already aware of the mathematically interesting one
Chris Hughes (Jan 06 2023 at 20:55):
What are the two sectioms for "all dependencies" and "immediate dependencies" then?
Eric Wieser (Jan 06 2023 at 21:01):
It sounds like the effect of not porting Data.String.Basic
will be that the finiteness files end up in the second heading
Eric Wieser (Jan 06 2023 at 21:01):
I don't think that's a problem
Mario Carneiro (Jan 07 2023 at 00:28):
Wait, why is Data.String.Basic
being considered for not-porting? Even if everything in it is moved to std or noaligned or whatever, the file itself should still be ported and marked as such even if it's basically empty
Chris Hughes (Jan 07 2023 at 00:34):
Because it's really hard to prove the theorems
Chris Hughes (Jan 07 2023 at 00:35):
It's not for not porting, just low priority, and it will be blocking a lot of progress pretty soon.
Mario Carneiro (Jan 07 2023 at 00:37):
If there are practical definitions that depend on theorems that we aren't interested in proving at the moment (but which we expect to be true), you can work around this by using an opaque
to define the function without proving the theorem
Mario Carneiro (Jan 07 2023 at 00:40):
I think we also need a way to say "this is an ad-hoc port but pretend it is ported anyway for the purpose of later files" to the port-status bot. This is what we already do for files in Tactic.*
and lean 3 core files but we might need it for selected files outside those areas as well
Mario Carneiro (Jan 07 2023 at 00:41):
that way we could just ad-hoc port the file and then update the bot so that later files are unblocked
Last updated: Dec 20 2023 at 11:08 UTC