logInfo in #eval

Stream: lean4

[Eric Wieser]

This log message seems to be going into the abyss:

import Lean
open Lean

#eval show MetaM Unit from logInfo m!"I am invisible"

is this expected behavior?

[Shreyas Srinivas]

Seems pretty normal. The return value is unit. #eval doesn't seem to care about doing anything other thanin the kernel evaluating expressions in the VM, getting the returned expr back, and printing it. See for example:

#eval ((do
        logInfo "something"
        return 2) : MetaM Nat)

[Alex J. Best]

It certainly isn't behaviour that has changed recently.
You can use dbg_trace in such evals, but normally I just make a command elab for testing such small things rather than #eval

[Kyle Miller]

@Shreyas Srinivas #eval knows about different monads due to the docs#MetaEval and docs#Eval classes.

In principle, it seems to me that the MetaM instances should be able to collect the logged info and report it somehow. Maybe the immediate problem is that these classes target IO instead of some monad supporting docs#Lean.MonadLog so there's nowhere for the messages to go, short of printing the messages.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Note that if you use an elaboration monad instead, then the message is shown: #eval show Elab.Command.CommandElabM Unit from logInfo m!"I am visible". This kind of inconsistency should count as a bug IMO.

[Shreyas Srinivas]

Since this thread came up again, I should probably mention that I have learnt since that eval can basically bypass the type checker when a prop is involved.

[Shreyas Srinivas]

(by bypass, I mean insert sorry and move on)