Coq8.18 - FiniteType with multiple arguments

[maxkurze1]

No description provided.

[spacefrogg]

Please use a separate devShell for your shell hook. This one caused an infinite loop of opening sub shells on my end.

Also, the last commit breaks tests/large_writeset.v. It looks like interp_scheduler or tc_compute choke on the new type.

[spacefrogg]

Also, your changes broke the koika build on Coq 8.14. Can this be avoided or is it a necessary compromise to migrate to Coq 8.18?

The error looks as follows:

> File "./coq/Vect.v", line 1194, characters 20-33:
> Error: The reference N.Div0.mod_eq was not found in the current environment.

[spacefrogg]

I cherry-picked the documentation and Coq 8.18 commits, as they were independent of the changes to FiniteType.

[spacefrogg]

I dropped the use of clang-format. So, the clang-tools dependency is not necessary anymore.

[maxkurze1]

Please use a separate devShell for your shell hook. This one caused an infinite loop of opening sub shells on my end.

Also, the last commit breaks tests/large_writeset.v. It looks like interp_scheduler or tc_compute choke on the new type.

I am sorry, I didn't see an infinite recursion coming there. However, I am quite interested in how that happened - as far as I understand a simple exec bash should not evaluate the shellHook again or does it?

[maxkurze1]

Also, your changes broke the koika build on Coq 8.14. Can this be avoided or is it a necessary compromise to migrate to Coq 8.18?

The error looks as follows:

> File "./coq/Vect.v", line 1194, characters 20-33:
> Error: The reference N.Div0.mod_eq was not found in the current environment.

As far as I can tell, this "could" be avoided. However, due to changes in the Coq standard library, some of the old methods are deprecated now, and I went ahead and replaced most of them with their new alternatives. (When compiling with 8.14 however, these new versions cannot be found obviously)

Ideally I would like to keep the new versions to prevent problems going forward. If i remember correctly, there was a way to tell nix to use a specific version of the git repo for building with a specific version of coq. Maybe it would be best to just leave a 'coq-8.14' tag and tell nix to build with the old version (although in this case new features might not be available for coq 8.14)

[maxkurze1]

I cherry-picked the documentation and Coq 8.18 commits, as they were independent of the changes to FiniteType.

I also observed some problems when building with the new FiniteType (somehow nix build just worked while dune build got stuck somewhere). I will investigate that further once I got the time again. For now, I would recommend to just use the nix build if you want to experiment with the rule composition example.

[maxkurze1]

I dropped the use of clang-format. So, the clang-tools dependency is not necessary anymore.

That seems very reasonable. I will remove the dependency again.