Xavier Leroy

When I wrote "you'll find static class initialization methods greater than 64k in code", that was my experience a while ago when I was working on class file transformers. The...

Thanks for the proposal. I haven't had time yet to study the diff but will do soon. @andrew-appel, @jhjourdan, @robbertkrebbers, any opinions on this proposal?

Well spotted, thank you. Commit 1a52f58 updates the help message. Concerning printing the configuration, I'm still undecided, so I'll leave this issue open.

Related to #362.

> Is it true that a Vfloat value can have more than one representation (in Flocq) as a 64-bit bitvector? I would be very surprised. > If you look at...

I'm uneasy about this suggestion. CompCert [prides itself](https://xavierleroy.org/bibrefs/Boldo-Jourdan-Leroy-Melquiond-JAR.html) of compiling FP computations exactly as written in the source, without excess precision, "contraction", reassociation, or any of that stuff allowed by...

I would expect CompCert to work fine with Clang, with two caveats: 1- CompCert invokes `gcc` or _targetname_`-gcc` to perform preprocessing, assembling, and linking. This may need to be changed...

Apologies for taking so long to acknowledge this proposal. It's instructive to see how to get rid of proof irrelevance and how it "costs" in terms of proof effort. Thanks...

Also: this set of axioms (functional extensionality + proof irrelevance) was agreed a long time ago with @andrew-appel as a common basis for CompCert and for [VST](https://github.com/PrincetonUniversity/VST). I see VST...

Thanks for the extra explanations, very useful. I care much more about specifications than about proofs. CompCert tries hard to use the specification styles most appropriate for what needs to...