PrincetonUniversity / VST

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

`builtin` and `type` don't exist in `dash` (`util/make_version` is invoked inconsistently) #702

Closed JasonGross closed 10 months ago

JasonGross commented 10 months ago

util/make_version seems to be written for bash according to https://github.com/PrincetonUniversity/VST/blob/288866356f56222be47af66630602e5cc0e14490/util/make_version#L1 but the Makefile explicitly invokes it with https://github.com/PrincetonUniversity/VST/blob/288866356f56222be47af66630602e5cc0e14490/Makefile#L858 rather than ./util/make_version or util/make_version (without sh)

On systems (like default Ubuntu, I think) where sh is symlinked to dash, this results in

util/make_version: 4: builtin: not found
util/make_version: 21: gdate: not found

and then the script quits. This is mostly alright, though it results in the date definition being the empty string. According to stack exchange, command -v is the POSIX-compliant way of writing type -P. Alternatively, you could drop the sh invocation