Release ritsu v0.55.0 · i2y/ritsu

ritsu 0.55.0

rulec now stops with E102 a row that a derive's reach and a constraint leave out together, whatever the order of the axes; 0.54.0 let such a row through with W128, saying that nothing had shown it unreachable. A row that a constraint alone leaves out passes, now without W128 where a derive takes part, and rulec coverage, which lists it, now names the constraint that leaves it out, where it used to say the vectors had found no input for it. rulec verify now says on standard error, once, when an adapter has left the handshake or a record unanswered for 30 seconds — most often an adapter that does not flush its output — and goes on waiting.

Fixed (rulec)

A row past a derive's reach that a constraint leaves out as well is E102, whatever the order of the axes. The third form of E102 walks the points of a row with the axes in the order of their sizes, and writes down the first test that leaves a point out. Where a constraint on two inputs came before the derive's axis, the walk never came to the derive, the row was not stopped for the reach, and W128 then said of it that no input reaching it was found and none was shown not to. A row the walk leaves out with no derive taking part is now walked again with the derives asked first. Here refund comes to at most 20 pounds, and no more items come back than were ordered:

rule return_route v1

enum route = decline | approve | review

inputs
  paid     : money[GBP]  range >=0GBP <=20GBP
  fee      : money[GBP]  range >=0GBP <=10GBP
  returned : number  range >=0 <=10
  ordered  : number  range >=0 <=10

constraint returned <= ordered

outputs
  outcome : route

derive refund : money[GBP] = paid - fee  range >=-1000GBP <=1000GBP

table route_of
policy first
| refund         | returned | ordered | -> outcome : route |
| <=0GBP         | -        | >=5     | decline            |
| >0GBP <=200GBP | -        | >=5     | approve            |
| >50GBP         | >5       | <=5     | review             |
| -              | -        | -       | approve            |

0.54.0 passed the rule with a warning on row 3:

$ rulec check return_route.rule
warning[W128]: No input was found that reaches row 3, and none was shown not to
  --> return_route.rule:23 table route_of
   |
23 | | >50GBP         | >5       | <=5     | review             |
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ row 3: undecided
   |
 This row asks for values of `refund`, which are computed. An input that gives them was looked for and not found, and it could not be shown that no input does.
 Look at the expressions and the row's conditions together to see whether some input reaches it. If one does, write it as an example and this warning goes; if none does, delete the row. If deleting it brings a completeness gap (E101), rulec cannot show that the combination never comes either, and the row can stay.

note return_route.rule: 2 shadow pairs (2 structural, 0 equivalent, 0 needs review)
ok return_route.rule

This release stops it:

$ rulec check return_route.rule
error[E102]: Unreachable row: row 3 never matches
  --> return_route.rule:23 table route_of
   |
23 | | >50GBP         | >5       | <=5     | review             |
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ row 3: no input reaches here
16 | derive refund : money[GBP] = paid - fee  range >=-1000GBP <=1000GBP
   |                              ^^^^^^^^^^ the reachable interval is >=-10GBP <=20GBP
   |
 Over the ranges of the inputs, `refund` can only come to >=-10GBP <=20GBP. None of those values meets this row's conditions.
 hint: rewrite the condition within the values `refund` can come to, or delete this row. Widening a derive's `range` does not change the values it can come to.

note return_route.rule: 2 shadow pairs (2 structural, 0 equivalent, 0 needs review)

W128 no longer calls undecided a row that a constraint alone leaves out. A row whose cell on a derive lies within what the derive comes to, and which only a constraint, a never, koyomi's days or a table above leaves out, now passes without W128, as such a row does in a table with no computed column. Its certificate is the same as 0.54.0's, which already listed the row in unreachable. 0.53.0 and 0.54.0 said W128 of it.
rulec coverage says what leaves out a row that no input reaches. check passes a row that only a constraint leaves out (E102 stops a row that a constraint leaves out only where a derived or define value takes part too), and coverage lists it as a row no vector reaches. It used to say the vectors had not found an input for the row, as it says of a row the generator missed. It now names what leaves out every input the row asks for — constraint lines, never lines, koyomi's days, the tables above — and says to delete the row or, if such an input can come, to correct them. The row stays an unmet obligation, and the exit code stays 1. Here no more items come back than were ordered:
```
rule return_check v1

enum route = decline | approve | review

inputs
  returned : number  range >=0 <=10
  ordered  : number  range >=0 <=10

constraint returned <= ordered

outputs
  outcome : route

table route_of
policy first
| returned | ordered | -> outcome : route |
| >5       | <=5     | review             |
| -        | >=5     | approve            |
| -        | -       | decline            |
```
0.54.0 said:
```
$ rulec coverage return_check.rule
…
unsatisfied obligations: 1
  [row coverage] table route_of row 1
    No vector produces an input on which this row wins. check named it neither unreachable (E102) nor undecided (W128): the vectors did not find an input for it.
```
This release says:
```
$ rulec coverage return_check.rule
…
unsatisfied obligations: 1
  [row coverage] table route_of row 1
    No input reaches this row: `constraint returned <= ordered` leaves out every input it asks for. Delete this row, or, if such an input can come, correct the `constraint` line.
```
A boundary-pair or shadow-pair obligation on such a row points at the row's row coverage obligation. Where a row above takes ordered >=6 and the row asks for returned >5, the two bounds are one step apart on whole numbers; the walk cannot tell that no input is left, and the old words stay. check and the certificate cannot tell either, and this release leaves them so.
rulec verify says that it is waiting when the adapter does not answer. rulec reads the adapter's answers a line at a time and sets no time limit on any of them, and it used to wait without a word. The commonest cause is an adapter that writes its answers and does not flush them: Python's print writes a line at once to a terminal and keeps it in a buffer when its output is a pipe, so an adapter that answered when it was tried by hand stopped at the handshake under rulec verify, with nothing on the screen and no end. When the handshake or a record has gone unanswered for 30 seconds, rulec now says so on standard error, once in a run, and goes on waiting. With an adapter whose print calls have no flush=True:
```
$ rulec verify parcel.rule --adapter python3 noflush.py
note: the adapter has not answered the handshake for 30 seconds. rulec goes on waiting, and sets no limit. An adapter that is only slow needs nothing done. One that does not flush its output after each line keeps its answers in its buffer, where rulec cannot read them (in Python, `print(..., flush=True)`)
```
An adapter that is only slow is waited for as before, and the run ends as it always did. This one takes 32 seconds over record 3:
```
$ rulec verify parcel.rule --adapter python3 slow.py
note: the adapter has not answered record 3 for 30 seconds. rulec goes on waiting, and sets no limit. An adapter that is only slow needs nothing done. One that does not flush its output after each line keeps its answers in its buffer, where rulec cannot read them (in Python, `print(..., flush=True)`)
Compared 15 / matched 15 (100.000%)
Counterpart: stand-in
No mismatches.
```
The exit status (0 here), the report on standard output and --format json do not change; a script that expects standard error to be empty sees this one line when an answer takes longer than 30 seconds. The time is counted for each answer, not for the run, so a long run with a quick adapter prints no note. There is no time limit and no flag for the 30 seconds: a legacy system that takes minutes over a record is still waited for. crates/rulec/docs/formats.md and the Compare and replay page describe it.

Changes that can make a run that used to pass fail

A row a derive's reach and a constraint leave out together is E102 where 0.54.0 passed it with W128. Rewrite its condition within the values the derive comes to, or delete the row.
rulec verify writes a note on standard error when an answer from the adapter takes longer than 30 seconds. A script that fails on anything on standard error fails there; the exit status and standard output do not change.

ritsu 0.55.0（日本語）

rulec は、導出の届く範囲と constraint が一緒に外す行を、軸の順によらず E102 で止めるようになりました。0.54.0 はそういう行を W128 で通し、届かないことを示せなかったと言っていました。constraint だけが外す行は通り（導出の列があっても W128 は出なくなりました）、その行を挙げる rulec coverage は、ベクタが見つけなかったと言う代わりに、外している constraint を言うようになりました。rulec verify は、アダプタがハンドシェイクか一件の答えを 30 秒返さないとき、標準エラーに一度だけそう書いて、そのまま待ち続けるようになりました。答えが来ない原因の多くは、出力をフラッシュしていないアダプタです。

直したこと（rulec）

導出の届く範囲の外にあり、constraint でも外れる行は、軸の順によらず E102 になります。 E102 の三つ目の形は、行の点を、座標の数の順に軸をたどって歩き、点を外した最初の検査を書き留めます。二つの入力に掛かる constraint の軸が導出の軸より先に来ると、歩きは導出まで来ず、行は届く範囲で止められませんでした。そのうえ W128 が、その行に当たる入力は見つからず、当たらないことも示せなかったと言っていました。今は、導出が加わらずに外れた行を、導出を先に問う歩きでもう一度たどります。上の return_route.rule では、refund は 20 ポンドを超えず、返品の数は注文の数を超えません。0.54.0 は行 3 に警告を出して通していました。

$ rulec check return_route.rule --lang ja
警告[W128]: 行3 に当たる入力を見つけられず、当たらないことも示せませんでした
  --> return_route.rule:23 表 route_of
   |
23 | | >50GBP         | >5       | <=5     | review             |
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 行3: 決められませんでした
   |
 この行は、計算した列 `refund` の値を求めています。その値になる入力を探しましたが見つからず、どの入力も当たらないことも示せませんでした。
 この行に当たる入力が本当にあるか、計算の式と行の条件を見比べてください。あるなら、その入力を例に書くと、この警告は消えます。無いなら、この行を削除してください。削除して完全性の欠落（E101）が出るなら、その組み合わせが起きないことも rulec は示せていないので、行は残してかまいません。

note return_route.rule: 隠れ 2 対（階段 2、同じ答え 0、要確認 0）
ok return_route.rule

この版は止めます。

$ rulec check return_route.rule --lang ja
エラー[E102]: 行3 はどの入力にも当てはまりません
  --> return_route.rule:23 表 route_of
   |
23 | | >50GBP         | >5       | <=5     | review             |
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 行3: ここに到達する入力はありません
16 | derive refund : money[GBP] = paid - fee  range >=-1000GBP <=1000GBP
   |                              ^^^^^^^^^^ 実際に取りうる値は >=-10GBP <=20GBP です
   |
 `refund` が取りうる値は、入力の範囲から計算すると >=-10GBP <=20GBP です。この行の条件に当てはまる値は、その中にありません。
 ヒント: 条件を `refund` の取りうる値の中に書き直すか、この行を削除してください。導出の `range` を広げても、取りうる値は変わりません。

note return_route.rule: 隠れ 2 対（階段 2、同じ答え 0、要確認 0）

constraint だけで外れる行を、W128 が「決められなかった」と言わなくなりました。 導出の列のセルが届く範囲の中にあり、constraint・never・koyomi の日・上流の表のどれかだけで外れる行は、計算した列の無い表で同じように外れる行と同じく、W128 なしで通ります。証明書は 0.54.0 と一字も同じで、その行は前から unreachable に載っています。0.53.0 と 0.54.0 は、この行に W128 を出していました。
どの入力も当たらない行について、rulec coverage が、外しているものを言うようになりました。 constraint だけが外す行は check が通し（constraint が外す行を E102 が止めるのは、導出か define の値も加わるときだけです）、coverage は、どのベクタも当たらない行として挙げます。前は、生成器が見落とした行と同じく「ベクタが入力を見つけなかった」と言っていました。今は、その行が求める入力を全部外しているもの（constraint の行、never の行、koyomi の日、上流の表）を挙げ、行を削除するか、そういう入力が来るならそれを直すよう言います。行は満たされない義務のままで、終了コードも 1 のままです。上の return_check.rule では、返品の数は注文の数を超えません。0.54.0 は、次のように言っていました。
```
$ rulec coverage return_check.rule --lang ja
…
足りないテストケース 1 件:
  [行カバー] 表 route_of 行1
    この行が勝つ入力を、ベクタが一つも作れていません。check は、この行を届かない行（E102）とも、決められない行（W128）とも言っていません。ベクタを作るときに、当たる入力が見つからなかった行です。
```
この版は次のように言います。
```
$ rulec coverage return_check.rule --lang ja
…
足りないテストケース 1 件:
  [行カバー] 表 route_of 行1
    この行に当たる入力はありません。この行が求める入力は、`constraint returned <= ordered` がすべて外しています。この行を削除するか、そういう入力が来るなら `constraint` の行を直してください。
```
同じ行に掛かる境界の両側カバーと隠れ対カバーの欠けは、その行の行カバーの欠けを指します。上の行が ordered >=6 を取り、行が returned >5 を求めるときのように、二つの境が整数で一つずれると、入力が残らないことを見分けられず、前の文のままです。check と証明書も同じく見分けられず、この版では変えていません。
rulec verify は、アダプタが答えないとき、待っていることを言うようになりました。 rulec はアダプタの答えを一行ずつ読み、待つ時間を切りません。これまでは、何も言わずに待ち続けていました。一番多い原因は、答えを書いてもフラッシュしないアダプタです。Python の print は、端末へは一行ごとに書きますが、出力がパイプのときはバッファにためます。手で試すと答えるアダプタが、rulec verify から起こすとハンドシェイクで止まり、画面には何も出ず、終わりもしませんでした。ハンドシェイクか一件の答えが 30 秒届かないと、rulec は標準エラーに一度だけそう書いて、そのまま待ち続けます。print に flush=True を付けていないアダプタでは、次のようになります。
```
$ rulec verify parcel.rule --adapter python3 noflush.py
注記: アダプタがハンドシェイクに 30 秒答えていません。rulec は時間を切らずに待ち続けます。遅いだけなら、このままで構いません。答えを一行ごとにフラッシュしていないと、答えはアダプタのバッファに残り、rulec には届きません（Python なら `print(..., flush=True)`）
```
遅いだけのアダプタは、これまでどおり待ちます。実行の終わり方も変わりません。次は、3 件目に 32 秒かかるアダプタです。
```
$ rulec verify parcel.rule --adapter python3 slow.py
注記: アダプタが 3 件目に 30 秒答えていません。rulec は時間を切らずに待ち続けます。遅いだけなら、このままで構いません。答えを一行ごとにフラッシュしていないと、答えはアダプタのバッファに残り、rulec には届きません（Python なら `print(..., flush=True)`）
照合 15 件 / 一致 15 (100.000%)
相手: stand-in
不一致はありません。
```
終了コード（ここでは 0）、標準出力の報告、--format json は変わりません。標準エラーが空であることを見ているスクリプトは、答えが一つでも 30 秒より長くかかると、この一行を見ます。時間は答え一つごとに数え、実行の全体では数えません。件数が多くても、アダプタが速ければ何も言いません。時間切れは無く、30 秒を変えるフラグもありません。一件に何分もかかる実装も、これまでどおり待ちます。crates/rulec/docs/formats.md と、サイトの「突き合わせと再生」のページに書きました。

前は通っていた実行が落ちうる変更

導出の届く範囲と constraint が一緒に外す行は、0.54.0 では W128 で通りましたが、E102 になります。条件を導出の取りうる値の中に書き直すか、行を削除してください。
rulec verify は、アダプタの答えが 30 秒より長くかかると、標準エラーに注記を一行書きます。 標準エラーに何か出ると失敗にするスクリプトは、そこで落ちます。終了コードと標準出力は変わりません。

Navigation Menu

Repository navigation

ritsu v0.55.0

Choose a tag to compare

Sorry, something went wrong.