4 ms·
This incorrectly passes the compiler, which is certainly a bug, but it does not pass the validator. $ ./configure.sh $ make coqdep -c -slash -R . Falso "
by anderskaseorg 12y ago
This incorrectly passes the compiler, which is certainly a bug, but it does not pass the validator.
$ ./configure.sh
$ make
coqdep -c -slash -R . Falso "All.v" > "All.v.d" || ( RV=$?; rm -f "All.v.d"; exit ${RV} )
coqc -q -R . Falso All
$ make validate
coqchk -silent -o -R . Falso All
Type error
Makefile:133: recipe for target 'validate' failed
make: *** [validate] Error 1
- panic 12y agoWhat is the validator doing that the compiler isn't?
- tel 12y agoMy understanding is that it's just smaller. By focusing entirely on validation it opens up less room for bugs.
- deafbybeheading 12y agoOh my! That `||` is gorgeous. I hadn't seen that before.
- userbinator 12y agoIt's like the opposite of && (continue until one alternative is false), for if you want to continue with alternatives in sequence until one alternative becomes true: a || b || c || ... This usage is commonly found in other places than the shell, like JavaScript, Perl, and PHP.
- deafbybeheading 12y agoThanks, I know `||` in general--I meant I hadn't seen the specific construction GP had used. The error handling to delete the output file in case the command failed is really elegant.
- peff 12y agoIt's actually a little dangerous; what happens when you hit "^C" and the process dies before getting a chance to clean up? It's safer to do: some_cmd >foo.tmp && mv foo.tmp foo The mv will do an atomic rename(), so that you either get the fully formed contents, or nothing at all.
- deafbybeheading 12y agoOnly if you interrupt the actual `rm`, no? If you interrupt the main command, you won't get a 0 exit code so the `||` branch still executes. Your mechanism is clearly safer, but the user is required to clean up `foo.tmp` themselves in case of failure, so it's not really comparable.