You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When used with an external CompCert, VST configures itself by looking at CompCert's Makefile.config to learn the target architecture and BITSIZE. But when CompCert has been installed with Opam, there is no Makefile.config present. Thus, VST does not build properly.
an installed CompCert provides a file called compcert.config which contains equivalent information to Makefile.config but is specifically intended for use by Coq makefiles, while Makefile.config was more a CompCert internal file.
This is supported by the coq-compcert.3.7~coq-platform series of packages and will also be supported by the main (non platform) compcert.3.8 package. VST should anyway use the coq-platform variants of CompCert, which use the platform supplied Flocq.
The new Makefile uses compcert.config, so I would consider this as fixed.
When used with an external CompCert, VST configures itself by looking at CompCert's Makefile.config to learn the target architecture and BITSIZE. But when CompCert has been installed with Opam, there is no Makefile.config present. Thus, VST does not build properly.
Thanks to @ybertot for reporting this.
The text was updated successfully, but these errors were encountered: