Hacker News Reader

Comment by anderskaseorg | Hacker News Reader

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

View on HN

What is the validator doing that the compiler isn't?

My understanding is that it's just smaller. By focusing entirely on validation it opens up less room for bugs.

Oh my! That `||` is gorgeous. I hadn't seen that before.

It'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.

Thanks, 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.

It'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.

Only 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.

Reply on news.ycombinator.com