math-comp / coq-combi Goto Github PK

I've recently installed MathComp but found myself unable to compile this due to breaking changes in MathComp. Anyone planning to rebase this? If not, I'll just downgrade my MathComp; but I'd rather know in advance if the issue will be moot in a week :)

https://github.com/hivert/Coq-Combi/blob/a335c43e7fe7bc90b7f13bf38a8e94f954349800/theories/Dendri/shufflealg.v#L82-L85

I guess that if you generalize this too, you could also capture bilinear forms (and possibly get a dot product by providing an appropriate f?)

By the way are you aware of this: math-comp/math-comp#207 ?

Thanks for the update! Installation has become really easy, to the point I can just "make" and run coqide and it works; I've been waiting for this for years.

The link to the doc in README.md is broken, though, as are many other links on your website. Some changes in the folder structure perhaps?

Also, I'd love to see some kind of "reading order" recommendation, telling me in what order to read the .v files to understand them. I know I could make a toposort of their dependencies (is there a one-line way to do that, by the way?), but a properly curated list could be better, particularly if it comes with brief explanations of what the files are doing. For example, looking at partition.v, I really have no clue what this here means:
Definition in_shape sh b := b.2 < nth 0 sh b.1.
Besides, there are probably specific chapters in the MCB book and files in the MathComp doc I should read beforehand.

ALEA is now a maintained project in coq-community. Please consider submitting extensions and changes to ALEA from here to that repo so that the community can benefit.