Multiple match cases trigger

[dselsam]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Under certain circumstances, a

match t with
| c1 => ...
| c2 => ...

seems to go down both branches. If t is printed in a dbgTrace though, only the correct match fires.

Steps to Reproduce

1. Download the gist: https://gist.github.com/dselsam/95b2c833129a5661767ec64e7625e050
2. Build it and run it.

Expected behavior:

It should print out "APP" only, and return the empty list.

Actual behavior:

It prints out "CONST" and "APP" before returning the empty list.

Reproduces how often:

Every time.

Versions

Lean (version 4.0.0, commit bb8b13d, Debug)

Additional Information

[leodemoura]

Note that dbgTrace is effectful, but it is being used in a pure context. The compiler is applying transformations assuming the code is pure. So, unexpected behavior like the one above is not uncommon.
The Lean compiler extracts closed terms from functions and pre-computes them before the main function is executed. The terms dbgTrace "CONST" pure and dbgTrace "APP" pure are closed. So, they are extracted and executed before the main function. This is why you see both. If we disable the optimization using

set_option compiler.extract_closed false

Then, we get the expected behavior.
Note that this issue affects any effectful primitive that can be used in a pure context. Similar problems affect unsafeIO in Lean and Haskell. See http://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.IO.Unsafe.html#unsafePerformIO for Haskell.

I have experienced these issues with unsafeIO, but I have never had problems with dbgTrace. The main problem in your example is that the continuation of the dbgTrace applications does not depend on them.

You also have the fragment

  -- Also: why doesn't this print?
  let foo := dbgTrace ("t: " ++ toString t ) id;

in your example. The issue is similar, you have effectful code in a pure context, but a different compiler optimization is responsible for the unexpected behavior. Here, foo is a dead variable, and is eliminated by the dead variable elimination step in the compiler. If you replace

  let foo := dbgTrace ("t: " ++ toString t ) id;

with

  dbgTrace ("t: " ++ toString t ) $ fun _ =>

you will get the expected behavior.

[leodemoura]

@Kha It seems this will be a recurrent issue with new users. Not sure how we should handle it.
1- We can black-list dbgTrace and ensure compiler transformation such as dead-code elimination and extract close term are not applied to terms containing it.
2- We document dbgTrace and all issues. Unfortunately, very few users read documentation.
3- We can add a macro that helps users to use dbgTrace as we expect them to use. For example, if we have a macro dbgTrace! <msg>; <expr> which expands to dbgTrace <msg> (fun _ => <expr>), then users would find more natural to write

dbgTrace ("t: " ++ toString t );
...

than

let foo := dbgTrace ("t: " ++ toString t ) id;
...

[dselsam]

Thank you for the detailed explanation.

3- We can add a macro

I like this a lot, and think beginners probably wouldn't run into the let issue any more.

Bigger picture, dbgTrace seems to be in an uncanny valley of being deceptively like printf but not printf. I hope there could be more principled ways of debugging pure code. I don't know much about it but will search around a bit.

[leodemoura]

Bigger picture, dbgTrace seems to be in an uncanny valley of being deceptively like printf but not printf. I hope there could be more principled ways of debugging pure code. I don't know much about it but will search around a bit.

I am wondering if we can avoid this issue by explaining the macro dbgTrace! <msg>; <expr> as follows:
We use the macro dbgTrace! <msg>; <expr> for displaying debugging/trace messages at runtime. We should not view these messages as part of the output produced by our programs but as a temporary debugging aid. At runtime, the <msg> is displayed immediately before executing the expression <expr>. It is important to keep in mind that the compiler may eliminate <expr> and consequently the dbgTrace! <msg> command if the expression <expr> is dead code. For example, consider the expression

let x : Unit := dbgTrace! "hello world"; ();
y + 1

The variable x is dead code as is removed by the Lean compiler.
Another potential pitfall is when the expression <expr> is executed. For example, the Lean compiler produces code that runs and caches close expressions before it starts executing the main function. For example, consider the following code

def foo (x : Nat) : Bool :=
match x with
| 0 => dbgTrace! "x is zero"; true
| _ => false

The expression dbgTrace! "x is zero"; true is a close term. So, the Lean compiler decides to run it during program initialization. This behavior may give the impression the trace message is being displayed in the incorrect place.

[dselsam]

I think the explanation is clear. My concern was not that it is too hard to grasp what dbgTrace will do, but that using dbgTrace may not be as good a debugging tool as printf is for imperative languages. However, I think the flag set_option compiler.extract_closed false seems to address the main issue.

[dselsam]

How about:

1. adding the dbgTrace! <msg>; <expr> macro
2. (possibly) having an set_option imperative_style_debug_traces = true that sets the compiler flags to make tracing as favorable as possible.

[Kha]

Then perhaps the mere presence of dbgTrace! should disable these optimizations (by default)? If you have debug trace output in your functions, it's unlikely you care about its performance at that point. Not sure how to implement that though 😅 .

[leodemoura]

I think the explanation is clear. My concern was not that it is too hard to grasp what dbgTrace will do, but that using dbgTrace may not be as good a debugging tool as printf is for imperative languages. However, I think the flag set_option compiler.extract_closed false seems to address the main issue.

@dselsam I have used dbgTrace hundreds of times for debugging. It works as well as printf. You had a bad experience because you were using it around dead code or close terms. If you keep these two gotchas in mind, it works great.
Note that examples such as

def foo (x : Nat) : Bool :=
match x with
| 0 => dbgTrace! "x is zero"; true
| _ => false

are a bit artificial since we are not even including x in the trace message. If we write

def foo (x : Nat) : Bool :=
match x with
| 0 => dbgTrace! ("x is zero: " ++ toString x); true
| _ => false

as we usually do when inspecting variable values using printf, the dbgTrace! expression will not be an open term anymore.

[leodemoura]

Then perhaps the mere presence of dbgTrace! should disable these optimizations (by default)? If you have debug trace output in your functions, it's unlikely you care about its performance at that point. Not sure how to implement that though 😅 .

@Kha I agree. We can implement this feature if users are still having problems after we add the macro dbgTrace!.

[leodemoura]

We have the dbgTrace! macro in the new frontend.