set exit code

Stream: general

[Matthew Ballard]

I assume there is no way to set the exit code for lean oof.lean in off.lean, correct?

[Alex J. Best]

I don't know if there is a recommended way, but if code fails the exit code will be 1, otherwise 0.
So something like

import system.io

meta
def main : io unit :=
do
  l ← io.get_line,
  if l = "secret_password" then io.print_ln "good" else io.fail "access denied"

has the following behavior

$ lean --run io.lean
secret_password
good
$ echo $?
0
$ lean --run io.lean
asdas
access denied
$ echo $?
1

[Matthew Ballard]

But there is no way to make it emit 0 with asdas, right?

[Matthew Ballard]

I realize this is a silly behavior when you verifying something but wanted to check

[Alex J. Best]

I guess there is no way to make lean exit zero if there is an error anywhere? But if the code checks with code 0 then you could choose when the code fails and emits 1, separately to whatever you print (you can always call tactics and capture the errors and print them, rather than letting the exception propogate up the call stack). But if there is something that genuinely errors in a tactic you don't control I don't know how you could capture that.

[Matthew Ballard]

Last I checked introducing constant proof : My_HWwill give you an exit of 0 where you might have had 1 before. But I am really looking for some functionality to set the exit code directly. I was 90% sure such a thing doesn’t exist. Now it’s 99%

[Sebastian Ullrich]

The only robust way to check whether a Lean file has indeed proved something is by inspecting the resulting .olean (or other export) file from outside the Lean process that created it. This is of course much easier in Lean 4 where there is a Lean API to do that, but if you are familiar with Haskell, Scala, or Rust, you could also extend one of the external Lean 3 checkers for that. In fact, depending on their output and pretty printer, it might be sufficient to carefully parse their output without modifying them.

[Matthew Ballard]

Thanks! I’ll definitely take a look. I assume the external tools are equally pleasant?

[Gabriel Ebner]

This is of course much easier in Lean 4 where there is a Lean API to do that

We also have an API to import modules in Lean 3. Note that using withImportModules is not safe in Lean 4 (i.e., it can easily crash Lean), so be careful when using it for a proof checker.