Jean-Marie Madiot (Aug 30 2020 at 09:32): Jean-Marie Madiot (Aug 30 2020 at 09:32):Karl Palmskog said:
Madiot's list is seemingly the most updated one of Wiedijk's 100 theorems for Coq, but even it references quite a lot of code that doesn't compile with modern Coq: https://madiot.fr/coq100/
That is presumably because sometimes I get updates from Freek, and occasionally I send him some as well. I can't make all code pointed by the page compilable with modern coq, but the files hosted on the repo do compile with coq 8.12.0. I'm ok with moving the project to coq-community to make it a more centralized list, I'll reply to the issue.
Karl Palmskog (Aug 30 2020 at 09:40):@Jean-Marie Madiot sounds great. One property we might add to the entries in the list is "last version of Coq known to work". For example, many of the links are contribs or hosted in coq-community, so this is easy to add for them (for coq-community, it could even be automated, since it's stored in metadata).
Jean-Marie Madiot (Aug 30 2020 at 09:42):Karl Palmskog said:
this has quite a lot of undergraduate math: https://github.com/coqtail/coqtail/ - there was an issue some time ago about coq-community there: https://github.com/coqtail/coqtail/issues/1
In there, there are results on arithmetic, on reals numbers, on complex numbers ... but also a lot of things that would probably need to be thrown away. Does it need to be reasonably clean before moving to coq-community?
Karl Palmskog (Aug 30 2020 at 09:45):@Jean-Marie Madiot not really, the only thing we (nominally) require is that it works with Coq master. If cleaning is needed, this is a good thing to put as an issue with "help wanted" tag, so the community knows how to pitch in.
Karl Palmskog (Aug 30 2020 at 09:47):Let's just say we have projects in the whole range of "messy" to "pristine". Quality and order is a nice long-term goal, but in the short-term I would settle for projects being easily available to the wider Coq community for latest Coq.
Jean-Marie Madiot (Aug 30 2020 at 10:34):I need to ask several questions before transferring, regarding e.g. licencing for the list of theorems (since it contains files and code excerpts), should I ask them here? Or in the issue on the original repo? Or should I make the proposal issue now and then discuss in that issue?
Karl Palmskog (Aug 30 2020 at 10:36):@Jean-Marie Madiot if you create an issue in the coq-community manifesto repo, that is a good place for licensing questions
Karl Palmskog (Aug 30 2020 at 10:39):coq-community members also hang around here and in the coq-community stream for more casual questions
Jean-Marie Madiot (Aug 31 2020 at 19:38):coq100 is probably not the best name. Maybe coq-100-theorems is better? Suggestions are welcome.
Karl Palmskog (Aug 31 2020 at 19:40):I think "Coq 100" is fine for now, maybe you can create a naming issue in the repo and someone might come up with something.
Karl Palmskog (Aug 31 2020 at 19:41):by the way @Jean-Marie Madiot do you mind if I do a PR with the usual _CoqProjectto the PR to keep ProofGeneral/CoqIDE happy?
Jean-Marie Madiot (Aug 31 2020 at 19:43):Karl Palmskog said:
by the way Jean-Marie Madiot do you mind if I do a PR with the usual
_CoqProjectto the PR to keep ProofGeneral/CoqIDE happy?
not at all, go ahead!
Karl Palmskog (Aug 31 2020 at 19:43):we also have a standard build boilerplate using coq_makefile
Karl Palmskog (Aug 31 2020 at 19:47):ah, we have a dependency on Coquelicot
Karl Palmskog (Aug 31 2020 at 19:48):I'll do a separate PR with some CI for that
Jean-Marie Madiot (Aug 31 2020 at 19:49):ah, yes. The dependencies are mentioned in the file, that's kind of a shame since all the others are standalone. Maybe it would make more sense inside Coquelicot?
Karl Palmskog (Aug 31 2020 at 19:49):indeed it might, but a question for another day/issue.
Jean-Marie Madiot (Aug 31 2020 at 20:04):regarding coqtail, only (and only parts of) the directory src would make sense to be in coq-community, is that possible? Maybe by forking, trimming the fork, and then transferring the fork? Or some other way that would leave the other directories in the original repo/organization?
Karl Palmskog (Aug 31 2020 at 20:10):indeed it would be possible to only put some directories in coq-community, in a new repo or as a compressed version of the current repo. The reason we recommend (but don't require) transferring a repo is that it will make all project URLs on the web forward to the current maintained version.
Karl Palmskog (Aug 31 2020 at 20:12):if you want to leave the original repo intact, we strongly recommend marking it archived/read-only, and having a prominent link to the new repo
Karl Palmskog (Aug 31 2020 at 20:13):ideally, the editing history of the Coq files would also be preserved in the coq-community repo (but again not required)
Jean-Marie Madiot (Aug 31 2020 at 21:20):I think the best is to keep the original repo (with the aforementioned recommendations). Is is possible to _also_ keep the edit history in both? I'm thinking of forking coqtail to coq-community, but maybe that's not what forks are for
Karl Palmskog (Aug 31 2020 at 21:49):yes, you could take the repo history and put it into a new repo (clone), remove the non-applicable parts, and mark the old repo as readonly. This would be preferable to starting a new repo from scratch with a "dump commit".
Théo Zimmermann (Aug 31 2020 at 22:12):If you want to keep only the history for the sub repository, this is also something that can be done with some git subtree magic.
Jean-Marie Madiot (Sep 01 2020 at 14:28):@Théo Zimmermann is the same as:
git filter-branch --prune-empty --subdirectory-filter src master
?
Théo Zimmermann (Sep 01 2020 at 15:44):Possibly. I just know that these commands exist but do not know them by heart (I need to look for them when I need them).
Last updated: May 31 2023 at 04:01 UTC