search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

Pass `COQEXTRAFLAGS` through to `coqc` #714

Closed JasonGross closed 9 months ago

JasonGross commented 9 months ago

This mimics the behavior of coq_makefile a bit more, and will allow the next release of VST to be compatible with coq-native even when its dependencies are not. For example, compcert only installs .coq-native files since version 3.13, cf https://github.com/AbsInt/CompCert/issues/476, and this change allows VST to be compatible with earlier versions of compcert even when coq-native is installed.

JasonGross commented 9 months ago

Ah, but I guess VST is specific to a particular version of compcert, so this won't be much use?