Add `debug` built-in #1267

romac · 2023-11-24T09:55:11Z

Closes: #1266

The debug built-in is a utility for aiding in debugging specifications by allowing the spec developer to print out a contextual message while executing a specification, whether in a run or in a test, along with a formatted representation of a value.

This can be useful when trying to understand the state of variables at specific points during the spec execution or while tracking down issues.

The debug function has the following signature:

def debug(header: str, value: a) -> a

The debug function prints both header and the value on the same line, preceded by a > character, and then returns the given value, which makes it easy to debug nested expressions without having the extract them into a variable first.

Example usage in the REPL:

>>> debug("a number:", 42)
> a number: 42
42

>>> debug("a record:", { foo: 32, bar: true })
> a record: { bar: true, foo: 32 }
{ bar: true, foo: 32 }

>>> debug("large record:", largeRecord)
> large record: {
  hello:
    {
      world:
        { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } }
    }
}
{
  hello:
    {
      world:
        { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } }
    }
}

>>> if (a * debug("nested", a + b) == 10) true else false
> nested 5
true

Tests added for any new code
Documentation added for any new functionality
Entries added to the respective CHANGELOG.md for any new functionality
Feature table on README.md updated for any listed functionality

The `debug` function is a utility designed to aid in debugging specifications by allowing the spec developer to print out a contextual message while executing a specification, whether in a run or in a test, along with a formatted representation of a value. This can be useful when trying to understand the state of variables at specific points during the spec execution or while tracking down issues. The `debug` function has the following signature: ``` def debug(header: str, value: a) -> a ``` The `debug` function prints both header and the value on the same line, preceded by a `>` character, and then returns the given value, which makes it easy to debug nested expressions without having the extract them into a variable first. Example usage in the REPL: ``` >>> debug("a number:", 42) > a number: 42 42 >>> debug("a record:", { foo: 32, bar: true }) > a record: { bar: true, foo: 32 } { bar: true, foo: 32 } >>> debug("large record:", largeRecord) > large record: { hello: { world: { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } } } } { hello: { world: { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } } } } >>> if (a * debug("nested", a + b) == 10) true else false > nested 5 true ```

bugarela

I love it! Thanks for getting this done, I'm sure it will be super useful.

I'd do three things before merging:

Adding an entry to CHANGELOG.md
Adding an integration test to io-cli-tests.md (i.e. evaluating a quint REPL shell invocation and checking that the debug line is sent to STDOUT)
Add an entry to builtin.qnt for debug with a docstring (and running npm run api-docs to generate a Markdown). This is used for showing overlay documentation in the IDEs.

If you are interested in doing any of those, please go ahead! Otherwise, I can pick it up 😄

romac · 2023-11-24T13:54:05Z

Thanks a lot for the pointers! I've done all three things, let me know if you want me to add more tests or expand on the documentation.

romac · 2023-11-24T13:56:53Z

I wonder if it would make sense to switch the arguments around, to allow for writing the following in method-call style:

>>> 42.debug("value is")
> value is 42

The downside with this order is that when used as a function it now reads less well imho:

>>> debug(42, "value is")
> value is 42

I don't feel strongly either way, so will defer to you on that if you don't mind :)

quint/src/builtin.qnt

quint/src/effects/builtinSignatures.ts

konnov

I like this feature! But I have my doubts about the operator name debug:

It only works for REPL. We add the prefix q:: to all internal or repl-specific operators.
The name misleading is a bit misleading. It's not really debugging anything. Quick alternatives from gdb: print, inspect, trace. Of course, I would prefer them to have the prefix q::.

konnov · 2023-11-24T14:59:34Z

quint/src/runtime/impl/compilerImpl.ts

+          this.applyFun(app.id, 2, (msg, value) => {
+            let columns = terminalWidth()
+            let valuePretty = format(columns, 0, prettyQuintEx(value.toQuintEx(zerog)))
+            console.log('>', msg.toStr(), valuePretty.toString())


Even though it works this way. Would not it be better to print the message via CompilerErrorTracker? We could probably introduce a debug/info level for this purpose.

I'd suggest leaving this as is for now, and replacing it with the proper logging lib along with all our other console prints when we get around to that. This is not a compilation error, so I wouldn't want to put it in the tracker for that.

romac · 2023-11-24T15:35:53Z

It only works for REPL. We add the prefix q:: to all internal or repl-specific operators.

Oh I wasn't aware of that. I'll see if I can figure out how to do that.

The name debug is a bit misleading. It's not really debugging anything. Quick alternatives from gdb: print, inspect, trace. Of course, I would prefer them to have the prefix q::.

Good point! If you ask me I would go with inspect:

a) to avoid overloading the "trace" term too much which could be confusing/misleading
b) while print might be a good alternative, I think a print built-in should allow omitting the value argument altogether and only print the message in that case. Conversely, an argument can probably be made for allowing one to pass only the value without a message to debug but I hadn't considered that previously.

konnov · 2023-11-24T16:22:23Z

I also like inspect or q::inspect :)

romac · 2023-11-24T16:56:55Z

Yeah I meant q::inspect :)

shonfeder · 2023-11-24T17:45:20Z

Thanks for the useful addition!

We'll need to make sure we strip this out of the IR before sending to alache I think, but we can do that in a followup.

bugarela · 2023-11-24T18:35:15Z

I personally like debug (or q::debug) more than inspect or the other alternatives. But I don't feel too strong about it.

bugarela · 2023-11-27T12:41:38Z

How should we proceed here? Should we go with q::inspect, or do we want to have further sync/async discussions on this?

konnov · 2023-11-28T15:44:15Z

How should we proceed here? Should we go with q::inspect, or do we want to have further sync/async discussions on this?

I would vote for proceeding like that.

thpani · 2023-11-28T16:37:57Z

I personally like debug (or q::debug) more than inspect or the other alternatives. But I don't feel too strong about it.

I'd also prefer debug (or even log) over inspect, but I'm not gonna block on naming.

konnov · 2023-12-04T12:16:08Z

@romac do you need help in getting this one merged?

romac · 2023-12-04T12:25:47Z

I was just waiting for the Quint team to decide on the final name, but if/once that's done I am happy to do the renaming if needed and prefix it with the q:: namespace :)

romac · 2023-12-05T10:44:50Z

I merged main in and moved debug under the q:: namespace.

Shall we keep the name or do I rename it to something else?

bugarela

I talked to the team and we are going with q::debug! Thanks for the patience and for all the updates.

romac · 2023-12-05T12:23:34Z

Thanks for helping me see this PR through!

romac force-pushed the romac/debug branch from fbcaff4 to e3e4bdc Compare November 24, 2023 09:56

romac changed the title ~~Add debug utility function~~ Add debug built-in Nov 24, 2023

bugarela reviewed Nov 24, 2023

View reviewed changes

romac added 4 commits November 24, 2023 14:09

Add changelog entry

3a85316

Add REPL test for debug

f2aa734

Rename header to msg

5e57cb4

Add documentation for debug built-in

b4557aa

Update generated documentation

5877cdd

romac requested a review from bugarela November 24, 2023 14:13

romac commented Nov 24, 2023

View reviewed changes

quint/src/builtin.qnt Outdated Show resolved Hide resolved

quint/src/effects/builtinSignatures.ts Outdated Show resolved Hide resolved

konnov self-requested a review November 24, 2023 14:52

konnov reviewed Nov 24, 2023

View reviewed changes

romac added 3 commits December 5, 2023 11:33

Merge branch 'main' into romac/debug

f2edb83

Move debug built-in to the q:: namespace

755fab6

Fix missing namespace in signature

db48556

Formatting

a95e495

bugarela approved these changes Dec 5, 2023

View reviewed changes

bugarela merged commit 84c12a7 into informalsystems:main Dec 5, 2023
15 checks passed

romac deleted the romac/debug branch December 5, 2023 12:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add `debug` built-in #1267

Add `debug` built-in #1267

romac commented Nov 24, 2023 •

edited

Loading

bugarela left a comment •

edited

Loading

romac commented Nov 24, 2023

romac commented Nov 24, 2023

konnov left a comment •

edited

Loading

konnov Nov 24, 2023

shonfeder Nov 24, 2023

romac commented Nov 24, 2023

konnov commented Nov 24, 2023

romac commented Nov 24, 2023

shonfeder commented Nov 24, 2023

bugarela commented Nov 24, 2023

bugarela commented Nov 27, 2023

konnov commented Nov 28, 2023

thpani commented Nov 28, 2023

konnov commented Dec 4, 2023

romac commented Dec 4, 2023

romac commented Dec 5, 2023

bugarela left a comment

romac commented Dec 5, 2023

Add debug built-in #1267

Add debug built-in #1267

Conversation

romac commented Nov 24, 2023 • edited Loading

bugarela left a comment • edited Loading

Choose a reason for hiding this comment

romac commented Nov 24, 2023

romac commented Nov 24, 2023

konnov left a comment • edited Loading

Choose a reason for hiding this comment

konnov Nov 24, 2023

Choose a reason for hiding this comment

shonfeder Nov 24, 2023

Choose a reason for hiding this comment

romac commented Nov 24, 2023

konnov commented Nov 24, 2023

romac commented Nov 24, 2023

shonfeder commented Nov 24, 2023

bugarela commented Nov 24, 2023

bugarela commented Nov 27, 2023

konnov commented Nov 28, 2023

thpani commented Nov 28, 2023

konnov commented Dec 4, 2023

romac commented Dec 4, 2023

romac commented Dec 5, 2023

bugarela left a comment

Choose a reason for hiding this comment

romac commented Dec 5, 2023

Add `debug` built-in #1267

Add `debug` built-in #1267

romac commented Nov 24, 2023 •

edited

Loading

bugarela left a comment •

edited

Loading

konnov left a comment •

edited

Loading