Proposal to move sudoku to coq-community

[siraben]

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): Laurent Théry @thery

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

[Zimmi48]

Thanks a lot for proposing to maintain this project.

I've fixed the "initial author field" (for coq-contribs, one should look to the description file which contains this info rather than the commit history).

There's nothing blocking adoption, so I'll proceed with the transfer and invite you to join coq-community.

[Zimmi48]

Once you accept the invitation, you should have write access to the repository.

One thing we usually do when we transfer former contribs is to transform the description file into a meta.yml file and to generate a few files (including the README) using the community templates. Feel free to ask for my help with this if you need it.

Something else that might be of interest to you since you are a Nix user is the coq-nix-toolbox. This is not stable yet nor properly documented, so expect some rough edges if you try it out but if you do, you can definitely ask for my help and @CohenCyril's. Integration with the community templates is a WIP.

[thery]

very good! @siraben I didn't know you updated the proofs (they needed it). I've also my local version. The only diff is some javascript files so that with js_ocaml we can generate a web page.

[Zimmi48]

Oh, I wasn't aware that you were maintaining your own version @thery. Sorry for proceeding to the transfer so fast. Would you have preferred if it was your version that was transferred to coq-community? If yes, it's still possible to change that.

BTW, do you have other "contribs" that you maintain on your side? If yes, we should archive them and redirect interested users to your versions.

[thery]

@Zimmi48 that's fine with me the proofs in coq-contribs where nicer thanks to @siraben. So transfering this version is best.

[Zimmi48]

Good to hear! Do you want to officially co-maintain this project?

[thery]

that's fine like it is

[siraben]

@thery I'd like to incorporate your changes to the repository, so far I cherry-picked the README change, but not sure about the rest. What would you like to be cherry-picked over?

[siraben]

Closed since move completed. TODO is to get it updated to use the template.

[Zimmi48]

@thery Maybe you can archive your version and point to the coq-community repository now. Let us know if at any point you want to officially co-maintain this project.

[palmskog]

While we are at it, I would also encourage @thery to upload his Sudoku project note to HAL for long-term preservation and canonical referencing, since keeping PDF documents in a repository is not the best idea.

[thery]

As said before my version is slightly different from the Coq community one since it contains a generation of an html with js_of_ocaml. If I have time this week, I will try to create a PR so I could archive my version.

[thery]

@Zimmi48 No problem to be co-maintainer

[thery]

@palmskog I will put the note in HAL asap

[thery]

I will put the note in HAL asap

done #4

[thery]

@Zimmi48 @palmskog the last merge put sudoku in sunc with my local version. Now I can archive my version. Just one question, what is the proper way to attach a project of the community to the CI?

[siraben]

I can add a Nix-build CI.

[thery]

@siraben cool! That would be nice

[palmskog]

@siraben our Nix CI configuration is highly specific to coq-community, so for maintainability, please use the approach recommended in the templates repository to generate the Nix GitHub Action.

[palmskog]

Solved by https://github.com/coq-community/sudoku/pull/6 - let's use issues in the sudoku repository for further discussion.