Stream: Coq devs & plugin devs

Topic: Extraction related issues


view this post on Zulip Kazuhiko Sakaguchi (Jul 22 2020 at 15:56):

In the Coq call today, I said I have some time to work on extraction this summer. Also, I read and sorted out all the extraction related issues reported (until the end of last year, I think). So here I have a list of issues classified into some categories (maybe I should put it as a meta issue to keep it visible): https://gist.github.com/pi8027/1a6050e5a90eeae1f4bb4de177d8ad08.

For me, it seems relatively easy to fix the value restriction issues, but it requires an infrastructure to properly generate fresh names which also fixes name conflict issues. I would like to give my priority to them because we can hope to close several issues in this way. CC: @Hugo Herbelin @Maxime Dénès @Jason Gross

view this post on Zulip Kazuhiko Sakaguchi (Jul 22 2020 at 15:59):

I will probably have to start with reading all the issues again because there are some new issues recently reported, and it may take some time. Anyway, I will try to work on this next week.

view this post on Zulip Maxime Dénès (Jul 22 2020 at 16:46):

Sounds fantastic!

view this post on Zulip Jason Gross (Jul 22 2020 at 19:30):

(maybe I should put it as a meta issue to keep it visible)

This might be a good use for GitHub Project Boards (https://github.com/coq/coq/projects).

Also, I believe you missed https://github.com/coq/coq/issues/11987 (a feature request of mine specifically about avoiding collision in name generation)


Last updated: Oct 21 2021 at 20:02 UTC