Sync with deps

[floriangru]

This builds with extructures 0.2.0, coq-utils 0.2.0 (and the math-comp libaries 1.9.0 with coq 8.9.1). Building coq-utils can be streamlined by pinning it with the upstream repo when arthuraa/coq-utils#3 would be merged. In the meantime, opam pin add coq-utils and copy-pasting the content of the file added in the coq-utils PR works for me.

[floriangru]

Now the project compiles well with the coq-utils version pinned as a submodule !
Tests are compiling as well but the changes in master that occured in between seem to cause (extremely strangely) a bad derivation of a very simple type (the registers at the intermediate level, which is basically an enum) :

File "./Tests/IntermediateProgramGeneration.v", line 220, characters 0-51:
Error:
Recursive definition of aux_shrink is ill-formed.
...

It works well without merging master though

[floriangru]

Ok it's been fixed (register was redefined as a Variant and it didn't work well with QuickChick deriving

[floriangru]

The issue for the derivation of variant is documented here but it doesn't look like it would be taken care of anytime soon QuickChick/QuickChick#155

[catalin-hritcu]

I'm building Coq directly, never via opam. Can I still build things?

[robblanco]

@floriangru and I discussed the changes again earlier today. In principle, everything should be ready for a final test and merge; I'll start looking at that now.

@catalin-hritcu As I understand it, you always have the choice of how to build, but you have the option to use opam to take care of the dependencies for you. In any case, the OPAM description file does not override the need for a description of the dependencies (if reading them from the file is not good enough).

[catalin-hritcu]

This works well for me too ... without any opam beyond for installing OCaml 4.08.1 ... so we should lift the 4.06 upper bound here:

Our tests are known to work with QuickChick branch 8.9 and OCaml from 4.02.3 to 4.06.

Here also the 4.02.3 lower bound seems quite hard to believe ... has anyone tried? :)

[floriangru]

This works well for me too ... without any opam beyond for installing OCaml 4.08.1 ... so we should lift the 4.06 upper bound here:

Apart from the extracted examples failing for most of them, the testing of SFI worked with 4.09.0 as well (up to 263 generated tests, didn't wait until the 600th)

Our tests are known to work with QuickChick branch 8.9 and OCaml from 4.02.3 to 4.06.

Here also the 4.02.3 lower bound seems quite hard to believe ... has anyone tried? :)

We'll have to lift the lower bound to 4.05.0 if we want compatibility with coq 8.10 (which now only depends on Arthur's libraries), so we won't have to try the older versions 😌