search

WasmCert / WasmCert-Coq

A mechanisation of Wasm in Coq
MIT License
92 stars 11 forks source link

Removing dependency on mathcomp #30

Closed raoxiaojia closed 11 months ago

raoxiaojia commented 11 months ago

As far as I'm aware, only the ssreflect part of mathcomp is used in the repository, which is now meregd into base Coq (as of version 8.18). So it makes sense to remove the dependency on it to avoid dealing with the slightly awkward CeCILL-B license (discovered in #29).

palmskog commented 11 months ago

@raoxiaojia looking around the codebase, it's pretty clear that you are using significant pieces of mathcomp-ssreflect that are not in Coq itself. The general idea is that the proof language SSReflect is in Coq, but most theories except for booleans is outside of Coq in MathComp.

Specifically, the theories here are defining canonical structures with decidable equality (eqType) and using MathComp sequences/lists and their notations (seq). This would be work to remove, just to avoid the CECILL-B licensing issues (which are basically only triggered by GPLv2 and GPLv3, which are not common in the Coq ecosystem).

cc: @spitters

raoxiaojia commented 11 months ago

That is true -- I had some thoughts about eqTypes and other things, but haven't realised that their lists (seq) are also not in base Coq. I guess this is too low a priority for now then.