Yves Bertot (May 14 2020 at 15:14): Yves Bertot (May 14 2020 at 15:14):Hello, I just spent a few hours porting the fsets library to coq-8.11. While doing so, I also tried to suppress warnings. In particular there are a log of warnings at the time a module is imported where the system complains that one is trying to mask existing names. I don't know how to fix this problem. Does somebody have a quick hint on how to do this?
Yves Bertot (May 14 2020 at 15:16):The code is visible at https://github.com/ybertot/fsets/tree/port-to-8.11
Gaëtan Gilbert (May 14 2020 at 15:29):How's this different from the fsets in the stdlib?
Yves Bertot (May 14 2020 at 16:54):I should have seen them, I can't remember how I missed them. Thanks.
Maxime Dénès (May 14 2020 at 16:55):Why do we keep a copy in coq-contribs, if they are included in the standard library?
Yves Bertot (May 14 2020 at 17:00):At first glance, it seems there is more in the coq-contrib, like red-black trees. I will have to look deeper.
Karl Palmskog (May 14 2020 at 17:05):I always use MSet instead of FSet from stdlib. Red-black trees are available for MSet in particular.
Karl Palmskog (May 14 2020 at 17:06):however, FMap, which shares code with FSet, was never modernized like MSet was, and so FMap lacks red-black trees
Yves Bertot (May 14 2020 at 17:06):@Karl Palmskog Do you have an example of using MSet that you can point me to?
Karl Palmskog (May 14 2020 at 17:08):@Yves Bertot this one is our most recent: https://github.com/palmskog/chip/blob/master/core/dfs_set.v#L113
Karl Palmskog (May 14 2020 at 17:09):the use case is described in our TACAS paper, p. 11: http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf
Yves Bertot (May 14 2020 at 17:10):Great, this turns into an interesting discussion about finite sets and maps. I will rename the topic.
Karl Palmskog (May 14 2020 at 17:11):I have come to the conclusion that MathComp's sets and finite maps (via Cyril's finmap) are nearly always to be preferred for reasoning, but then I want to refine to executable code, and the functor-based ones from Filliatre and Appel (who did the red-black tree stuff) win out easily for OCaml execution
Yves Bertot (May 14 2020 at 17:13):When you mention FMap, it seems this name appears only three comment lines in the Coq sources. Are using something taken from CompCert when you wish to use FMaps?
Karl Palmskog (May 14 2020 at 17:14):@Yves Bertot here is a file where I use FMapInterface.S as an example: https://github.com/palmskog/fitch/blob/master/coq/fitch_metatheory.v (checked with Coq 8.11)
Karl Palmskog (May 14 2020 at 17:15):see here for the top-level interface with FMaps: https://github.com/palmskog/fitch/blob/master/coq/dyadic_ordered.v#L151
Yves Bertot (May 14 2020 at 17:21):Thanks a lot for the pointers.
Karl Palmskog (May 14 2020 at 17:22):interestingly, I believe the particularly efficient finite map from binary Z that we use for implementing distributed key-value stores in Verdi was first implemented (or at least used) in CompCert and then moved to the stdlib (FMapPositive), here is some code using this: https://github.com/uwplse/verdi/blob/master/lib/FMapVeryWeak.v
if I recall correctly it was extensively benchmarked when they developed Verdi against FMapAVL etc.
Bas Spitters (May 14 2020 at 17:32):There are a couple of implementations here too:
https://gitlab.mpi-sws.org/iris/stdpp/-/tree/master/theories
Nice topic for stdlib2...
Bas Spitters (May 14 2020 at 17:33):And of course in math-classes:
https://github.com/coq-community/math-classes/blob/master/theory/finite_sets.v
Karl Palmskog (May 14 2020 at 17:49):as can be seen by various traces, Pierre Letouzey was at some point working on a modernization of FMap similar to MSet (e.g., https://lists.gforge.inria.fr/pipermail/coq-commits/2015-March/014564.html). I even recall seeing a separate GitHub repo with code related to "MMap", I think it was in the 8.6/8.7 cycle
Karl Palmskog (May 14 2020 at 17:49):ah, here it is, and he still seems to be working on it: https://github.com/letouzey/coq-mmaps/ -- however, no red-black tree based finite map in that repo
Karl Palmskog (May 14 2020 at 18:05):I did a comparison where I implemented the same quite complex mutually recursive function that uses finite maps in both Coq and HOL4 (https://github.com/palmskog/fitch). My experience is that using functor-based maps are terrible for reasoning about high-level properties in a nice way. In HOL4, they have super-abstract finite maps that are are near-automatically refined by CakeML to verified assembly. If one could set up a workflow using mathcomp-finmap and then refinement via, say, CoqEAL to FMap/MMap and then to extracted OCaml, that workflow would likely be comparable to the HOL4 one.
Bas Spitters (May 14 2020 at 18:35):There;s a parallel discussion on coqclub about this topic. I wonder whether there is technology to create that link.
Karl Palmskog (May 14 2020 at 18:38):ah, for efficiency there's also https://github.com/thtuerk/MSetsExtra (coq-msets-extra in OPAM) which optimizes a lot for specific cases
Karl Palmskog (May 14 2020 at 18:38):we can at least ping in @Gregory Malecha here
Paolo Giarrusso (May 20 2020 at 11:56):Nice about stdpp’s implementation is that they use typeclasses — Robbert tried at some point to extract them, with some success, but they’re not optimized for computing with them _in Coq_ at the moment
Paolo Giarrusso (May 20 2020 at 11:57):(I worked a bit on that, but more engineering remains to be done; there are discussions in Iris’s Mattermost and maybe on the bug tracker, I could dig them up if anybody is interested)
Last updated: Apr 18 2024 at 22:02 UTC