Andrew Appel

More measurements, [shown here](https://github.com/PrincetonUniversity/VST/files/7303388/issue514.txt) demonstrate that having 20 lvars, with the associated 20 data_at conjuncts, and functions with between 0 and 20 pointer parameters (with the corresponding 0 to 20...

Generally speaking, VST correctly handles the issues just mentioned by @roconnor-blockstream. If you don't recall seeing maximum-width side-conditions, it's because VST efficiently (and soundly) optimizes those away when the shift...

Can you give an example of a proof goal in which this documentation would be useful?

I would have thought that ExportClight.ml would also need to be edited, but I don't see that in the list of "files changed."

Yes, I'm pretty sure it does. I don't have time to test it this month. I recommend merge the P.R. Thank you.

What about the fact that symlinks don't always work in cygwin? Will this be an issue for Coq following -Q options via symlink, in the Windows build?

Regarding what is the "default": Although the "default" VST has been 32-bit in the past, I think it would be fine if the "default" VST installation were 64-bit. I regularly...

> P.S.: the main downside of variant 3) is that we are talking about a lot of opam packages Isn't that also true for variant 4) ? And a separate...

I will leave this issue open for a few days, while I consider whether to create a new release 2.11 of VST that incorporates new concurrency features. If I don't...

I have created VST release 2.11 and tagged it: https://github.com/PrincetonUniversity/VST/releases/tag/v2.11 Please use this for the Coq Platform release.