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 add sources and exercises from Coq'Art book to Coq-community #78

Closed palmskog closed 5 years ago

palmskog commented 5 years ago

Move a project to coq-community

Project name: Coq sources and exercises from Coq'Art

Initial author(s): @Casteran @ybertot

Current URL: http://www.labri.fr/perso/casteran/CoqArt/

Kind: pure Coq library

License: CeCILL-B

Status: unclear (last update was for Coq 8.7)

Coq'Art is still the reference book I use most when working with Coq, and it would be great to have its Coq sources and exercises available for current and future Coq versions, continually checked via CI scripts we use for other projects.

@ybertot @Casteran do you agree this is a good idea?

I can help out with metadata and CI scripts, but don't have enough cycles for porting to recent versions of Coq.

Casteran commented 5 years ago

Dear Karl,

I agree !

I can prepare an update for CoqV8.9 with the sources and solutions of exercices of the Coq'Art from the 8.7 version. I think it will take some time if I integrate recent idioms but it should be ready for mid-september.

Then, we will organize the adaptation to the Coq-community format.

Yves, are you OK ?

Best regards,

Pierre

De: "Karl Palmskog" notifications@github.com À: "coq-community/manifesto" manifesto@noreply.github.com Cc: "pierre casteran" pierre.casteran@labri.fr, "Mention" mention@noreply.github.com Envoyé: Vendredi 26 Juillet 2019 00:46:18 Objet: [coq-community/manifesto] Proposal to add sources and exercises from Coq'Art book to Coq-community (#78)

Move a project to coq-community

Project name: Sources and exercises from Coq'Art

Initial author(s): [ https://github.com/Casteran | @Casteran ] [ https://github.com/ybertot | @ybertot ]

Current URL: [ http://www.labri.fr/perso/casteran/CoqArt/ | http://www.labri.fr/perso/casteran/CoqArt/ ]

Kind: pure Coq library

License: CeCILL-B

Status: unclear (last [ http://www.labri.fr/perso/casteran/CoqArt/booksite87-export.tar.gz | update ] was for Coq 8.7)

Coq'Art is still the reference book I use most when working with Coq, and it would be great to have its Coq sources and exercises available for current and future Coq versions, continually checked via CI scripts we use for other projects.

[ https://github.com/ybertot | @ybertot ] [ https://github.com/Casteran | @Casteran ] do you agree this is a good idea?

I can help out with metadata and CI scripts, but don't have enough cycles for porting to recent versions of Coq.

— You are receiving this because you were mentioned. Reply to this email directly, [ https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AJW6FCU6GVYMIFH6V7KN2G3QBIULVA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBS6QBQ | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AJW6FCUBISUJRE3MCJH7ZGTQBIULVANCNFSM4IG672FQ | mute the thread ] .

ybertot commented 5 years ago

I agree. I understand that Pierre will look at the problem of porting the stuff to coq 8.9. However, if Pierre wants some help, just write to me again about it.

Yves

From: "Karl Palmskog" notifications@github.com To: "coq-community/manifesto" manifesto@noreply.github.com Cc: "Yves Bertot" yves.bertot@inria.fr, "Mention" mention@noreply.github.com Sent: Friday, July 26, 2019 12:46:17 AM Subject: [coq-community/manifesto] Proposal to add sources and exercises from Coq'Art book to Coq-community (#78)

Move a project to coq-community

Project name: Sources and exercises from Coq'Art

Initial author(s): [ https://github.com/Casteran | @Casteran ] [ https://github.com/ybertot | @ybertot ]

Current URL: [ http://www.labri.fr/perso/casteran/CoqArt/ | http://www.labri.fr/perso/casteran/CoqArt/ ]

Kind: pure Coq library

License: CeCILL-B

Status: unclear (last [ http://www.labri.fr/perso/casteran/CoqArt/booksite87-export.tar.gz | update ] was for Coq 8.7)

Coq'Art is still the reference book I use most when working with Coq, and it would be great to have its Coq sources and exercises available for current and future Coq versions, continually checked via CI scripts we use for other projects.

[ https://github.com/ybertot | @ybertot ] [ https://github.com/Casteran | @Casteran ] do you agree this is a good idea?

I can help out with metadata and CI scripts, but don't have enough cycles for porting to recent versions of Coq.

— You are receiving this because you were mentioned. Reply to this email directly, [ https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AAZ73ZJ7VJIR5YVVN4MSIALQBIULTA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBS6QBQ | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AAZ73ZJRMTURVZKAN7IPCYDQBIULTANCNFSM4IG672FQ | mute the thread ] .

Casteran commented 5 years ago

Yes, I will advise you when I have a version that is fully compatible with coq V8.9 (no errors, no warnings). Pierre

----- Yves Bertot notifications@github.com a écrit :

I agree. I understand that Pierre will look at the problem of porting the stuff to coq 8.9. However, if Pierre wants some help, just write to me again about it.

Yves

From: "Karl Palmskog" notifications@github.com

To: "coq-community/manifesto" manifesto@noreply.github.com

Cc: "Yves Bertot" yves.bertot@inria.fr, "Mention" mention@noreply.github.com

Sent: Friday, July 26, 2019 12:46:17 AM

Subject: [coq-community/manifesto] Proposal to add sources and exercises from

Coq'Art book to Coq-community (#78)

Move a project to coq-community

Project name: Sources and exercises from Coq'Art

Initial author(s): [ https://github.com/Casteran | @Casteran ] [

https://github.com/ybertot | @ybertot ]

Current URL: [ http://www.labri.fr/perso/casteran/CoqArt/ |

http://www.labri.fr/perso/casteran/CoqArt/ ]

Kind: pure Coq library

License: CeCILL-B

Status: unclear (last [

http://www.labri.fr/perso/casteran/CoqArt/booksite87-export.tar.gz | update ]

was for Coq 8.7)

Coq'Art is still the reference book I use most when working with Coq, and it

would be great to have its Coq sources and exercises available for current and

future Coq versions, continually checked via CI scripts we use for other

projects.

[ https://github.com/ybertot | @ybertot ] [ https://github.com/Casteran |

@Casteran ] do you agree this is a good idea?

I can help out with metadata and CI scripts, but don't have enough cycles for

porting to recent versions of Coq.

—

You are receiving this because you were mentioned.

Reply to this email directly, [

https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AAZ73ZJ7VJIR5YVVN4MSIALQBIULTA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBS6QBQ

| view it on GitHub ] , or [

https://github.com/notifications/unsubscribe-auth/AAZ73ZJRMTURVZKAN7IPCYDQBIULTANCNFSM4IG672FQ

| mute the thread ] .

--

You are receiving this because you were mentioned.

Reply to this email directly or view it on GitHub:

https://github.com/coq-community/manifesto/issues/78#issuecomment-515383624

Casteran commented 5 years ago

Hello,

I updated the stuff to coq 8.9. The tar.gz is now at the following address : [ http://www.labri.fr/perso/casteran/CoqArt/coqart.V89.tar.gz | https://www.labri.fr/perso/casteran/CoqArt/coqart.V89.tar.gz ]

In addition to the examples and solutions of the exercises of the book, it contains also the scripts associated to the tutorials I co-authored with Eduardo and Matthieu. Please tell me if you have any problem to port this directory to Coq-community. I suggest that any improvement or additional stuff will be made in the community framework.

Best regards,

Pierre

De: "Yves Bertot" notifications@github.com À: "coq-community" manifesto@noreply.github.com Cc: "pierre casteran" pierre.casteran@labri.fr, "Mention" mention@noreply.github.com Envoyé: Vendredi 26 Juillet 2019 11:42:42 Objet: Re: [coq-community/manifesto] Proposal to add sources and exercises from Coq'Art book to Coq-community (#78)

BQ_BEGIN I agree. I understand that Pierre will look at the problem of porting the stuff to coq 8.9. However, if Pierre wants some help, just write to me again about it.

Yves

From: "Karl Palmskog" notifications@github.com To: "coq-community/manifesto" manifesto@noreply.github.com Cc: "Yves Bertot" yves.bertot@inria.fr, "Mention" mention@noreply.github.com Sent: Friday, July 26, 2019 12:46:17 AM Subject: [coq-community/manifesto] Proposal to add sources and exercises from Coq'Art book to Coq-community (#78)

Move a project to coq-community

Project name: Sources and exercises from Coq'Art

Initial author(s): [ https://github.com/Casteran | @Casteran ] [ https://github.com/ybertot | @ybertot ]

Current URL: [ http://www.labri.fr/perso/casteran/CoqArt/ | http://www.labri.fr/perso/casteran/CoqArt/ ]

Kind: pure Coq library

License: CeCILL-B

Status: unclear (last [ http://www.labri.fr/perso/casteran/CoqArt/booksite87-export.tar.gz | update ] was for Coq 8.7)

Coq'Art is still the reference book I use most when working with Coq, and it would be great to have its Coq sources and exercises available for current and future Coq versions, continually checked via CI scripts we use for other projects.

[ https://github.com/ybertot | @ybertot ] [ https://github.com/Casteran | @Casteran ] do you agree this is a good idea?

I can help out with metadata and CI scripts, but don't have enough cycles for porting to recent versions of Coq.

— You are receiving this because you were mentioned. Reply to this email directly, [ https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AAZ73ZJ7VJIR5YVVN4MSIALQBIULTA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBS6QBQ | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AAZ73ZJRMTURVZKAN7IPCYDQBIULTANCNFSM4IG672FQ | mute the thread ] .

— You are receiving this because you were mentioned. Reply to this email directly, [ https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AJW6FCTVKWPQNMHFDFHZ5XTQBLBJFA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD24CCSA#issuecomment-515383624 | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AJW6FCQUKOK6N4P4CQMPQRDQBLBJFANCNFSM4IG672FQ | mute the thread ] . BQ_END

palmskog commented 5 years ago

Dear Pierre and Yves,

As you may have already noticed, I created the Coq-community repository and imported the sources from Pierre's 8.9 archive: https://github.com/coq-community/coq-art

With your permission, I will continue to help out with continuous integration and metadata for the repository (but will not modify actual Coq content).

Casteran commented 5 years ago

Thank you !

By the way, I forgot to remove some old files which are useless now. Since I'm not expert in github yet, could you remove them ? alltex.sh AFAIRE.txt README.txt make_project To_do.txt

Best regards,

Pierre

De: "Karl Palmskog" notifications@github.com À: "coq-community" manifesto@noreply.github.com Cc: "pierre casteran" pierre.casteran@labri.fr, "Mention" mention@noreply.github.com Envoyé: Dimanche 28 Juillet 2019 17:35:24 Objet: Re: [coq-community/manifesto] Proposal to add sources and exercises from Coq'Art book to Coq-community (#78)

Dear Pierre and Yves,

As you may have already noticed, I created the Coq-community repository and imported the sources from Pierre's 8.9 archive: [ https://github.com/coq-community/coq-art | https://github.com/coq-community/coq-art ]

With your permission, I will continue to help out with continuous integration and metadata for the repository (but will not modify actual Coq content).

— You are receiving this because you were mentioned. Reply to this email directly, [ https://github.com/coq-community/manifesto/issues/78?email_source=notifications&email_token=AJW6FCQEV4ZIM6SC6OC6FVTQBW4DZA5CNFSM4IG672F2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD27BAUQ#issuecomment-515772498 | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AJW6FCTYBBFTHGU2CVYN3T3QBW4DZANCNFSM4IG672FQ | mute the thread ] .

palmskog commented 5 years ago

Hi Pierre,

Sure, I can take care of removing those files when I add scripts for CI.

Thanks, Karl

Zimmi48 commented 5 years ago

@palmskog Should we close this now that the repository has been created?