Kazuhiko Sakaguchi (Jul 22 2020 at 15:56): 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
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.
Maxime Dénès (Jul 22 2020 at 16:46):Sounds fantastic!
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: Dec 05 2023 at 11:01 UTC