Stream: math-comp users

Topic: FreeModules


view this post on Zulip Daniel Kirk (Jan 05 2021 at 14:43):

Hi all, hope everyone had a relaxing Christmas and new year's break.
I'm releasing a functional iteration of my implementation of free-left-modules, bases (both finite and infinite) and (finite) direct sums of modules extending Mathcomp's lmodType.
https://github.com/Modularius/MathcompFreeModules
It currently compiles and works however I'm hoping someone with more knowledge can help explain why I'm getting warnings for several of the canonical declarations claiming they are redundant. I'm not at all sure why this happens or what it means, I'm still learning the particulars of canonical structures.

view this post on Zulip Daniel Kirk (Jan 05 2021 at 14:44):

There are commented notes in the .v files that should give a good overview of what the files do. I'd be very grateful to anyone who tries them out.

view this post on Zulip Karl Palmskog (Jan 05 2021 at 14:54):

you probably want to specify which MathComp version you're compatible with and add some continuous integration to check that. See here for boilerplate/examples:

In particular, *.conf files should not be under version control.

view this post on Zulip Daniel Kirk (Jan 05 2021 at 19:15):

Thanks! I used version 1.11, I've not upgraded to 1.12 yet.


Last updated: Feb 08 2023 at 04:04 UTC