search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move project Coqtail to coq-community #119

Closed jmadiot closed 3 years ago

jmadiot commented 3 years ago

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, Amaury Pouly

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

jmadiot commented 3 years ago

Note that https://github.com/coqtail/coqtail/ is the original repository and contains more than Coq files, so I moved the files of the "src" subdirectory to the repository https://github.com/jmadiot/coqtail (keeping the git history), which is the one I am proposing to move to coq-community. I also cleaned up a little. As recommended we will discourage pushing new commits to (the src part of) the original repository.

spitters commented 3 years ago

@jmadiot This library contains some nice results. What is the goal with this library? Do you want it to be a historical archive, or would it make sense to try to integrate with the coq stdlib, or math-comp analysis?

palmskog commented 3 years ago

@jmadiot this all sounds great, but some minor questions:

  1. Normally, we would want there to be a canonical location for all releases (e.g., Git tags), both historical and new ones, of a project. Should this location be the "new" repo or the one at: https://github.com/coqtail/coqtail
  2. Coqtail is not currently compatible with Coq 8.12 - do you have an intuition for how difficult it would be to fix this?
liyishuai commented 3 years ago

Reminds me of another nice project named Coqtail: https://github.com/whonore/Coqtail. Maybe worth adding a line in README to distinguish, after transferring the repository.

palmskog commented 3 years ago

What is the goal with this library? Do you want it to be a historical archive, or would it make sense to try to integrate with the coq stdlib, or math-comp analysis?

This is a good general question for coq-community maintainers to ask themselves, but to be extra clear, it's not a requirement for projects here to have a specific high-level goal (other than the more operational ones of keeping up-to-date with Coq releases, and facilitating reuse by the community).

jmadiot commented 3 years ago

@jmadiot This library contains some nice results. What is the goal with this library? Do you want it to be a historical archive, or would it make sense to try to integrate with the coq stdlib, or math-comp analysis?

@spitters Mainly archive for now, I guess? But if someone thinks it is useful to integrate some of the results in another library or stdlib, that can definitely be done --I think the other authors would agree-- and I'm happy to help/do it.

  1. Normally, we would want there to be a canonical location for all releases (e.g., Git tags), both historical and new ones, of a project. Should this location be the "new" repo or the one at: https://github.com/coqtail/coqtail

@palmskog It should be https://github.com/coqtail/coqtail. The new one was only to clean up what was not supposed to go in coq-community (e.g. papers, website, etc.), and should be temporary.

  1. Coqtail is not currently compatible with Coq 8.12 - do you have an intuition for how difficult it would be to fix this?

Ah, yes, I have no idea, but it was easy for previous versions, so I guess it should be easy for this one. I'm on it. (EDIT : I'm done, and it was indeed easy.)

Reminds me of another nice project named Coqtail: https://github.com/whonore/Coqtail. Maybe worth adding a line in README to distinguish, after transferring the repository.

@liyishuai True, thanks, I'll add it.

palmskog commented 3 years ago

@jmadiot since you are already a member of the coq-community organization, feel free to transfer the repo when you think it's ready. We can open repo issues about to-do items, such as 8.12 support, when the transfer is done.

Zimmi48 commented 3 years ago

Reminds me of another nice project named Coqtail: https://github.com/whonore/Coqtail.

What is even more strange in this accidental homonymy, is that both Coqtail projects (the library and the Vim plugin) are the successors of projects named Coquille!

It worries me that the Vim plugin might be more well-known and that people might be mistaken about which of the two projects has been moved to coq-community (and we can even imagine the other one being moved there as well at some undefined point in the future).

Therefore, what do you think of adding a suffix to the name of the repository to make it clear which one it is? There are several options like coqtail-theorems, coqtail-math, etc.

palmskog commented 3 years ago

Since the repository has been transferred and is now located at https://github.com/coq-community/coqtail-math, let's close this issue and continue any discussion as issues in that repository.