search

PrincetonUniversity / VST

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

`make install` silently installs nothing when `IGNORECOMPCERTVERSION=true` is passed and the versions mismatch #706

Closed JasonGross closed 10 months ago

JasonGross commented 10 months ago

https://github.com/PrincetonUniversity/VST/blob/288866356f56222be47af66630602e5cc0e14490/Makefile#L671 invokes util/calc_install_files without setting IGNORECOMPCERTVERSON, and the makefile contains no export IGNORECOMPCERTVERSION, so https://github.com/PrincetonUniversity/VST/blob/288866356f56222be47af66630602e5cc0e14490/util/calc_install_files#L5 is run without passing along IGNORECOMPCERTVERSION, and the result is an error message like

Makefile:131: *** COMPCERT VERSION MISMATCH: COMPCERT_VERSION=version=3.12 but /home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/compcert/VERSION=version=3.14.  Stop.

which isn't displayed due to >& /dev/null