Skip to content

Port changes from MetaCoq

Yannick Forster requested to merge yforster/coq-bytestring:master into master

In MetaCoq we have been relying on bytestrings for a while, since Coq's strings turned out to be way too inefficient.

In the process, Matthieu (@mattam82) has made several adjustments, mostly to improve efficiency even more. If I understand correctly, the main change is to do comparison of bytes by converting them to N. Matthieu also introduced trees over bytestrings to have a more efficient append functionality.

Due to request from the ConCert team we would be interested on relying on an up-to-date coq-bytestring package, rather than using and adapting the file.

This PR is for now just a place to discuss whether you (@gmalecha / other bedrock people) would be interested in updating coq-bytestring to newer Coq versions and in incorporating Matthieu's changes. I happily volunteer to do the busywork regarding version compatibility of Coq and opam files.

The corresponding file by Matthieu is here. I tried to keep the new file structure closer to the original and reverted some renaming Matthieu did (the module is called Bytestring again, not String, which will also reduce confusion in projects depending on MetaCoq in the future). A version of MetaCoq compiling with the content of this MR installed is here.

Merge request reports