## Stream: math-comp users

### Topic: topological sorting in mathcomp

#### Evgeniy Moiseenko (Oct 21 2021 at 19:33):

Hi folks.
In my project, I need a lemma stating that any finite partial order can be extended to a total order, which boils down to the topological sorting of a finite graph. I was hoping to find a ready-to-go solution, preferably in mathcomp-style.
I was looking for the required lemma in `ssreflect/fingraph.v` https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fingraph.v but haven't found it.
I was also searching in graph-theory library https://github.com/coq-community/graph-theory, also unsuccessfully.
But perhaps I just overlooked it? Topological sorting seems to be quite a basic thing, so expect someone already did it in Coq/mathcomp.

#### Karl Palmskog (Oct 21 2021 at 19:39):

there are a couple of implementations of topological sorting out there, originally by Cyril Cohen and Laurent Théry. I have adapted their solutions a bit for my purposes of analyzing dependency graphs in code that is extractable to OCaml. See here, in particular `topos.v` (proofs of topological sorting) and `kosaraju.v` (topological sorting function `tseq`): https://github.com/palmskog/chip/blob/master/core

This is the original development I adapted: https://github.com/CohenCyril/tarjan

This is Cyril and Laurent's paper on the general graph algorithm formalizations of which topological sorting is one part: http://drops.dagstuhl.de/opus/volltexte/2019/11068/pdf/LIPIcs-ITP-2019-13.pdf
This is the paper I co-authored on dependency graph analysis where we used parts of Cyril & Laurent's work: https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7_9.pdf
Laurent's tech report on the original formalization of Kosaraju's algorithm, which uses topological sorting: http://www-sop.inria.fr/marelle/Laurent.Thery/Kosaraju/Kosaraju.pdf

I guess the main drawback is that this code is currently for MathComp 1.7, so would need some porting to recent MathComp (both Cyril's tarjan repo and my repo)

#### Evgeniy Moiseenko (Oct 21 2021 at 19:48):

Thank you, looks very useful indeed.
The restriction on version 1.7 of math comp is a bit problematic, since I currently use some features from the dev version.

#### Karl Palmskog (Oct 21 2021 at 19:49):

well, I could take a look at in the near future to port my repo if you can confirm it has what you need

#### Karl Palmskog (Oct 21 2021 at 19:58):

ah, for completeness I should mention also a quite different non-MathComp topological sorting implementation (using the stdpp library), could likely be adapted to MathComp quite easily: https://github.com/runtimeverification/casper-cbc-proofs/blob/master/Lib/TopSort.v

#### Evgeniy Moiseenko (Oct 21 2021 at 20:01):

Karl Palmskog said:

well, I could take a look at in the near future to port my repo if you can confirm it has what you need

I am studying the source code.
I guess this is the lemma I need?
https://github.com/palmskog/chip/blob/072de78e61de5ed8a5891da5db3f9e267d063a0b/core/kosaraju.v#L348

I wonder why there is no precondition on graph/relation `r` being acyclic? (or I just don't see it)

#### Karl Palmskog (Oct 21 2021 at 20:02):

@Evgeniy Moiseenko this is what Laurent didn't have and which I added, you have two variations here:

#### Evgeniy Moiseenko (Oct 21 2021 at 20:04):

Oh, I see, very cool, thank you

#### Karl Palmskog (Oct 21 2021 at 20:04):

it turns out that the correctness of Kosaraju for strong connectedness needs topological sorting, but does not use the acyclicity. We needed acyclicity.

#### Karl Palmskog (Oct 21 2021 at 20:08):

if you think you can reuse `kosaraju.v`/`acyclic.v`/`topos.v`, please open an issue about the port to mathcomp-dev and we can take it from there: https://github.com/palmskog/chip/issues

[Quoting…]
done

#### Evgeniy Moiseenko (Oct 21 2021 at 20:20):

would you expect it to be hard to update chip to latest mathcomp?
I can have a try by myself in coming days. In case there would be no significant problems I can just do it by myself.

#### Karl Palmskog (Oct 21 2021 at 20:22):

quite a lot has happened over the last few years in terms of lemmas changing name and so on. It shouldn't take too much work, and I might have time this weekend, but you can also jump into the port yourself if you want (then please fork and submit a pull request if you succeed)

Note that you need both `coq-mathcomp-ssreflect` and `coq-mathcomp-fingroup` at least.

I would then also recommend looking at the dependencies between files and ignore everything that doesn't have anything to do with `topos.v` (remove from `_CoqProject`)

#### Evgeniy Moiseenko (Oct 21 2021 at 20:32):

Karl Palmskog said:

I would then also recommend looking at the dependencies between files and ignore everything that doesn't have anything to do with `topos.v` (remove from `_CoqProject`)

I was hoping to get a working version of the whole library and then just add it to my opam as a dependency :sweat_smile:

#### Karl Palmskog (Oct 21 2021 at 20:33):

ah OK, I see. But why I think we should port those files first is because I copied other files from other places, and they have been maintained upstream, so one might copy them over again from there.

ok, I see :)

#### Karl Palmskog (Oct 21 2021 at 20:35):

it's not clear that the best thing here is to put out a conglomeration of files not-all-so-related to graphs as an opam package. Ideally we would put together a graph algorithms package which also includes Tarjan's algorithm with the work by Cyril and Laurent.

#### Evgeniy Moiseenko (Oct 21 2021 at 20:38):

Maybe then promote some graph theory to `fingraph.v`? I think topological sorting at least would be very useful.

#### Karl Palmskog (Oct 21 2021 at 20:38):

this could take more time and a bit of communication, so that's why it may be a good idea to vendor the topsort files you need (put them in your repo) when they are first ported to mathcomp-dev, and then switch to using the imagined graph-algorithms package via opam later

#### Evgeniy Moiseenko (Oct 21 2021 at 20:39):

ok, I see, thank you. I'll have a look.

#### Karl Palmskog (Oct 21 2021 at 20:39):

the standards for getting code into the mathcomp repo alongside `fingraph.v` are super strict. If one creates a `coq-graph-algorithms` package/project, then eventually parts of that repository may be accepted into MathComp proper

#### Evgeniy Moiseenko (Oct 21 2021 at 20:41):

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).
That is why I am proposing to update `chip`, or move to `ssreflect`, etc

#### Karl Palmskog (Oct 21 2021 at 20:42):

yes, we are trying to coordinate those kinds of projects, where people set up new repos with code to maintain to not have divergence, in coq-community: https://github.com/coq-community/manifesto/

#### Karl Palmskog (Oct 21 2021 at 20:43):

in the short term though, it's probably hard to avoid some vendoring

#### Evgeniy Moiseenko (Oct 21 2021 at 20:43):

Ok, hypothetical `coq-graph-algorithms` package looks like the best solution to me.
But as a first step, I would try to just fork `chip` and fix things in-place.

#### Evgeniy Moiseenko (Oct 21 2021 at 20:45):

Also, there is https://github.com/coq-community/graph-theory
Looks like it also overlaps with the theme of graph algorithms
Are you familiar with that library?

#### Karl Palmskog (Oct 21 2021 at 20:46):

yes, the maintainer said he prefers not to have algorithms like what is in chip and the tarjan repo in that project

ok, I see

#### Karl Palmskog (Oct 21 2021 at 20:47):

it also has different notions/definitions of graphs than `fingraph.v` (although I guess they are convertible)

#### Paolo Giarrusso (Oct 21 2021 at 21:24):

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).

And clear attribution/copyright notices (maybe a separate folder) should address this concern, and you probably need that to fulfill licensing requirements :-)

#### Evgeniy Moiseenko (Oct 22 2021 at 07:49):

Paolo Giarrusso said:

I am a bit uncomfortable with copying other people code to my repo (because in my opinion, it blurs the contributions of the community).

And clear attribution/copyright notices (maybe a separate folder) should address this concern, and you probably need that to fulfill licensing requirements :-)

Yes, for sure I would put license and credentials, but still ))

#### Karl Palmskog (Oct 22 2021 at 08:06):

maybe @Cyril Cohen could move this topic to the MathComp stream - and also possibly comment on what he thinks about consolidating MathComp graph algorithm results into some GitHub repo, for example his `tarjan` repo (or other repo where we adopt the `tarjan` code)

#### Notification Bot (Oct 22 2021 at 08:23):

This topic was moved here from #Coq users > topological sorting in mathcomp by Cyril Cohen

#### Cyril Cohen (Oct 22 2021 at 08:38):

I'm in favor of submitting PRs to mathcomp whenever some stuff are used by more than one user. We can converge by discussing in PR threads.

#### Karl Palmskog (Oct 22 2021 at 10:48):

OK, I'm reading this as that we could submit the topological sorting + lemmas about it as PR to MathComp proper. Will think about this when we get things ported to MathComp `master`.

#### Karl Palmskog (Oct 23 2021 at 13:48):

I ported my repo to MathComp master (compatibility with 1.12): https://github.com/palmskog/chip

With Laurent's encouragement I will also revive my old PR to the tarjan repo with changes to topological sorting and acyclicity from chip: https://github.com/CohenCyril/tarjan/pull/10

If this PR is merged, I will probably change chip to depend on the tarjan repo/package.

#### Karl Palmskog (Oct 24 2021 at 14:01):

PR was revived now: https://github.com/CohenCyril/tarjan/pull/10

#### Evgeniy Moiseenko (Oct 25 2021 at 09:06):

@Karl Palmskog awesome, thank you so much

#### Karl Palmskog (Oct 27 2021 at 16:19):

many thanks to Laurent who did great proof script improvements in my PR branch! I try to learn better MC/SSR style over time, and this is great for that. I didn't catch up to the `boolP` predicate until now.

#### Evgeniy Moiseenko (Oct 28 2021 at 13:24):

@Karl Palmskog thank you for your contributions!
Should I now use `chip` as my opam dependency?
Or should I use `tarjan` repo after your PR will be merged?
`tarjan` currently has no opam package, but I could PR basic `.opam` file for the library, if the contributors are okay with that.

#### Karl Palmskog (Oct 28 2021 at 14:11):

Cyril just did a PR against my PR about an hour ago, he has a much more math-compy way of handling acyclicity that I think looks good, I will review and merge his PR soon. Probably you should depend on `tarjan` after my PR + Cyril's improvements are merged

#### Cyril Cohen (Oct 28 2021 at 15:27):

I think the next steps to do are actually

1. review and merge PR CohenCyril/tarjan#10
2. move the repo to the `math-comp` organization
3. move all `.v` files to `theories` directory
4. add a `meta.yml` package (and generate metadata from it)
5. publish an opam package and a nix package (note that it suffices to add this file to https://github.com/nixos/nixpkgs.
6. backport the stuff to mathcomp `master`

#### Karl Palmskog (Oct 28 2021 at 15:46):

@Cyril Cohen can/should I generate a basic `meta.yml` and do a PR with that? Or I guess we wait until after the move, OK.

#### Cyril Cohen (Oct 28 2021 at 17:27):

Step 2. is done and Step 3. is math-comp/tarjan#13 and merged
@Karl Palmskog you could prepare step 4. in parallel

#### Karl Palmskog (Oct 28 2021 at 17:43):

OK, working on the `meta.yml` file now, should be done in the next hour

#### Karl Palmskog (Oct 28 2021 at 17:46):

@Cyril Cohen is the MIT license OK, or do your prefer some CECILL one?

#### Karl Palmskog (Oct 28 2021 at 22:42):

OK, the MathComp Tarjan and Kosaraju opam package, version 1.0.0, is now out in the Coq opam archive:

``````opam install coq-mathcomp-tarjan
``````

It has definitions of graph acyclicity and verified topological sorting, as well as variants of strongly connected components algorithms.

#### Evgeniy Moiseenko (Oct 29 2021 at 08:08):

Thank you so much to all people involved @Karl Palmskog @Cyril Cohen @Laurent Théry .
I want to say that mathcomp community is just awesome.

#### Karl Palmskog (Oct 30 2021 at 18:25):

just saw this other piece of graph algorithm formalization using `fingraph`, flavor feels familiar to the Kosaraju formalization: https://github.com/fetburner/coq-dijkstra

Last updated: Jul 25 2024 at 16:02 UTC