Skip to content

Commit 659a079

Browse files
Add log-timing for implies and simplify in docs (#3844)
The documentation mentions `log-timing` is a valid option for `implies` and `simplify`: https://github.com/runtimeverification/haskell-backend/blob/5db6dfc03c9f3b18191bf35954a966a59c441cba/docs/2022-07-18-JSON-RPC-Server-API.md?plain=1#L304 This PR includes the parameter under the corresponding request descriptions. Co-authored-by: rv-jenkins <[email protected]>
1 parent a0907df commit 659a079

File tree

1 file changed

+12
-7
lines changed

1 file changed

+12
-7
lines changed

docs/2022-07-18-JSON-RPC-Server-API.md

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -337,12 +337,13 @@ Not all backends support logging processing time, and some won't have the differ
337337
"params": {
338338
"antecedent": {"format": "KORE", "version": 1, "term": {}},
339339
"consequent": {"format": "KORE", "version": 1, "term": {}},
340-
"module": "MODULE-NAME"
340+
"module": "MODULE-NAME",
341+
"log-timing": true
341342
}
342343
}
343344
```
344345

345-
Optional parameters: `module` (main module name)
346+
Optional parameters: `module` (main module name), `log-timing`
346347

347348
### Error Response:
348349

@@ -390,7 +391,8 @@ If the implication holds, `satisfiable` is `true` and `condition` contains a wit
390391
"condition": {
391392
"substitution": {"format": "KORE", "version": 1, "term": {}},
392393
"predicate": {"format": "KORE", "version": 1, "term": {}}
393-
}
394+
},
395+
"logs": []
394396
}
395397
}
396398
```
@@ -403,7 +405,8 @@ If the implication cannot be shown to hold, `satisfiable` is false.
403405
"id": 1,
404406
"result": {
405407
"implication": {"format": "KORE", "version": 1, "term": {}},
406-
"satisfiable": false
408+
"satisfiable": false,
409+
"logs": []
407410
}
408411
}
409412
```
@@ -429,12 +432,13 @@ indicating that the program configuration can be rewritten further => `satisfiab
429432
"method": "simplify",
430433
"params": {
431434
"state": {"format": "KORE", "version": 1, "term": {}},
432-
"module": "MODULE-NAME"
435+
"module": "MODULE-NAME",
436+
"log-timing": true
433437
}
434438
}
435439
```
436440

437-
Optional parameters: `module` (main module name)
441+
Optional parameters: `module` (main module name), `log-timing`
438442

439443
### Error Response:
440444

@@ -447,7 +451,8 @@ Same as for execute
447451
"jsonrpc": "2.0",
448452
"id": 1,
449453
"result": {
450-
"state": {"format": "KORE", "version": 1, "term": {}}
454+
"state": {"format": "KORE", "version": 1, "term": {}},
455+
"logs": []
451456
}
452457
}
453458
```

0 commit comments

Comments
 (0)