Stream: coq-community devs & users

Topic: Example of MIT Licensed coq-community project


view this post on Zulip Yves Bertot (Jun 19 2020 at 07:14):

Hello, I would like to place one of my past projects under MIT licence, and I would like to mimic the templates used in coq-community. Is there an easy way to find which of coq-community projects are already using this license?

view this post on Zulip Anton Trunov (Jun 19 2020 at 07:56):

Hi @Yves Bertot , you can use GitHub's advanced search (https://github.com/search/advanced). You can specify coq-community as the user there and there is a drop-down menu that lets you choose a license kind. Here is an example of your request: https://github.com/search?q=user%3Acoq-community+license%3Amit&type=Repositories&ref=advsearch&l=&l=

view this post on Zulip Yves Bertot (Jun 19 2020 at 07:59):

Great thank you @Anton Trunov !

view this post on Zulip Karl Palmskog (Jun 19 2020 at 08:08):

For the record, I always try to use the exact words from the SPDX list for a license (both informal name and identifier): https://spdx.org/licenses/

Not all licenses are searchable like this on GitHub, e.g., CECILL-B

view this post on Zulip Yves Bertot (Jun 19 2020 at 11:44):

I am simply reviving an old development from 2010. I obtained from my co-author the permission to add the MIT license, I wanted to use an existing example to make sure I make it as searchable as possible. However, I don't intend to place under the umbrella of coq-community, because this would imply an engagement to maintain this code very precisely. So I only grabbed a few lines from the meta.yml example I found in coq-community/semantics. You may want to look at the current state of this project which is publicly available on an inria git host.

view this post on Zulip Karl Palmskog (Jun 19 2020 at 11:49):

note that we are taking special care so one can use meta.yml and our templates for non-coq-community projects, example here: https://github.com/uwplse/StructTact

view this post on Zulip Karl Palmskog (Jun 19 2020 at 11:51):

https://gitlab.inria.fr/bertot/delaunayflip does not seem to be publicly available yet though?

view this post on Zulip Yves Bertot (Jun 19 2020 at 12:15):

my mistake, it should be good now.

view this post on Zulip Anton Trunov (Jun 19 2020 at 12:20):

@Yves Bertot Could you perhaps rename Make file into _CoqProject to help the tools handle Coq projects in a uniform way?


Last updated: Feb 04 2023 at 02:03 UTC