Jira sync

jira.yml

611 workflow runs

Std.Http: a valid UPDATEREDIRECTREF request gets 400 when a read ends inside the method name
completed successfully:
Jira sync#1401:Issue#16111closedbyalgebraic-dev
Nov 9, 20266s
Std.Http server: answer a syntactically valid but unrecognized method with 501, not 400?
completed successfully:
Jira sync#1400:Issue#16335closedbyalgebraic-dev
Nov 9, 20267s
Std.Http server accepts Transfer-Encoding: gzip, chunked requests and passes the coded body on
completed successfully:
Jira sync#1399:Issue#16334closedbyalgebraic-dev
Nov 9, 20266s
Std.Http server answers HTTP/1.0 requests with an HTTP/1.0 status-line
completed successfully:
Jira sync#1398:Issue#16332closedbyalgebraic-dev
Nov 9, 20265s
Std.Http server: error responses the H1 machine writes (400, 414, 431, 505) have no body
completed successfully:
Jira sync#1397:Issue#16333closedbyalgebraic-dev
Nov 9, 20267s
Std.Http server writes the handler's content in a 205 Reset Content response
completed successfully:
Jira sync#1396:Issue#16331closedbyalgebraic-dev
Nov 9, 20266s
Std.Http server: 4xx responses generated by the H1 machine carry no Date header
completed successfully:
Jira sync#1395:Issue#16330closedbyalgebraic-dev
Nov 9, 20268s
IO.Process.output hangs on large input strings
completed successfully:
Jira sync#1394:Issue#14000closedbyTwoFX
Nov 9, 20269s
IO.Process.run throws an error on non-UTF8 stdout or stderr.
completed successfully:
Jira sync#1393:Issue#14003closedbyTwoFX
Nov 9, 20267s
IO.Process.output can throw an error while the underlying spawned process is still running
completed successfully:
Jira sync#1392:Issue#14001closedbyTwoFX
Nov 9, 20268s
Std.Http: a URI with no authority and a path starting with // prints as https://a, which parses back with host a
completed successfully:
Jira sync#1391:Issue#16268closedbyalgebraic-dev
Nov 9, 202645s
Std.Http: decideRedirect resolves Location: / to the current request path instead of /
completed successfully:
Jira sync#1390:Issue#16036closedbyalgebraic-dev
Nov 9, 202645s
Std.Http: query values containing = are rejected (?a=b=c, base64 padding)
completed successfully:
Jira sync#1389:Issue#16021closedbyalgebraic-dev
Nov 9, 202641s
decide on bounded quantifiers reaches maxRecDepth sooner since #15371
completed successfully:
Jira sync#1388:Issue#16108closedbynomeata
Nov 9, 20266s
simp [h] cannot use h : ¬ v = 0 on BitVec, because the goal's 0 becomes 0#w before h is tried
completed successfully:
Jira sync#1387:Issue#16260closedbybenaadams
Nov 9, 20267s
WorkspaceEdits fail when targeting a URI without a version
completed successfully:
Jira sync#1386:Issue#16236closedbymhuisi
Nov 9, 20265s
grind_linarith: internal error "linarith term has not been internalized" on negative Int8..Int64 literals (regression after 4.36)
completed successfully:
Jira sync#1385:Issue#16286closedbyleodemoura
Nov 7, 20265s
lia proof using Nat.Simproc.add_le_add_le takes kernel time linear in a numeric literal
completed successfully:
Jira sync#1384:Issue#16311closedbyleodemoura
Nov 7, 20268s
Array.ugetBorrowed's _boxed wrapper returns its element after releasing the array
completed successfully:
Jira sync#1383:Issue#16329closedbyhargoniX
Nov 7, 20267s
Segfault on the second withImportModules in one process: findOLean's root cache keeps a Name from a freed .olean region (regression in 4.36.0-rc1)
completed successfully:
Jira sync#1382:Issue#16267closedbyKha
Nov 6, 20267s
Std.Http: a request with an overlong request-target gets 400 or 414 depending on where a read ends
completed successfully:
Jira sync#1381:Issue#16035closedbyalgebraic-dev
Nov 6, 20266s
grind_linarith: internal error "structure is not a preorder" on < / ≤ over Fin n and BitVec w
completed successfully:
Jira sync#1380:Issue#16287closedbyleodemoura
Nov 5, 20268s
lia/grind: kernel rejects the proof of x % 3 ≤ 2 * x % 3 → 4 * x % 3 ≤ 2 * x % 3 (eq_of_dvd_ediv type mismatch)
completed successfully:
Jira sync#1379:Issue#16228closedbyleodemoura
Nov 5, 20267s
contradiction fails with the internal error "mkNoConfusion: No manifest constructors" on h : 0 + 0 = 1 (regression since 4.22)
completed successfully:
Jira sync#1378:Issue#16285closedbyleodemoura
Nov 5, 20267s
proj_idx truncation: size_t → unsigned
completed successfully:
Jira sync#1377:Issue#12746closedbynomeata
Nov 5, 20269s

Navigation Menu

Jira sync

611 workflow runs

`Std.Http`: a valid `UPDATEREDIRECTREF` request gets 400 when a read ends inside the method name

Std.Http server: answer a syntactically valid but unrecognized method with 501, not 400?

Std.Http server accepts Transfer-Encoding: gzip, chunked requests and passes the coded body on

Std.Http server answers HTTP/1.0 requests with an HTTP/1.0 status-line

Std.Http server: error responses the H1 machine writes (400, 414, 431, 505) have no body

Std.Http server writes the handler's content in a 205 Reset Content response

Std.Http server: 4xx responses generated by the H1 machine carry no Date header

IO.Process.output hangs on large input strings

IO.Process.run throws an error on non-UTF8 stdout or stderr.

IO.Process.output can throw an error while the underlying spawned process is still running

Std.Http: a URI with no authority and a path starting with `//` prints as `https://a`, which parses back with host `a`

Std.Http: `decideRedirect` resolves `Location: /` to the current request path instead of `/`

Std.Http: query values containing `=` are rejected (`?a=b=c`, base64 padding)

`decide` on bounded quantifiers reaches `maxRecDepth` sooner since #15371

`simp [h]` cannot use `h : ¬ v = 0` on `BitVec`, because the goal's `0` becomes `0#w` before `h` is tried

`WorkspaceEdit`s fail when targeting a URI without a version

`grind_linarith`: internal error "linarith term has not been internalized" on negative `Int8`..`Int64` literals (regression after 4.36)

`lia` proof using Nat.Simproc.add_le_add_le takes kernel time linear in a numeric literal

`Array.ugetBorrowed`'s `_boxed` wrapper returns its element after releasing the array

Segfault on the second `withImportModules` in one process: `findOLean`'s root cache keeps a `Name` from a freed `.olean` region (regression in 4.36.0-rc1)

Std.Http: a request with an overlong request-target gets 400 or 414 depending on where a read ends

`grind_linarith`: internal error "structure is not a preorder" on `<` / `≤` over `Fin n` and `BitVec w`

`lia`/`grind`: kernel rejects the proof of `x % 3 ≤ 2 * x % 3 → 4 * x % 3 ≤ 2 * x % 3` (`eq_of_dvd_ediv` type mismatch)

`contradiction` fails with the internal error "mkNoConfusion: No manifest constructors" on `h : 0 + 0 = 1` (regression since 4.22)

`proj_idx` truncation: `size_t` → `unsigned`

Workflow runs for Jira sync

611 workflow runs