Jason Hu (Jul 08 2022 at 17:54): Jason Hu (Jul 08 2022 at 17:54):Hi,
I am looking for a data structure which is effectively a map, but its key is ordered, so we can do things like find_ge which finds a binding for the smallest key that is greater than or equal to the input, as well as find_le for the symmetric direction. The standard library does expose FMapFullAVL, but it seems does not expose the interface I want. is there any way I can get this data structure? It does not have to be in stdlib if other libraries provide it.
Karl Palmskog (Jul 08 2022 at 18:10):you may want to look at this: https://github.com/xavierleroy/coq-mmaps
Karl Palmskog (Jul 08 2022 at 18:11):the RBT version likely has the invariant you want, per https://www.cs.princeton.edu/~appel/papers/redblack.pdf
Karl Palmskog (Jul 08 2022 at 18:14):now if we only could get this PR merged and an opam package: https://github.com/letouzey/coq-mmaps/pull/2
Paolo Giarrusso (Jul 08 2022 at 23:46):Is the problem that Avl trees don't have that invariant, or they just don't expose it? I'd have expected the latter?
Paolo Giarrusso (Jul 08 2022 at 23:48):@Karl Palmskog is this a candidate for coq-community? Not that I have energy to contribute sadly :-|
Karl Palmskog (Jul 12 2022 at 13:06):@Paolo Giarrusso I would personally like coq-mmaps to join Coq-community. But we would need permission from Pierre Letouzey, who I think has not been active on GitHub for a while. You are welcome to propose adding coq-mmaps to Coq-community though and ping in Pierre (or even email him beforehand): https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package
The proposer of a package doesn't have to volunteer to be maintainer.
Théo Zimmermann (Jul 13 2022 at 10:35):Note that "we need permission" is a bit too strong. Our process is to ask permission from the original author and to proceed (e.g., with a fork) in case we don't hear back. That being said, it would be preferable to be able to transfer the repo instead of creating a fork, so I can also ask Pierre Letouzey (who is in my lab) directly (but probably after the summer).
Théo Zimmermann (Jul 13 2022 at 10:35):But there is not much point in doing this effort if we do not find a volunteer maintainer to start with.
Karl Palmskog (Jul 13 2022 at 11:46):I guess I could step in as an interim maintainer, since I would at least like to see this package have Xavier's changes and put it on opam. Then I will do the minimum to keep it compatible until someone takes over. But it all depends on what Pierre says (if he likes the idea)
Karl Palmskog (Jul 13 2022 at 11:47):I recently ported Andrew's RBT to CakeML, so I know the codebase
Alexander Gryzlov (Jul 13 2022 at 12:01):I've recently implemented a bunch of search tree structures with SSReflect here https://github.com/clayrat/fav-ssr
Karl Palmskog (Jul 13 2022 at 12:02):@Alexander Gryzlov any plans to package those in some way? Ideally, this would become part of some official MathComp project (cc: @Enrico Tassi )
Alexander Gryzlov (Jul 13 2022 at 12:04):Yeah I was planning to finish part 4 first, then propose some of the auxilliary theories (e.g. division with ceiling) for core mathcomp, and maybe the repo itself as some sort of mathcomp project
Alexander Gryzlov (Jul 13 2022 at 12:05):The only problem is that part 4 is the hardest one and the ratio of actual code to the stuff they describe in the book is much higher than in the other chapters :D
Karl Palmskog (Jul 13 2022 at 12:05):we already have https://github.com/thery/mathcomp-extra which is a bit similar, and also deserves more highlighting
Karl Palmskog (Jul 13 2022 at 12:06):it's definitely a cliche, but "perfect" or "complete" may sometimes be the enemy of good (enough to publish)
Alexander Gryzlov (Jul 13 2022 at 12:08):Yeah, I know of mathcomp-extra, I used its logarithm ceiling for this project for a while and then @Laurent Théry even upstreamed it to mathcomp core
Enrico Tassi (Jul 13 2022 at 12:51):@Karl Palmskog it is a bit unclear what you mean, or better I don't know what "official MC project" is. For example we are moving (with your help) some projects to coq-community. If you mean "being integrated in the main MC repo" then the thing is about maintenance and the code quality is going to be examined carefully. (and I agree totally with "perfect is enemy of good")
Karl Palmskog (Jul 13 2022 at 12:53):@Enrico Tassi well, this was just me checking in what you think the process should be. If indeed you think Coq-community should be the home for MathComp-related projects by default, then that's great, and we can just ask Alexander to follow the process here when ready.
But to me, "official" MathComp has meant the project being part of the math-comp GitHub org.
Enrico Tassi (Jul 13 2022 at 12:55):When we created that, coq-community was not even there, and we were kind of proposing the same "services", eg we test against you. Today we do that with nix, no matter where you place your project... Visibility is also different, you can opam search mathcomp, in the past you could not...
Enrico Tassi (Jul 13 2022 at 12:55):This is why we started moving some projects to coq-community
Karl Palmskog (Jul 13 2022 at 12:56):OK, sounds great to me. Then I guess the only "official" thing left will be the coq-math-comp- prefix in package names?
Enrico Tassi (Jul 13 2022 at 12:57):We can try to define this precisely. To me a user of MC shall not use that prefix. But a library which adds some theory to MC should, even if it is not hosted in MC/
Enrico Tassi (Jul 13 2022 at 12:58):Example: if you add a structure to the hierarchy (today hard, starting from MC 2.0 easier) or provide instances of general interest, then the prefix makes sense to me
Enrico Tassi (Jul 13 2022 at 12:59):If you follow similar style
Enrico Tassi (Jul 13 2022 at 12:59):if it would make sense to merge your library in MC, eventually...
Enrico Tassi (Jul 13 2022 at 12:59):We don't have that written up, this is what looks reasonable to me (on the top of my head)
Enrico Tassi (Jul 13 2022 at 13:01):clearly a thing called "mathcomp-extra" has that trajectory in mind
Laurent Théry (Jul 13 2022 at 13:20):@Alexander Gryzlov didn't know your work. Great!!. If you need some manpower to progress in chapter 4, don't hesitate to ask.
Théo Zimmermann (Jul 13 2022 at 14:50):If people need not permission from the math comp team to get the math comp prefix, this should indeed be documented. And if they need it but there is a process to apply, it should be documented as well :wink:
Karl Palmskog (Jul 13 2022 at 16:36):somewhat counterintuitively, the rules around the coq-math-comp- prefix should probably be documented in the Coq opam archive, and be enforced by opam archive maintainers
Matthieu Sozeau (Jul 22 2022 at 10:29):Re the invariant on stdlib’s fmaps/fsets, I think there is an additional functor in the stdlib that shows that folding over a set/map is order-preserving (assuming the keys are ordered) so you could implement it I think
Last updated: Oct 13 2024 at 01:02 UTC