Support for Coq 8.5

[catalin-hritcu]

Maxime already started working on this.

[catalin-hritcu]

Will the plugin still work with 8.4 though? I think we should try to maintain compatibility with 8.4 for quite a while, since that's what most people will keep using.

[jwiegley]

Any news on whether the plugin will work with 8.5b2?

[catalin-hritcu]

Maxime can answer better, he started a 8.5 port a while back, but then we realized this would break support for 8.4, which is more widely used at this point, so we postponed the move. The code is more stable now, so supporting both for a while might be easier now than it was back then?

[jwiegley]

I'd be happy to beta test for you on both platforms, since I use both fairly actively.

[jwiegley]

@catalin-hritcu I've received approval here at BAE to put some work time into assisting QuickChick. Is there something I can do to help with the upgrade to 8.5?

[catalin-hritcu]

I've just pinged Maxime about this. Hopefully he can give you some guidance with this.

[maximedenes]

Sorry for the late reply, I've started to work on making the plugin compile again with the current 8.5. Once this is done, it will need a lot of testing, so any help welcome @jwiegley

The interfaces for plugins have changed a lot between 8.4 and 8.5 so I don't think we can support both from the same version of the plugin. So I'll create a branch. The .v files should be easy to share, though.

[jwiegley]

@maximedenes Ok, just let me know when to start on it, and I'll put several hours into writing tests. Also, if you're away of any areas to concentrate on especially, I can pay special attention there.

[catalin-hritcu]

I would say the sooner, the better.

[jwiegley]

Is it ready to start testing against 8.5b2? I will be able to put time into it after ICFP next week.

[maximedenes]

The coq8.5 branch of QuickChick should be ready to be tested against Coq 8.5 now.

It is known to compile with coq 8.5 branch (head ae8f8433) and with Mathematical Components master branch (head ade7c12) on github https://github.com/math-comp/math-comp

Unlike what I said previously, I actually had to update the .v files in a way that is not backward compatible (with coq 8.4). I hope it's ok, since it is relatively small changes.

@jwiegley Thanks for you help testing!

[maximedenes]

This can probably be closed now.