本报告未能采集到解析后的依赖集合：GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository
原始 JSON 报告 机器可读
{
"data": {
"repo": {
"topics": [
"category-theory",
"homotopy-type-theory",
"proof-assistant",
"haskell"
],
"is_fork": false,
"size_kb": 69463,
"has_wiki": true,
"homepage": "https://rzk-lang.github.io/rzk/",
"languages": {
"CSS": 2061,
"Nix": 14793,
"EBNF": 11649,
"HTML": 409,
"Shell": 1346,
"Haskell": 749874,
"Makefile": 5045,
"JavaScript": 436,
"TypeScript": 31963
},
"pushed_at": "2026-07-24T21:43:59Z",
"created_at": "2020-11-26T10:28:20Z",
"owner_type": "Organization",
"updated_at": "2026-07-24T20:52:21Z",
"description": "An experimental proof assistant based on a type theory for synthetic ∞-categories.",
"is_archived": false,
"is_disabled": false,
"license_spdx": null,
"default_branch": "develop",
"license_spdx_raw": null,
"primary_language": "Haskell",
"significant_languages": [
"Haskell"
]
},
"owner": {
"blog": null,
"name": "rzk proof assistant, satellite tools, and formalisations",
"type": "Organization",
"login": "rzk-lang",
"company": null,
"location": null,
"followers": 39,
"avatar_url": "https://avatars.githubusercontent.com/u/139073969?v=4",
"created_at": "2023-07-09T19:02:35Z",
"is_verified": null,
"public_repos": 15,
"account_age_days": 1115
},
"license": {
"state": "absent",
"spdx_id": null,
"raw_spdx": null,
"file_present": false,
"scorecard_found": false,
"profile_has_license": false
},
"activity": {
"releases": [
{
"tag": "v0.11.1",
"kind": "patch",
"published_at": "2026-07-24T20:59:31Z"
},
{
"tag": "v0.11.0",
"kind": "minor",
"published_at": "2026-07-21T08:28:55Z"
},
{
"tag": "v0.10.0",
"kind": "minor",
"published_at": "2026-07-15T17:43:29Z"
},
{
"tag": "v0.9.2",
"kind": "patch",
"published_at": "2026-07-13T20:47:24Z"
},
{
"tag": "v0.9.1",
"kind": "patch",
"published_at": "2026-06-26T13:52:49Z"
},
{
"tag": "v0.9.0",
"kind": "minor",
"published_at": "2026-06-25T04:48:20Z"
},
{
"tag": "v0.8",
"kind": "other",
"published_at": "2026-06-03T23:07:18Z"
},
{
"tag": "v0.7.7",
"kind": "patch",
"published_at": "2025-11-03T22:22:31Z"
},
{
"tag": "v0.7.6",
"kind": "patch",
"published_at": "2025-08-14T11:40:17Z"
},
{
"tag": "v0.7.5",
"kind": "patch",
"published_at": "2024-08-18T06:40:23Z"
},
{
"tag": "v0.7.4",
"kind": "patch",
"published_at": "2024-04-01T18:26:53Z"
},
{
"tag": "v0.7.3",
"kind": "patch",
"published_at": "2023-12-16T11:06:53Z"
},
{
"tag": "v0.7.2",
"kind": "patch",
"published_at": "2023-12-12T10:37:47Z"
},
{
"tag": "v0.7.1",
"kind": "patch",
"published_at": "2023-12-08T14:07:50Z"
},
{
"tag": "v0.7.0",
"kind": "minor",
"published_at": "2023-12-08T12:57:16Z"
},
{
"tag": "v0.6.7",
"kind": "patch",
"published_at": "2023-10-07T20:08:16Z"
},
{
"tag": "v0.6.6",
"kind": "patch",
"published_at": "2023-10-01T23:46:15Z"
},
{
"tag": "v0.6.5",
"kind": "patch",
"published_at": "2023-10-01T19:21:33Z"
},
{
"tag": "v0.6.4",
"kind": "patch",
"published_at": "2023-09-27T16:27:41Z"
},
{
"tag": "v0.6.3",
"kind": "patch",
"published_at": "2023-09-27T07:21:40Z"
},
{
"tag": "v0.6.2",
"kind": "patch",
"published_at": "2023-09-26T08:11:13Z"
},
{
"tag": "v0.6.1",
"kind": "patch",
"published_at": "2023-09-23T22:58:03Z"
},
{
"tag": "v0.6.0",
"kind": "minor",
"published_at": "2023-09-23T18:02:37Z"
},
{
"tag": "v0.5.7",
"kind": "patch",
"published_at": "2023-09-21T13:51:43Z"
},
{
"tag": "v0.5.6",
"kind": "patch",
"published_at": "2023-09-19T15:30:25Z"
},
{
"tag": "v0.5.5",
"kind": "patch",
"published_at": "2023-09-19T14:13:27Z"
},
{
"tag": "v0.5.4",
"kind": "patch",
"published_at": "2023-08-18T22:16:24Z"
},
{
"tag": "v0.5.3",
"kind": "patch",
"published_at": "2023-07-12T05:27:27Z"
},
{
"tag": "v0.5.2",
"kind": "patch",
"published_at": "2023-07-05T19:46:18Z"
},
{
"tag": "v0.5.1",
"kind": "patch",
"published_at": "2023-06-29T11:37:38Z"
},
{
"tag": "v0.5",
"kind": "other",
"published_at": "2023-06-20T10:39:22Z"
},
{
"tag": "v0.4.1.1",
"kind": "other",
"published_at": "2023-06-15T23:10:55Z"
},
{
"tag": "v0.4.1",
"kind": "patch",
"published_at": "2023-06-15T21:44:50Z"
},
{
"tag": "v0.4.0",
"kind": "minor",
"published_at": "2023-05-18T10:03:12Z"
},
{
"tag": "v0.3.0",
"kind": "minor",
"published_at": "2023-04-28T17:39:40Z"
},
{
"tag": "v0.2.0",
"kind": "minor",
"published_at": "2023-04-20T06:41:07Z"
},
{
"tag": "v0.1.0",
"kind": "minor",
"published_at": "2023-03-25T22:56:21Z"
}
],
"recent_commits": [
{
"oid": "f1d87d1002794c72bf0868dd8cbdb3de2d98bd54",
"body": "Release v0.11.1",
"is_bot": false,
"headline": "Merge pull request #332 from rzk-lang/release-v0.11.1",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T20:52:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "52e5516fd06ee30f7c8ecb84a1e9f4468d243cb5",
"body": "Higher inductive types: a #data constructor may return an identity\ntype, declaring a path, and the generated eliminators gain one method\nand one propositional computation rule per path constructor. The new\nre-ascription clauses let a declaration spell those generated types\nthrough library transport/ap/apd. Modal let mod gains an explicit\nmotive, and the playground deploys are fixed.\n\nVersion bumped in package.yaml, rzk.cabal (regenerated) and\nCITATION.cff; ChangeLog section covers #326-#331.",
"is_bot": false,
"headline": "Release v0.11.1",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T20:32:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e1145ceac07511309367a3a8363665ded23ed96f",
"body": "let mod with explicit motive",
"is_bot": false,
"headline": "Merge pull request #327 from rzk-lang/lishy2-let-mod-motive",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T20:12:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c76eb87f58c3bd653f08d54ae1640c2b3b8b15c1",
"body": "The page was never in docs/docs/ru/rzk.yaml, so neither the typecheck\nnor the formatting lane ever looked at it, even though the English\nversion of the same page was covered by both. Adding it brings the two\ninclude lists to parity for this file.\n\nThe one formatting difference this surfaces is pre-existing: b-dup's\nreturn type is spelled the way the formatter (and the English page)\nalready spell it.",
"is_bot": false,
"headline": "CI: typecheck the Russian modalities reference",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T20:05:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "450dd1b1e1d8d344bdcb4d6e534d38036dd14d19",
"body": "The reference described only the motive-free `let mod`, whose body is\nchecked against the type the whole binding is expected to have. The new\nsubsection gives the three rules the motive adds and the flat induction\nprinciple as the example, since flat has no eta rule and so needs the\nmotive to identi\n[…]\ns previously called `let mod` a \"modal binding\",\nwhich collides with the modal parameter annotations `(x :µ A)`\ndocumented two sections below; it is now a modal let-binding\n(модальное let-связывание).",
"is_bot": false,
"headline": "Docs: document the let-mod motive",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T19:58:42Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "021257ef90b0ab69684e60de5285562150a90c7c",
"body": "All three cases in happy-modal-let-into used a constant motive, which\nthe motive-free `let mod` already handles, so the suite would have\npassed with the motive ignored entirely.\n\nTwo dependent cases are added instead. The flat one is the canonical\ndependent modal elimination: the goal is `C x` while\n[…]\n writes the motive\nas a lambda rather than passing it by name.\n\nThe new ill-modal-let-into-body checks the other direction, that the\nbody really is checked against the motive at the introduction form.",
"is_bot": false,
"headline": "Tests: cover the dependent let-mod motive",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T19:58:42Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "46eb142d93fb1a9cceb61beed93677c0a9d92e6e",
"body": "The motive is an elaboration annotation: it fixes how a `let mod` is\ntyped, but it does not contribute to the term's value. Two stuck\n`let mod`s with the same modalities, value, and body are therefore the\nsame term whichever motive each was written with, so unification no\nlonger compares motives. Th\n[…]\nose (an explicit motive already fixes the type, so that form is\ninferred and unified by the generic branch). This is now stated in a\ncomment rather than left to the reader to infer from the `Nothing`.",
"is_bot": false,
"headline": "Modal: tidy the let-mod motive elaboration",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T18:43:18Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "8ad4190658d26931c9356c5c0a619d7272a3bb80",
"body": null,
"is_bot": false,
"headline": "modal let with explicit motive",
"author_name": "Islam Talipov",
"author_login": "LIshy2",
"committed_at": "2026-07-24T18:11:10Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "849ae18454debe3acd1fd62daf7fced86eb64f87",
"body": "nix: add parser generators to the dev shell (pinned to CI versions)",
"is_bot": false,
"headline": "Merge pull request #330 from rzk-lang/lishy2-nix-parser-tools",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T18:02:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0a9a88cb694d2da0006be769847ff2bd5d7e3b11",
"body": "Refactor: `#data` eliminator construction and the match eliminator choice",
"is_bot": false,
"headline": "Merge pull request #331 from rzk-lang/refactor-data-decl-elaboration",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-24T15:27:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c98ac36046fca7833a999ad1040707af0247d476",
"body": "The eliminator machinery had grown 'withDataDecls' well past what fits\nin one screen: a single 'bindElims' allocated the fresh binders, built\nthe surface types of ind-D and rec-D and the path computation rules, and\nthen elaborated and bound them. The type-building part is pure surface\nsyntax and doe\n[…]\nes the\nElimSpec, and elaborates the results as before.\n\nNo behavioural change; Decl.hs drops about 255 lines and the eliminator\ntype-building is now a pure function. The typecheck suite is unaffected.",
"is_bot": false,
"headline": "Data: split the eliminator construction into Decl.Data",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-23T09:58:50Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "a129c32498d24ecd6bd2d6abc6f18142d8b92844",
"body": null,
"is_bot": false,
"headline": "nix parser update",
"author_name": "Islam Talipov",
"author_login": "LIshy2",
"committed_at": "2026-07-22T13:50:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9a8fe7a5ae9ad0eb0a6da4ec8b18fc03f250bbf6",
"body": "Generating the eliminators indexed two lists positionally with the\npartial (!!): the induction-hypothesis binders and a constructor's field\npatterns. A stale index would surface as the opaque \"Prelude.!!: index\ntoo large\" with no hint of which list or invariant broke.\n\nIntroduce 'nthByConstruction',\n[…]\nt; the third (a hypothesis binder per recursive field) disappears by\nzipping the binders against the recursive-field positions directly, since\nthey are aligned by construction.\n\nNo behavioural change.",
"is_bot": false,
"headline": "Data: replace (!!) in eliminator generation with a labelled helper",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T13:07:34Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "dece98ab360597e48c80a3d2a41557110d896897",
"body": "The elaboration of a match decided between ind-D and rec-D with a\nboolean 'pickRec', computed at the top of checkMatch and consulted again\nsome sixty lines away when building the motive from the goal. The two\nsites had to agree on what the boolean meant, and the later one also\nre-inspected the scrut\n[…]\n from the\nsame parsed decision, so they cannot drift apart, and the variable to\nabstract travels with the choice instead of being recomputed.\n\nNo behavioural change; the typecheck suite is unaffected.",
"is_bot": false,
"headline": "Match: parse the eliminator choice into MatchPlan",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T12:58:08Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "bcce338abc092949096c2b9209218ddf56e478df",
"body": "Path constructors in #data, with propositional computation",
"is_bot": false,
"headline": "Merge pull request #329 from rzk-lang/data-path-constructors",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T12:49:19Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "477b46489e45290bfded89c9f9e73e7b7844f17e",
"body": "Extend the interval fixture with relative function extensionality for\nfunctions out of a shape, which RS17 postulate as an axiom (Axiom\n4.6, weak extension extensionality; sHoTT assumes it as extext). The\nproof is essentially the same as for ordinary function\nextensionality (Lemma 6.3.2 of the HoTT book): the pointwise\nidentification factors through the interval, and ap on seg finishes.\nAlong the way this exercises match on a path constructor under a\ntope context and eta for shape-lambdas.",
"is_bot": false,
"headline": "Tests: relative funext from the interval (RS17, Axiom 4.6)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T08:36:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5278cc24b0fa41f2346a99ac94daf43222654472",
"body": "The interval higher inductive type proves function extensionality: a\npointwise identification makes a map A -> interval -> B whose ends\nare f and g, and ap of its flip on seg identifies f with g. The\nfixture follows Lemma 6.3.2 of the HoTT book and doubles as a record\nthat declaring such a #data cha\n[…]\nry (funext no\nlonger needs to be assumed); it also exercises match on a path\nconstructor inside a let-bound lambda, and the function\neta-equality the final ap application relies on (q left against f).",
"is_bot": false,
"headline": "Tests: funext from the interval (HoTT book, Lemma 6.3.2)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T08:32:26Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "d1dceb33e722e45a7cae79a16de1b580a65e8fc9",
"body": "The #data page gains a path-constructors section (the circle, named\nmethod binders, propositional beta and the generated compute- rules,\nthe endpoint restriction, the propositional truncation) and rewrites\nthe clause section for \"eliminate with\"/\"compute with\", with the full\ncircle example re-ascrib\n[…]\nogy follows Chern's translation of the HoTT book:\nvysshie induktivnye tipy, konstruktory putey/tochek, istochnik i\ntsel' puti; tip-tozhdestvo and opredelitel'nyy stay per the existing\nsite convention.",
"is_bot": false,
"headline": "Docs: path constructors and the re-ascription clauses",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T05:02:26Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "0ab678e2a2a290d73d73b4aca5137b66fef60826",
"body": "Happy: the circle (generated eliminator and compute-rule types spelled\nout, definitional iota on the point constructor, the identity map\nthrough rec and through match), the propositional truncation\n(recursive fields as endpoints, collapse to Unit through Unit's eta),\nthe pushout (endpoints applying \n[…]\nrrier and\nidentity-typed field), compute with on a declaration without path\nconstructors, a kind-mismatched clause, a non-convertible re-ascribed\ncomputation rule, and a match missing its path branch.",
"is_bot": false,
"headline": "Tests: fixtures for path constructors and re-ascription clauses",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T04:54:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "30dfcedf7a94b21328775191bcc59f379fabba90",
"body": "A match without \"into\" whose goal does not mention the scrutinee used\nto elaborate into ind-D with a constant family. For point\nconstructors the two eliminators agree definitionally, but a path\nbranch under the constant ind-D family is checked against a\ntransport that does not reduce, so the natural\n[…]\nrough ind-D. Since applyMethods instantiates the\neliminator's type one branch at a time, a later path branch already\nsees the earlier point branches; no separate declaration-order\nmachinery is needed.",
"is_bot": false,
"headline": "Match: elaborate through rec-D when the goal ignores the scrutinee",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T04:39:36Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "6a2f135bf63783c89d9725c574247597260e13ea",
"body": "The re-ascription clause of #data now covers the generated\ncomputation rules, whose idJ-inlined canonical types are the least\nreadable of the generated entries. Since the clause has not shipped\nin a release, the keyword moves: \"eliminate with <name> : <type>\"\nre-ascribes an eliminator (previously \"e\n[…]\nof entries. Grammar regenerated with the pinned\ntools (zero conflicts); the stolen keywords \"eliminate\", \"with\" and\n\"compute\" have no code occurrences in the corpora (\"with\" appears\nonly in comments).",
"is_bot": false,
"headline": "Data: re-ascription clauses \"eliminate with\" and \"compute with\"",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T04:37:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "dcecdf026efbecc38f596b306d8ede12144fcbaa",
"body": "A constructor whose return type is an identity over the declared type\n(l =_{D ...} r) now declares a path. The boundary is checked by the\nordinary constructor typecheck (endpoints elaborate with the type\nformer and the earlier constructors in scope); on top of that, an\nendpoint must be built from th\n[…]\nmilies, an unannotated identity return type, endpoints that are\nnot constructor-built, and higher paths (an identity carrier or an\nidentity-typed field).\n\nFixtures and docs follow in the next commits.",
"is_bot": false,
"headline": "Data: path constructors with propositional computation",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T04:20:46Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "a2262752553a44564a085c3748a25674cd3fae7b",
"body": "Check the eliminator re-ascription clause of #data",
"is_bot": false,
"headline": "Merge pull request #328 from rzk-lang/data-eliminator-reascription",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-22T03:40:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3a1446a4bf80775aef08791f17e53747d2cc4257",
"body": "Add the clause to the #data syntax sketch and describe it in its own\nsection (definitional equality against the canonical type, values and\ncomputation untouched, the spelling propagates to display), with a\nworked example through an unfolding synonym. Drop the clause from the\ncurrent-restrictions list. Both the English and the Russian pages.",
"is_bot": false,
"headline": "Docs: document the eliminator re-ascription clause",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T18:57:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d00971f7b726940845a8c359914bb94830e0fb67",
"body": "The optional eliminator clause of #data, parsed since the grammar\nlanded, is now checked instead of rejected. The clause names one of\nthe generated eliminators (ind-D or rec-D) and re-ascribes its type\nwith the user's own spelling, which must be definitionally equal to\nthe canonical generated type (\n[…]\neascription (a synonym spelling\nstays interchangeable with the canonical type, computation is\nuntouched) and ill-data-eliminator-{mismatch,unknown,duplicate};\nthe stage-1 rejection fixture is removed.",
"is_bot": false,
"headline": "Typecheck: accept the eliminator re-ascription clause",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T18:31:13Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "ea87bd34023289f18d08b7fe6801e7da0411b09a",
"body": "Playground deploys: mike-safe targets, no force-push, relative base",
"is_bot": false,
"headline": "Merge pull request #326 from rzk-lang/fix-playground-deploy",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T15:43:59Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "352531517d3670add0c776dbff52503d4cc9d03d",
"body": "Three deploy bugs surfaced together after the v0.11.0 release, each\nhiding the others:\n\nThe per-ref targets <ref>/playground and latest/playground sit in\nroot directories that mike owns (it deletes the directories named\nafter the doc version and its aliases on every docs deploy), so the\ntag deploys \n[…]\nies no playground. Publish steps also\nrun on workflow_dispatch now, so a lost deploy can be re-run by hand.\nThe root playground/ content was restored on gh-pages manually\n(commits e20a0e36, 06e1d023).",
"is_bot": false,
"headline": "Playground deploys: mike-safe targets, no force-push, relative base",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T11:31:16Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "ecf7d09c1f4865f266ec90c16a5c8786a332baf0",
"body": "Release v0.11.0",
"is_bot": false,
"headline": "Merge pull request #325 from rzk-lang/release-v0.11.0",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T08:24:07Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c077c5d43db4f058b8622c9b9abf0441bb68af17",
"body": "Bump the version in package.yaml, rzk.cabal and CITATION.cff, and\nwrite the ChangeLog entry: inductive types (#data with recursion and\nindexed families, and match expressions as notation for the generated\ninduction principles, with definitional computation rules), the\nremoval of the syntax forms dep\n[…]\n entry\ndeferred from #304), lattice operations on the interval cubes, the\nmeta-prefix warning, the parse-back guarantee for hole suggestions,\nand the playground rebuilt on the GHC WebAssembly backend.",
"is_bot": false,
"headline": "Release v0.11.0",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T07:52:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "77ec4bc3b5f4afd3da1d238a4c9c6e50132c0737",
"body": "Holes: a unit pattern binds nothing user-visible",
"is_bot": false,
"headline": "Merge pull request #324 from rzk-lang/fix-unit-pattern-holes",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T07:19:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "cfdeddb701c46f2a6de3166098591b3dc16e65ce",
"body": "Reject a binder repeated within one binder group",
"is_bot": false,
"headline": "Merge pull request #323 from rzk-lang/fix-repeated-binders",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-21T07:19:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "62e8dc6fe4f65c3b91bab84d06573b39cc6cc9e6",
"body": "The equation convoy (case-vec) with a wildcard binder as a test case",
"is_bot": false,
"headline": "Merge pull request #322 from rzk-lang/match-eq-convoy-fixture",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-20T20:28:20Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "65441ca2a475489a373b6a8d7dc5dceac580e423",
"body": "Repeating a binder name in one group — a λ's parameter list, a\ndeclaration's parameters, a constructor's fields, or a single pattern\n— was silently accepted, with the later occurrence freshened for\ndisplay. The freshened name (x₁) showed up in hole contexts and\nmessages, but the user never wrote it \n[…]\nion gets a chance to freshen. Shadowing across separate\ngroups — an inner λ reusing an outer parameter's name, which the\ncorpus does routinely — is untouched and keeps its warning. sHoTT\nchecks clean.",
"is_bot": false,
"headline": "Reject a binder repeated within one binder group (#321)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-20T20:15:42Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "53548f55df5aada897d2553c231ed901ac5032c9",
"body": "A λ that matches the unit pattern binds a point of Unit that the user\ncannot name: the pattern introduces no identifiers, and the point is\nspelled \"unit\". The hole context listed it anyway (once per pattern,\ndisplayed as \"unit : Unit\"), and worse, every move mentioning the\npoint was dropped by the p\n[…]\n-trips. The idJ moves of is-set-Unit are back, with unit\nas the endpoints.\n\nChecking is untouched: the binder still enters the context (the point\nis operationally real), only its presentation changes.",
"is_bot": false,
"headline": "Holes: a unit pattern binds nothing user-visible (#320)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-20T20:03:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "07a4c047c275d1c9f94a497097f5a6d3c89cc99a",
"body": "Coq's case_vec, ported through the into motive: the motive generalises\nthe index with a fresh m and returns a function out of the equation\nx = m, so each branch receives the index equation as an explicit\nhypothesis, and the whole match is applied to refl. Also the first\ncoverage for _ as a branch binder: it counts towards the arity and\nbinds nothing. Computation runs through the eliminator and the refl\napplication, pinned by a refl-checked equality.",
"is_bot": false,
"headline": "Fixture: the equation convoy (case-vec) with a wildcard binder",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-20T19:32:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b3ba500c70c9176b089e31ec3e60dc565f539937",
"body": "`match` expressions for inductive types",
"is_bot": false,
"headline": "Merge pull request #319 from rzk-lang/match-sugar",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-20T13:35:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "190423203cada7969615300f68abb8063dfa6d2a",
"body": "A hole with a #data-typed hypothesis in scope now gets the match\nnotation as a candidate, ahead of the ind-/rec- spines: one branch per\nconstructor, each body a hole. Branch binders reuse the constructor's\ndeclared field names, an induction hypothesis is named \"ih\", and both\nare freshened against th\n[…]\nily is skipped (there is no\nbranch syntax for zero constructors), so it keeps only the\neliminators. The node is display-only and never typechecked: its\nannotations are holes, dropped before rendering.",
"is_bot": false,
"headline": "Holes: offer a match over a datatype hypothesis",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T23:24:21Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "95aef5d257b554b6a8e5a1392ae84fe18bbcc59d",
"body": "The convoy pattern is named in 8.4, Dependently Typed Red-Black\nTrees, of Chapter 8, More Dependent Types; the footnote (en/ru) now\nsays so instead of naming only the chapter.",
"is_bot": false,
"headline": "Docs: point the CPDT citation at 8.4 (red-black trees)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T22:14:21Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b3a28d90790388da9d3f0067e411f5c4648e8fd0",
"body": "The elaboration discipline is attributed inline (The view from the\nleft; the Pterodactyl talk) and the convoy pattern gets its source\n(CPDT's MoreDep chapter), en and ru alike. A few overloaded sentences\nare split in passing.",
"is_bot": false,
"headline": "Docs: cite Epigram, Pterodactyl and CPDT on the match page",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T22:10:47Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "630087d650d11a3564276af7515dcbdd5a45e376",
"body": "The safe head on vec A (suc n) computes its motive by a nested match\non the index, so the nil branch is asked for a Unit and the cons\nbranch for an A; the iota-rule runs through the nested-match motive\ndefinitionally (vhead on a concrete vector round-trips by refl in the\nfixture). Added to the reference page (en/ru) and to the indexed\nmatch fixture.",
"is_bot": false,
"headline": "Docs and fixture: an into-motive that uses the index (safe vhead)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T21:46:09Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5c6786f8444ca678b642f812711d9c8d665a5f47",
"body": "Fixtures cover the happy paths (basics with recursion, computation,\nboth motive modes, non-variable scrutinees, branch order, a nested\nmatch; indexed families) and every structured error (missing,\nduplicate and unknown branches, branch arity, a non-#data scrutinee, a\nmotive-less match in inference p\n[…]\nmat-clean) with the branch rule, both motive modes, a worked convoy\nexample (a motive of function type, applied to the hypothesis\nafterwards) and the indexed-family caveat; the #data page links to it.",
"is_bot": false,
"headline": "Tests and docs for match; reduce redexes in hypothesis types",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T20:58:49Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "41b591f2d65c09e54f55888546bc408cbd61be67",
"body": "The branch arrow joins the binary-operator spacing rules and the\nASCII-to-unicode replacements (\"=>\" becomes the canonical arrow). Like\nthe λ-arrow, it ends its line in the canonical layout, so the\nmove-to-next-line rule is suppressed for it. Both canonical match\nlayouts (inline and multi-line) are idempotent; the new formatter test\npins them.",
"is_bot": false,
"headline": "Format: space the match-branch arrow; keep it at line ends",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T20:58:35Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5e9a366cca1af6f6b3d81fa627a4788f7465dd62",
"body": "The reference index treats a branch's constructor name as a use linked\nto the constructor's declaration, and scopes the branch binders over\nthe branch body like λ parameters. Semantic tokens mark the\nconstructor name as an enum member (as constructor uses are) and the\nbinders as parameter declarations.",
"is_bot": false,
"headline": "LSP: index and tokenize match branches",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T19:21:01Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "392aa5545c72af1c6d8ed068a9f93431babd96f5",
"body": "A match elaborates into an application of its datatype's generated\ninduction eliminator: ind-D params motive method1 ... methodk indices\nscrutinee. The scrutinee is inferred and its type's spine must be a\n#data former; branches must be in bijection with the constructors,\neach binding exactly one pat\n[…]\nays a named application.\n\nStructured errors cover the failure modes: scrutinee not of a #data\ntype, missing, duplicate and unknown branches, branch arity mismatch,\nand a match that cannot be inferred.",
"is_bot": false,
"headline": "Typecheck: elaborate match into the induction eliminator",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T19:19:21Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "8142468c7856c505f61efb46ef166574004d4172",
"body": "A match branch binds its constructor's method arguments one binder at\na time: MatchArmF holds one Binder and one real scope, and a branch is\na chain of arms ending in the branch body. This keeps every binder in\nan ordinary scope (holes inside a branch see the branch binders as\nhypotheses), makes α-e\n[…]\n Evaluation\nis untouched: a typed match node never exists (typechecking elaborates\nthe surface node into the generated eliminator's spine), so whnf and\nthe normalisers only gain panicImpossible cases.",
"is_bot": false,
"headline": "Core: represent match branches as arm chains",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T19:09:54Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "52d0efee2315b6e3b1b4da3d94f92b7dfa5d4c7f",
"body": "A match expression eliminates a #data scrutinee by one branch per\nconstructor: match n (zero ⇒ e | suc k ih ⇒ e'), with an optional\nmotive after \"into\". Branches bind exactly one pattern per method\nargument; \"=>\" is the ASCII form of \"⇒\".\n\nThe Match/MatchInto pair follows the TypeId/TypeIdSimple pre\n[…]\n and\nASCII branch forms collapse into the single MatchBranch label by\ndefines, as #define variants do. Parser regenerated with the pinned\ntools (bnfc 2.9.6.3, alex 3.5.4.0, happy 2.2); zero conflicts.",
"is_bot": false,
"headline": "Grammar: add match expressions with branch patterns",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T19:03:49Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "703ca707e9e9150fe453af84369d05390f44446e",
"body": "Holes: one taken-name environment for every move binder",
"is_bot": false,
"headline": "Merge pull request #318 from rzk-lang/display-naming-stage2",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T17:59:31Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "faedad1c532184748ce83d437b195b3668f7cb68",
"body": "CI: cache the wasm toolchain; pin ghc-wasm-meta, add a mirror",
"is_bot": false,
"headline": "Merge pull request #316 from rzk-lang/ci-wasm-toolchain-cache",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T17:33:43Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6d32b830d4b5301f0c7a930cb7836ea0d7ea9910",
"body": "The second stage of the display-naming redesign: every binder a move\nintroduces is named in the move, from one environment, instead of\neach construction site freshening against its own ad-hoc list.\n\nrecordHoleShape derives a single taken-name set per hole: the source\nnamespace (the positionTable key\n[…]\ne set-based variant.\nTests add the promised coproduct-eliminator assertions for the\ndestructuring-pattern repro: rec-coprod and ind-coprod survive the\nparse-back check and no motive binder shadows x₁.",
"is_bot": false,
"headline": "Holes: one taken-name environment for every move binder",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T17:18:31Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "036fd9c262563ff8806af5c76a46d4b89214c4c1",
"body": "Holes: render moves with source names; emit only what parses back",
"is_bot": false,
"headline": "Merge pull request #317 from rzk-lang/display-naming-stage1",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T17:06:52Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1d42dd5d1e9b43c99ffe58418d70ba1f79b12530",
"body": "The first PR run of this lane hung for half an hour inside the\ngitlab.haskell.org download: its anti-bot layer tarpits a connection\nrather than refusing it, and a stalled transfer never triggers\ncurl's --retry or the mirror fallback (it also raced the dispatch\nrun that was still populating the cache\n[…]\n1 kB/s\nfor 30 s) or exceeds two minutes, so a tarpit converts into the\nGitHub-mirror fallback; bound the install step at 30 minutes and the\njob at 60, so nothing holds a runner for the 6-hour default.",
"is_bot": false,
"headline": "CI: fail a stalled wasm toolchain download instead of hanging",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T17:03:44Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "f8475dc97666e6a94a11ec05dd236e9b4351f878",
"body": "The first two stages of the display-naming redesign. A move (a hole\ncandidate or introduction) is inserted as source text, so it has a\nstronger contract than a display: parsing the rendered text at the\nhole must resolve to the very term it renders. Previously this was\napproximated by a string-level \n[…]\ns correctly not offered.\n\nTests: the shadowed-context candidate is offered as b (previously\ndropped), a shadowed-out hypothesis is not offered, and the\nwhole-point pattern rendering still round-trips.",
"is_bot": false,
"headline": "Holes: render moves with source names; emit only what parses back",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T16:43:12Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "c6f6265e7b9df8397db40f9b499eb20716fa5141",
"body": "The wasm lane downloaded the ghc-wasm-meta master tarball on every\nrun and let setup.sh fetch the bindists, so any outage of those hosts\nfailed the lane; only the cabal store was cached.\n\nPin ghc-wasm-meta to a fixed revision (bumped together with FLAVOUR)\nand cache the whole installed toolchain und\n[…]\n: the cache is the fallback for outages.\nOn a miss, the tarball is fetched from gitlab.haskell.org with the\nread-only GitHub mirror as a secondary source.\n\nThe lane stays advisory (continue-on-error).",
"is_bot": false,
"headline": "CI: cache the wasm toolchain; pin ghc-wasm-meta, add a mirror",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T16:27:28Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "c5693127b68f3506bc7692b624e7e0ca646eaced",
"body": "Recursive inductive types and indexed families",
"is_bot": false,
"headline": "Merge pull request #310 from rzk-lang/data-stage2",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T16:23:09Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d0d7dbbd09156cde0b6e9546bcda8da98c55a7c9",
"body": "Warn about unsaturated meta-prefix uses",
"is_bot": false,
"headline": "Merge pull request #312 from rzk-lang/meta-parameter-check",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T16:20:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f14ea3188adc1a57326b8d3172c98f3467564fa2",
"body": "Holes: keep hidden scrutinee names out of the user namespace",
"is_bot": false,
"headline": "Merge pull request #315 from rzk-lang/fix-hidden-scrutinee-names",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T16:19:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "21673f2db92b02884dff43e40eeff5e3422b2022",
"body": "A destructuring λ (\\ (na, nb) → …) binds one hidden scrutinee\nvariable, and the context naming gave it a placeholder from the\ndefault supply: it claimed x₁, so a user-written x₁ bound later\ndisplayed as x₂ — the reported hole context disagreed with the source\n— and, being display-renamed, the user's\n[…]\nndering as the pattern, which is also\nthe pair expression a move may insert.\n\nTests: the repro's hole shows x₁ (not x₂) with its candidate intact,\nand a whole-point pattern use renders as the pattern.",
"is_bot": false,
"headline": "Holes: keep hidden scrutinee names out of the user namespace",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T15:21:50Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "fbae20a404cc3565d7880ddc4e7e2bbda52717ba",
"body": "…4 U-formers)\n\nConflict in allIntroductionsOf: develop added the UniverseT case (type\nformers at a U-goal) where this branch had added the data-former\nfallback (constructor introductions); both are kept, the UniverseT\ncase first. A U-goal thus offers in-scope datatypes hole-saturated,\nand a former-headed goal offers its constructors.",
"is_bot": false,
"headline": "Merge origin/develop (#311 postulate tokens, #313 hole shadowing, #31…",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T11:22:43Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8d8c91c2b9d03704f54c11103aed9f8efb7b0cb2",
"body": "The type theory implemented in rzk separates a meta-theoretic\nparameter layer from the object theory (see section 3.2 of the Rzk\npaper, arXiv:2607.12207, where a statement is abstracted over a\ncontext of schematic cube, tope, and type parameters), but nothing\nenforced responsible use of it. Per decl\n[…]\nmarking,\nwarning-free plumbing, the section recomputation, and both\nnon-default sensitivities; hole-candidate tests cover the suggestion\ngating. The option is documented in the options reference page.",
"is_bot": false,
"headline": "Warn about unsaturated meta-prefix uses",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T11:16:14Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "cf6aa83f412921418a3cbf517cb78435a172e1cb",
"body": "Holes: introduce a U goal by the type formers",
"is_bot": false,
"headline": "Merge pull request #314 from rzk-lang/hole-type-formers",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T10:56:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "415d656b87a58df595e6a71571fcaa9242ae03cf",
"body": "A hole of type U had no introductions. A type is built by a type\nformer, so each is an introduction of a U-goal: a function type\n(? → ?), a Σ-type (Σ (x : ?), ?), an identity type (? =_{?} ?), the\nunit type, and every user-declared datatype in scope, applied to\nholes through its parameter telescope \n[…]\ntroduction's\nbinder; the identity type's endpoints are terms of an as-yet-unknown\ntype, mirroring the tope universe's points. Datatype formers are\nrecognised through the data roles that point at them.",
"is_bot": false,
"headline": "Holes: introduce a U goal by the type formers",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T10:37:49Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "3b49e38f35900a4b14a9fc803ec8174ee95ee5f2",
"body": "Holes: keep offered moves out of shadowing trouble",
"is_bot": false,
"headline": "Merge pull request #313 from rzk-lang/fix-hole-intro-shadowing",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T10:37:18Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "20bca60d5873d9f8ae36f0cdf1754f50aef2e7fb",
"body": "Three fixes to the hole inventory, all about names already in scope\nat the hole.\n\nFirst, a Π-introduction over an anonymous domain (a type written\nB → A → C) left its λ binder unnamed, so the binder was named at\nrender time, bypassing the freshening against the names in scope:\nintroducing twice yiel\n[…]\ntaps on an anonymous\nmulti-argument function type, freshening against telescope and λ\nbinders, the freshened idJ motive at transport's initial hole, and\nthe motive-shadowing fallout at the inner hole.",
"is_bot": false,
"headline": "Holes: keep offered moves out of shadowing trouble",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T10:20:35Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "b03de2b720c876e4d2170c026a9f7d7c19fbbb6b",
"body": "LSP: highlight postulates and assumptions distinctly",
"is_bot": false,
"headline": "Merge pull request #311 from rzk-lang/postulate-highlight",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T07:40:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7e9673aa4752a9e7a3cd9cef4e51c26afacd0f5a",
"body": "A proof that uses an axiom directly in its body is complete only up to\nthat axiom, but nothing in the editor makes this visible: the\nuses-clause is not required for names used explicitly. Mark axiom\nnames with standard semantic token modifiers, both at the declaration\nsite and at every use site, so \n[…]\nognises them there, syntactically. A local\nbinder that shadows an assumption resolves to its own definition\nsite and stays plain.\n\nTests cover declaration-site and use-site tokens for all three\ntiers.",
"is_bot": false,
"headline": "LSP: mark postulates and assumptions as abstract, by severity",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T07:29:03Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "3eddbf082ad1e2a5a23b8b8812271070953cc494",
"body": "No constructors, one index: the index telescope is checked through\nthe type former's own type, and the generated eliminator is ex falso\nthrough the index.",
"is_bot": false,
"headline": "Fixture: an indexed empty family",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:13:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "81ff683eb1f80de9fe038521d3d01eb902a39ace",
"body": "A clean merge: the stage-2 checker work and the LSP overlay touch\ndisjoint regions now that sinkable-decl is the common base. In\npassing, commit the hpack-regenerated extra-source-files for the\nstage-2 fixtures, which had been left in the working tree.",
"is_bot": false,
"headline": "Merge origin/develop (#308 sinkable-decl, #309 use-site tokens)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:03:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c98eef4146f7f8a8d51a8ebbb5e7d5a38352d016",
"body": null,
"is_bot": false,
"headline": "Merge remote-tracking branch 'origin/develop' into data-stage2",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:02:31Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b62c872634642bf275269eed12a4aff26024611a",
"body": "LSP: use-site semantic highlighting for #data products",
"is_bot": false,
"headline": "Merge pull request #309 from rzk-lang/use-site-tokens",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:01:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "97976bbf9965ec49816837433ef4e458c90f3e32",
"body": "Sink declarations and name lists by coercion",
"is_bot": false,
"headline": "Merge pull request #308 from rzk-lang/sinkable-decl",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:01:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "37dfe1738f6dae45e9701e8f45dc618a81278f1a",
"body": "The #data reference page (en/ru) documents index telescopes, the\nspelled-out return types, and the vec eliminator; the restrictions\nlist drops indexed families and gains the cube/shape-index exclusion.\n\nThe external validation the roadmap asks for lands as a fixture: the\nHoTT book §2.13 encode-decod\n[…]\ned by double recursion into U, successor\ninjectivity, and Peano's zero ≠ suc n, where decode-encode\nround-trips by refl on numerals. A copy sits in notes/ as the draft\nfor the actual hottbook chapter.",
"is_bot": false,
"headline": "Docs and validation: indexed families in the reference; HoTT 2.13",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-19T00:01:16Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "aaebdd0832c182b23d2a00f5c47161d55f0a64b2",
"body": "A goal headed by a #data type former is introduced by its\nconstructors applied to holes, and a constructor whose return indices\ncannot meet the goal's (nil against vec A (suc n)) is filtered out by\nthe same structural probe the other candidates use. A hypothesis of a\ndatatype offers the generated el\n[…]\ne constructors and eliminators of a type former are found by their\nroles with a scan over the names in scope; the type former itself\ncarries no role, so this is the lookup direction the roles support.",
"is_bot": false,
"headline": "Hole inventory: constructors and eliminators of #data types",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T23:58:24Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "595b9d5e54d79e79da5e349afa8b23f36c935489",
"body": "The sort of a #data becomes an index telescope: U as before, or a\nPi-telescope of plain types ending in U (named or anonymous binders;\nlater index types may depend on named ones). The type former's type\nspells the sort as written. Constructors of an indexed family must\nspell out their return type, w\n[…]\nter #end; ill-cases for a missing return type, an\nill-typed index term, and a malformed sort (the non-U-sort fixture is\nrepurposed: sorts are supported now, so it asserts the telescope\nshape instead).",
"is_bot": false,
"headline": "Indexed inductive families: sorts, return types, index-aware iota",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T23:44:18Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "9ee2763efc655e3568ea292f997f9e578f81bc5b",
"body": "The last postulated encoding of the dependent-types page becomes a\n#data declaration: the induction principle with its induction\nhypothesis is generated, the propositional computation-rule postulates\ndisappear, and doubling a numeral is checked by refl. The #data\nreference page documents direct recursion and moves the W-type shape\nto the restrictions list.",
"is_bot": false,
"headline": "Docs: natural numbers go native (en/ru)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T23:15:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a32c6e9098a4aaa9ccb113d46599820a950c142a",
"body": "Stage 2, first half. A constructor field whose type is the declared\ntype applied to its parameters is directly recursive: the stage-1\nrejection becomes a classification, and the positivity probe covers\nthe remaining fields only. Any other occurrence of the type in a\nfield is an error, split into two\n[…]\nh ap),\nlist (length into nat), recursion under a section; ill-cases for\nnegative occurrence and function-typed recursive fields. The stage-1\nill-data-recursive fixture is superseded by happy-data-nat.",
"is_bot": false,
"headline": "Recursive inductive types: positivity, induction hypotheses, iota",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T23:11:29Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "8ef102a87b9723008bff3e5890c9b9a2e690bf58",
"body": "With the use-site overlay colouring the annotation in =_{bool}, the\nidentity type's punctuation became visibly inconsistent: =_{ carries\na semantic operator token while } was left to the editor, and themes\nrender the two differently. Since the brace shape-parameters were\nremoved, } occurs only as the closer of =_{ and refl_{, so it can\nsafely take the same operator classification as its opener.",
"is_bot": false,
"headline": "Tokenize: classify } as an operator, matching its opener",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T23:01:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7d6ddaa63a084de7c560c15daa092bda4f6ba8e2",
"body": "An occurrence of a constructor in a term is a plain variable to the\nAST tokenizer, so use-site classification needs name resolution: the\nreference index resolves every occurrence, and the typecheck cache\nknows each declaration's kind. A new overlay colours the uses — a\nconstructor as an enum member,\n[…]\nection with\nthe location at #end time (the last command's line), because toDecl\nignored the entry's recorded location. It now prefers varLocation,\nso DeclView locations point at the declaring command.",
"is_bot": false,
"headline": "LSP: use-site semantic highlighting for #data products",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:50:24Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "bd914ff7c05f8f685d368a99f62adb1f265458ef",
"body": "Decl gets a Sinkable instance, so sinkDecl is Foil.sink (a coercion)\ninstead of a field-by-field record rebuild, and the list sites use\nsinkContainer (sinkDecls) instead of map sinkDecl, which rebuilt the\nspine per element. The same sweep replaces every map Foil.sink over\nname lists (the used-variab\n[…]\ning the\nwarning pragmas for the evidence-only constraint. An upstream note for\nfree-foil (an O(1) sink for SinkableK-style shapes, so downstream\ndoes not hand-roll unsafeCoerce) is drafted separately.",
"is_bot": false,
"headline": "Sink declarations and name lists by coercion",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:41:09Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "001e37c089e50e7f17976ee5b70e1d4df14e207d",
"body": "Add #data: non-recursive inductive types with generated eliminators",
"is_bot": false,
"headline": "Merge pull request #306 from rzk-lang/data-stage1",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:26:55Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5eb32b97907f78180036323516bd9be246911140",
"body": "Playground: modernise the initial example (fix removed syntax)",
"is_bot": false,
"headline": "Merge pull request #307 from rzk-lang/fix-playground-example",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:22:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0e7116a27556b4e985bd07976d2a64f4b67094da",
"body": "The two branches rewrote the same symbol providers, and the features\ninteract: the astral-line maps now thread through the hierarchical\ndocument outline and the kind-aware workspace symbols, so #data\nsymbol ranges come out in UTF-16 units like everything else.",
"is_bot": false,
"headline": "Merge origin/develop (UTF-16 positions, #305) into data-stage1",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:20:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c3b60a053d5b878a9e5044a05558ae3aa3819dc1",
"body": "The initial snippet becomes a plain Rzk file, bundled into the\nplayground through Vite's raw import, so the TypeScript string\nescaping disappears and the file is checkable like any other. The\n\"Check Rzk formalizations\" job typechecks it standalone with the\nfreshly built rzk; it cannot join rzk.yaml, whose modules share one\nscope per run and already define the same names in recId.rzk.md.\nThis is what would have caught the snippet rotting when the\ndeprecated forms were removed.",
"is_bot": false,
"headline": "Playground: keep the initial snippet as a CI-checked Rzk file",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:16:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9d5d59bb5595b47f147f81cd7f7f6ebce755e4bd",
"body": "LSP: convert positions to UTF-16",
"is_bot": false,
"headline": "Merge pull request #305 from rzk-lang/fix-astral-positions",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:15:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "74e7acb80996e2269e1e1885f32895a6d5e41c3c",
"body": "The initial snippet still used the brace shape-parameter syntax\n{t : I | psi t}, which was removed together with the other deprecated\nforms, so the playground opened with code that no longer parses. The\nparameters now use the modern (t : I | psi t) spelling, and a comment\nmentioning the removed 4-argument recOR uses the restriction form.\nThe snippet typechecks against the current parser.",
"is_bot": false,
"headline": "Playground: modernise the initial example (fix removed syntax)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:11:29Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "06a5c877b5c5a39a038f9f36e670b58b0732f93f",
"body": "The MkDocs lane checks formatting after typechecking; the rewritten\ncode blocks needed the formatter's nested-paren spacing and trailing\nnewlines. Applied with rzk format --write; all four pages still\ntypecheck.",
"is_bot": false,
"headline": "Docs: make the rewritten pages rzk-format clean",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T22:01:47Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6f9b0bf77b66a6f06222e1590da6ae8a4c6b4116",
"body": "The diagnoseCheckWarning insertion landed between diagnoseHole's doc\ncomment and the function, orphaning the comment.",
"is_bot": false,
"headline": "Diagnostic: reattach diagnoseHole's haddock to its definition",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T21:42:38Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "dffb33d57a27eeb0611a22cc5c21f9328826e96b",
"body": "A definition whose value is an under-applied eliminator, such as\nnot := rec-bool bool true false, reaches the spine hook as a neutral\napplication rather than a variable: whnf of the head chases the\ndefinition's value and returns the eliminator's own (incomplete)\nspine. The hook now re-collects that \n[…]\nt-not-is-identity while local runs passed. A dedicated fixture pins\nthe case now; rzk.cabal picks up the hpack-expanded extra-source-files\nfor the #data fixtures, which had been stranded the same way.",
"is_bot": false,
"headline": "Fire the iota-rule through a neutral-application head",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T21:42:38Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "0cb97b77737fcd508a68c9e287d34a928c1923b0",
"body": "The dependent-types page declares the empty type, coproducts, and\nbooleans with #data instead of postulating them: the propositional\ncomputation-rule postulates disappear, the recursion principles are\nthe generated rec-D instead of hand-written definitions, and the\nnot-not-is-identity proof, which t\n[…]\nminators and their argument order, the largeness warning, and the\ncurrent restrictions), linked from the commands section of both\nlanguage navs. This is the docs half of the M3 stage-1 exit criterion.",
"is_bot": false,
"headline": "Docs: native #data replaces the postulated encodings (en/ru)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T20:32:25Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "295e8d4ed9926e38b0f23388bf07c8a882a500c2",
"body": "The := rule breaks the line before a definition's body, which is wrong\nfor a short #data (the canonical inline form is `#data bool := false |\ntrue`, design/inductive-types.md §3). Inside a #data the := now stays\nwhere the user put it, so both the inline and the multi-line canonical\nlayouts are idempotent; the paren, spacing, and ASCII-to-unicode rules\napply inside the declaration as everywhere else.",
"is_bot": false,
"headline": "Format: keep both canonical #data layouts",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T20:23:04Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "615eb36cc4d1a785de043f1f9756f7c7147eea90",
"body": "The reference index's global environment did not know #data at all, so\nthe type name, the constructors, and the generated eliminators were\nunresolvable at any use after the declaration (hover, definition, and\nreferences worked only inside the declaration, which has its own local\nenvironment). The en\n[…]\ns children and keeps the generated eliminators\nout (they are not in the source), while workspace symbol search still\nfinds them; symbol kinds mirror the semantic tokens (class, enum\nmember, function).",
"is_bot": false,
"headline": "LSP: resolve #data names at use sites; hierarchical symbols",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T20:16:16Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "81eb43af40bb0aa638e686da23a3b7ca8dde62db",
"body": "Five happy cases (bool with induction and definitional computation,\nparameterised coprod, the empty family, the largeness warning, and\nuniform section closure with the iota-rule firing after #end) and\nseven ill cases (recursion, non-U sort, indexed return type, shape\nfield, eliminator clause, duplic\n[…]\n,\nwith warnings: [] asserting a warning-free run and an absent field\nasserting nothing. The tag is the warning's diagnostic code\n(checkWarningTag), shared with the JSON output so the two cannot\ndrift.",
"is_bot": false,
"headline": "Fixtures for #data stage 1; warnings field in the fixture schema",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T19:57:41Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "cfb9ddbe1eba006e1588ca15c384bda1bfd8afe1",
"body": "The large-inductive-type warning becomes structured: a CheckWarning\nrecorded beside the holes on the (now paired) writer channel and\nfolded into the Checked package, instead of a trace line. The CLI\nprints it in human mode and emits it as a warning-severity diagnostic\nin --json mode; the LSP publish\n[…]\nvention, and\nsafe mode can later escalate the same record into an error.\n\nThe probe censors in the hole inventory discard the whole writer\noutput (const mempty), as before; probes never emit warnings.",
"is_bot": false,
"headline": "Carry checker warnings on the writer channel (large inductive types)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T19:54:20Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "a721b6b1a4599a3d995f68cbba799c4e0c509e7e",
"body": "A #data elaborates to ordinary top-level entries: the type former, one\nentry per constructor, and the generated eliminators ind-D and rec-D\n(HoTT-book argument order: parameters, motive, one method per\nconstructor in declaration order, scrutinee). All are opaque; their\ntypes are built as surface ter\n[…]\nlare their deep assumption dependencies, so\nuniform closure needs no uses clause. In passing, the used/unused\nresult of makeAssumptionExplicit is now a named AssumptionUse instead\nof a commented Bool.",
"is_bot": false,
"headline": "Elaborate #data: opaque entries, generated eliminators, iota-rule",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T19:46:39Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "79255fd9ba4b14bbbc8f69b5eea43dabcc1c8562",
"body": "One new toplevel command, per the M3 proposal (design/inductive-types.md):\n\n #data D uses (...) (params) : Sort := c1 (fields) : T | c2 ...\n eliminator ind-D : T'\n\nThe optional pieces (sort, defaulting to U; the constructor list, omitted\nfor an empty family; a constructor's return type; the elim\n[…]\ne LSP tokenizer highlights the\ndeclaration (type name as class, constructors as enum members), and the\nreference index records the declared names and the identifier occurrences\ninside the declaration.",
"is_bot": false,
"headline": "Grammar: add the #data command for inductive type declarations",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T19:19:26Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "fe0230d7b924e43ff146d1f9286193652bcc6f59",
"body": "LSP positions count UTF-16 code units (the default encoding, and the\nonly one VS Code supports), while alex positions and everything\nderived from them count Unicode code points. The two differ on lines\ncontaining astral-plane characters such as the cube name U+1D540 (the\ndouble-struck I), which take\n[…]\nd definition on a file using the\ndouble-struck interval): token spans come out in UTF-16 units and\nrequests at UTF-16 positions to the right of an astral character\nresolve to the intended identifiers.",
"is_bot": false,
"headline": "LSP: convert positions to UTF-16 at the wire (fix #303)",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T18:38:48Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "d8238b9534c0a9f29570032a9831efe41487fdb5",
"body": "Remove deprecated syntax",
"is_bot": false,
"headline": "Merge pull request #304 from rzk-lang/remove-deprecated-syntax",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T18:15:46Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7092075816471bf5dc62864f3948bc44dff9de77",
"body": "The recId example (en/ru) still showed the 4-argument recOR in its\nprose and in a comment; both now use the restriction-mapping form.\nThe tope-disjunction-elimination reference (en/ru) documented the\n4-argument form as deprecated-but-available; the warning admonition\nbecomes a note stating the form has been removed. A comment in the\nhappy-interval-basics fixture showed the angle-bracket extension type\nand now shows the shaped function type instead.",
"is_bot": false,
"headline": "Docs: modernise mentions of the removed deprecated syntax",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T17:17:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e17e5e39705ce2fe13c43619f517dd6f24e4eae2",
"body": "Remove the seven productions deprecated since v0.5.0: braces around\nparameters ({p : A}, {p : I | phi}, {(p : I) | phi} in Pi-position and\n{p : I | phi} in lambda-position), angle brackets around extension\ntypes (<Phi -> A>, Unicode and ASCII), and the 4-argument recOR. All\nseven are verified extinc\n[…]\nore conversion, and the LSP tokenizer and reference\nindex lose their matching cases. A new ParserSpec pins the removal:\neach removed form is now a parse error, and the modern replacements\nstill parse.",
"is_bot": false,
"headline": "Remove deprecated syntax forms from the grammar",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T17:17:27Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "84c4448ec136b74c3665339e580cfe2fbdf5d482",
"body": "Bring the playground back with a WebAssembly logic core",
"is_bot": false,
"headline": "Merge pull request #302 from rzk-lang/rzk-js-wasm",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T08:41:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5fa442e3642e6f81e05264122a88549a594e0069",
"body": "Replace the retired GHCJS deploy lane with one that builds the playground the\nnew way: install the GHC wasm toolchain (ghc-wasm-meta, as wasm.yml does),\nrun rzk-js/build-wasm.sh to produce the wasm core, build the Vite frontend,\nand publish rzk-playground/dist to GitHub Pages. The deploy targets are\n[…]\natest/playground/` -- and ASSET_URL sets Vite's\nbase so the loader fetches the wasm relative to it. Advisory\n(continue-on-error) like wasm.yml, since it depends on the external\nghc-wasm-meta download.",
"is_bot": false,
"headline": "CI: add the wasm playground build-and-deploy workflow",
"author_name": "Nikolai Kudasov",
"author_login": "fizruk",
"committed_at": "2026-07-18T08:30:33Z",
"body_truncated": true,
"is_coding_agent": false
}
],
"releases_count": 37,
"commits_last_year": 565,
"latest_release_at": "2026-07-24T20:59:31Z",
"latest_release_tag": "v0.11.1",
"releases_from_tags": false,
"days_since_last_push": 4,
"active_weeks_last_year": 20,
"days_since_latest_release": 4,
"mean_days_between_releases": 78.4
},
"community": {
"has_readme": true,
"has_license": false,
"has_description": true,
"has_contributing": false,
"health_percentage": 25,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"ecosystem": {
"packages": []
},
"popularity": {
"forks": 15,
"stars": 285,
"watchers": 12,
"fork_history": {
"days": [
{
"date": "2023-06-15",
"count": 1
},
{
"date": "2024-02-17",
"count": 1
},
{
"date": "2024-03-13",
"count": 1
},
{
"date": "2024-03-18",
"count": 1
},
{
"date": "2024-04-15",
"count": 1
},
{
"date": "2024-05-26",
"count": 1
},
{
"date": "2024-05-29",
"count": 1
},
{
"date": "2024-10-10",
"count": 1
},
{
"date": "2024-11-06",
"count": 1
},
{
"date": "2025-01-02",
"count": 1
},
{
"date": "2025-05-26",
"count": 1
},
{
"date": "2026-01-02",
"count": 1
},
{
"date": "2026-01-04",
"count": 1
},
{
"date": "2026-03-18",
"count": 1
},
{
"date": "2026-04-30",
"count": 1
}
],
"complete": true,
"collected": 15,
"total_forks": 15
},
"star_history": null,
"open_issues_and_prs": 49
},
"ai_readiness": {
"has_nix": true,
"example_dirs": [
"examples"
],
"has_llms_txt": false,
"has_dockerfile": false,
"has_mcp_signal": false,
"bootstrap_files": [
"rzk/Makefile",
"rzk/src/Language/Rzk/Makefile"
],
"api_schema_files": [],
"has_devcontainer": false,
"typecheck_configs": [
"rzk-playground/rzk-lezer/tsconfig.json",
"rzk-playground/tsconfig.json"
],
"toolchain_manifests": [],
"largest_source_bytes": 12931,
"source_files_sampled": 14,
"oversized_source_files": 0,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"dependencies": {
"manifests": [
"docs/requirements.txt",
"rzk-playground/package.json"
],
"advisories": {
"error": null,
"scope": null,
"source": null,
"findings": [],
"collected": false,
"malicious": [],
"truncated": false,
"by_severity": {},
"advisory_count": 0,
"affected_count": 0,
"assessed_count": 0,
"malicious_count": 0,
"assessed_package": null,
"unassessed_count": 0,
"direct_affected_count": 0
},
"ecosystems": [
"npm",
"pypi"
],
"dependencies": [
{
"name": "@bjorn3/browser_wasi_shim",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^0.4.1"
},
{
"name": "@uiw/react-codemirror",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^4.21.18"
},
{
"name": "re-resizable",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^6.9.11"
},
{
"name": "react",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^18.2.0"
},
{
"name": "react-dom",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^18.2.0"
},
{
"name": "react-keybinds",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^1.0.8"
},
{
"name": "react-resizable",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "^3.0.5"
},
{
"name": "rzk-lezer",
"manifest": "rzk-playground/package.json",
"ecosystem": "npm",
"version_constraint": "./rzk-lezer"
},
{
"name": "@lezer/lr",
"manifest": "rzk-playground/rzk-lezer/package.json",
"ecosystem": "npm",
"version_constraint": "^1.4.0"
}
],
"all_dependencies": {
"error": "GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository",
"source": null,
"packages": [],
"collected": false,
"truncated": false,
"total_count": null,
"direct_count": null,
"indirect_count": null
}
},
"maintainership": {
"issues": {
"open_prs": 5,
"merged_prs": 215,
"open_issues": 44,
"closed_ratio": 0.542,
"closed_issues": 52,
"closed_unmerged_prs": 16
},
"bus_factor": 1,
"bot_contributors": 1,
"top_contributors": [
{
"type": "User",
"login": "fizruk",
"commits": 1120,
"avatar_url": "https://avatars.githubusercontent.com/u/686582?v=4"
},
{
"type": "User",
"login": "aabounegm",
"commits": 100,
"avatar_url": "https://avatars.githubusercontent.com/u/11016151?v=4"
},
{
"type": "User",
"login": "LIshy2",
"commits": 80,
"avatar_url": "https://avatars.githubusercontent.com/u/52125920?v=4"
},
{
"type": "User",
"login": "deemp",
"commits": 58,
"avatar_url": "https://avatars.githubusercontent.com/u/48378098?v=4"
},
{
"type": "User",
"login": "geffk2",
"commits": 7,
"avatar_url": "https://avatars.githubusercontent.com/u/29220566?v=4"
},
{
"type": "User",
"login": "alicelogos",
"commits": 2,
"avatar_url": "https://avatars.githubusercontent.com/u/81925537?v=4"
},
{
"type": "User",
"login": "dannypsnl",
"commits": 1,
"avatar_url": "https://avatars.githubusercontent.com/u/22004511?v=4"
},
{
"type": "User",
"login": "ncfavier",
"commits": 1,
"avatar_url": "https://avatars.githubusercontent.com/u/4323933?v=4"
},
{
"type": "User",
"login": "tristan-f-r",
"commits": 1,
"avatar_url": "https://avatars.githubusercontent.com/u/26509014?v=4"
}
],
"contributors_sampled": 9,
"top_contributor_share": 0.818
},
"quality_signals": {
"has_ci": true,
"has_tests": true,
"ci_workflows": [
"bench.yml",
"cabal.yml",
"cache-cleanup.yml",
"ghc.yml",
"parser-drift.yml",
"playground.yml",
"release.yml",
"wasm.yml"
],
"has_docs_dir": true,
"linter_configs": [
".eslintrc.cjs"
],
"has_editorconfig": false,
"has_linter_config": true,
"has_precommit_config": false
},
"security_signals": {
"lockfiles": [
"package-lock.json"
],
"scorecard": {
"checks": [
{
"name": "Binary-Artifacts",
"score": 10,
"reason": "no binaries found in the repo",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#binary-artifacts"
},
{
"name": "Branch-Protection",
"score": null,
"reason": "internal error: error during branchesHandler.setup: internal error: some github tokens can't read classic branch protection rules: https://github.com/ossf/scorecard-action/blob/main/docs/authentication/fine-grained-auth-token.md",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#branch-protection"
},
{
"name": "CI-Tests",
"score": 10,
"reason": "9 out of 9 merged PRs checked by a CI test -- score normalized to 10",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#ci-tests"
},
{
"name": "CII-Best-Practices",
"score": 0,
"reason": "no effort to earn an OpenSSF best practices badge detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#cii-best-practices"
},
{
"name": "Code-Review",
"score": 2,
"reason": "Found 2/9 approved changesets -- score normalized to 2",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#code-review"
},
{
"name": "Contributors",
"score": 10,
"reason": "project has 11 contributing companies or organizations",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#contributors"
},
{
"name": "Dangerous-Workflow",
"score": 10,
"reason": "no dangerous workflow patterns detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dangerous-workflow"
},
{
"name": "Dependency-Update-Tool",
"score": 10,
"reason": "update tool detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dependency-update-tool"
},
{
"name": "Fuzzing",
"score": 0,
"reason": "project is not fuzzed",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#fuzzing"
},
{
"name": "License",
"score": 0,
"reason": "license file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#license"
},
{
"name": "Maintained",
"score": 10,
"reason": "30 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#maintained"
},
{
"name": "Packaging",
"score": null,
"reason": "packaging workflow not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#packaging"
},
{
"name": "Pinned-Dependencies",
"score": 0,
"reason": "dependency not pinned by hash detected -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#pinned-dependencies"
},
{
"name": "SAST",
"score": 0,
"reason": "SAST tool is not run on all commits -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#sast"
},
{
"name": "Security-Policy",
"score": 0,
"reason": "security policy file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#security-policy"
},
{
"name": "Signed-Releases",
"score": 0,
"reason": "Project has not signed or included provenance with any releases.",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#signed-releases"
},
{
"name": "Token-Permissions",
"score": 0,
"reason": "detected GitHub workflow tokens with excessive permissions",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#token-permissions"
},
{
"name": "Vulnerabilities",
"score": 0,
"reason": "20 existing vulnerabilities detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#vulnerabilities"
}
],
"commit": "f1d87d1002794c72bf0868dd8cbdb3de2d98bd54",
"ran_at": "2026-07-28T23:49:57Z",
"aggregate_score": 4.2,
"scorecard_version": "v5.5.0"
},
"has_codeql_workflow": false,
"has_security_policy": false,
"has_dependabot_config": false
},
"contribution_flow": {
"collected": true,
"ci_last_run_at": "2026-07-27T09:29:22Z",
"oldest_open_prs": [
{
"number": 69,
"created_at": "2023-07-12T00:14:12Z",
"last_comment_at": "2023-10-11T10:11:48Z",
"last_comment_author": "fizruk"
},
{
"number": 71,
"created_at": "2023-07-12T15:51:36Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 187,
"created_at": "2024-06-11T12:59:35Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 219,
"created_at": "2026-02-08T21:03:20Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 260,
"created_at": "2026-06-25T09:56:32Z",
"last_comment_at": null,
"last_comment_author": null
}
],
"last_merged_pr_at": "2026-07-24T20:52:16Z",
"ci_last_conclusion": "SUCCESS",
"oldest_open_issues": [
{
"number": 17,
"created_at": "2023-03-19T11:04:49Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 19,
"created_at": "2023-03-19T11:09:14Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 23,
"created_at": "2023-03-22T12:48:17Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 32,
"created_at": "2023-04-20T09:51:32Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 36,
"created_at": "2023-05-11T21:33:42Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 41,
"created_at": "2023-05-19T07:14:57Z",
"last_comment_at": "2023-05-22T23:07:47Z",
"last_comment_author": "aabounegm"
},
{
"number": 42,
"created_at": "2023-05-24T00:02:06Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 45,
"created_at": "2023-05-29T21:49:18Z",
"last_comment_at": "2023-10-06T16:36:11Z",
"last_comment_author": "fizruk"
},
{
"number": 46,
"created_at": "2023-05-29T21:54:33Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 47,
"created_at": "2023-05-29T21:55:05Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 48,
"created_at": "2023-05-29T21:56:35Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 50,
"created_at": "2023-05-31T18:16:34Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 62,
"created_at": "2023-07-04T22:23:24Z",
"last_comment_at": "2023-07-05T09:47:01Z",
"last_comment_author": "fizruk"
},
{
"number": 72,
"created_at": "2023-07-12T20:25:44Z",
"last_comment_at": "2023-07-14T08:04:09Z",
"last_comment_author": "emilyriehl"
},
{
"number": 75,
"created_at": "2023-08-15T16:22:23Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 81,
"created_at": "2023-09-12T20:48:04Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 92,
"created_at": "2023-09-22T20:48:22Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 93,
"created_at": "2023-09-22T20:51:14Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 94,
"created_at": "2023-09-22T20:51:35Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 96,
"created_at": "2023-09-23T06:42:26Z",
"last_comment_at": null,
"last_comment_author": null
}
]
}
},
"config": {
"disabled_metrics": [],
"disabled_categories": [],
"disabled_components": {}
},
"source": {
"url": "https://github.com/rzk-lang/rzk",
"host": "github.com",
"name": "rzk",
"owner": "rzk-lang"
},
"metrics": {
"overall": {
"key": "overall",
"band": "at_risk",
"name": "Overall health",
"note": "High-Risk Jurisdiction Policy applies a 50% multiplier to weighted overall health and gives it an At risk ceiling of 49.",
"notes": [
{
"code": "jurisdiction_overall_adjustment",
"params": {
"cap": 49,
"pct": 50
}
}
],
"value": 30,
"inputs": {
"security": 21,
"vitality": 80,
"community": 41,
"governance": 51,
"engineering": 90,
"high_risk_jurisdiction_cap": 49,
"high_risk_jurisdiction_multiplier": 50,
"weighted_overall_before_jurisdiction": 59,
"overall_after_jurisdiction_multiplier": 30
},
"components": []
},
"categories": [
{
"key": "vitality",
"band": "good",
"name": "Vitality",
"value": 80,
"weight": 0.22,
"metrics": [
{
"key": "development_activity",
"band": "good",
"name": "Development activity",
"note": null,
"notes": [],
"value": 78,
"inputs": {
"commits_last_year": 565,
"human_commit_share": 1,
"days_since_last_push": 4,
"active_weeks_last_year": 20
},
"components": [
{
"key": "push_recency",
"name": "Push recency",
"detail": "last push 4 days ago",
"points": 36,
"status": "met",
"details": [
{
"code": "push_recency",
"params": {
"days": 4
}
}
],
"max_points": 36
},
{
"key": "commit_cadence",
"name": "Commit cadence",
"detail": "20/52 weeks with commits",
"points": 13.8,
"status": "partial",
"details": [
{
"code": "commit_cadence_weeks",
"params": {
"weeks": 20
}
}
],
"max_points": 36
},
{
"key": "commit_volume",
"name": "Commit volume",
"detail": "565 commits in the last year",
"points": 18,
"status": "met",
"details": [
{
"code": "commits_last_year",
"params": {
"count": 565
}
}
],
"max_points": 18
},
{
"key": "openssf_scorecard_maintained",
"name": "OpenSSF Scorecard: Maintained",
"detail": "30 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "release_discipline",
"band": "good",
"name": "Release discipline",
"note": null,
"notes": [],
"value": 83,
"inputs": {
"releases_count": 37,
"latest_release_tag": "v0.11.1",
"releases_from_tags": false,
"days_since_latest_release": 4,
"mean_days_between_releases": 78.4
},
"components": [
{
"key": "ships_releases",
"name": "Ships releases",
"detail": "37 releases published",
"points": 27,
"status": "met",
"details": [
{
"code": "releases_published",
"params": {
"count": 37
}
}
],
"max_points": 27
},
{
"key": "release_recency",
"name": "Release recency",
"detail": "latest release 4 days ago",
"points": 36,
"status": "met",
"details": [
{
"code": "release_recency",
"params": {
"days": 4
}
}
],
"max_points": 36
},
{
"key": "release_cadence",
"name": "Release cadence",
"detail": "a release every ~78.4 days",
"points": 19.8,
"status": "partial",
"details": [
{
"code": "release_cadence",
"params": {
"gap": 78.4
}
}
],
"max_points": 27
},
{
"key": "openssf_scorecard_signed_releases",
"name": "OpenSSF Scorecard: Signed-Releases",
"detail": "Project has not signed or included provenance with any releases.",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "abandonment",
"band": "excellent",
"name": "Abandonment",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"cap": null,
"state": "maintained",
"guards": [],
"signals": [],
"red_flag": false,
"multiplier_pct": 100,
"declared_reason": null,
"unverified_reason": null,
"unanswered_open_prs": null,
"unanswered_open_issues": null,
"days_since_last_merged_pr": null,
"days_since_last_human_commit": 4,
"days_since_last_human_commit_is_floor": false
},
"components": [
{
"key": "project_is_still_maintained",
"name": "Project is still maintained",
"detail": "last human commit 4 days ago",
"points": 100,
"status": "met",
"details": [
{
"code": "abandonment_maintained",
"params": {
"days": 4
}
}
],
"max_points": 100
}
]
}
],
"description": "Is the project alive — is code being written and are releases shipping?"
},
{
"key": "community",
"band": "at_risk",
"name": "Community & Adoption",
"value": 41,
"weight": 0.18,
"metrics": [
{
"key": "popularity",
"band": "moderate",
"name": "Popularity & adoption",
"note": null,
"notes": [],
"value": 55,
"inputs": {
"forks": 15,
"stars": 285,
"watchers": 12,
"growth_state": "unverified",
"growth_factor_pct": 100,
"growth_unverified_reason": "no_history"
},
"components": [
{
"key": "stars",
"name": "Stars",
"detail": "285 stars",
"points": 39.8,
"status": "partial",
"details": [
{
"code": "stars",
"params": {
"count": 285
}
}
],
"max_points": 60
},
{
"key": "forks",
"name": "Forks",
"detail": "15 forks",
"points": 9.6,
"status": "partial",
"details": [
{
"code": "forks",
"params": {
"count": 15
}
}
],
"max_points": 25
},
{
"key": "watchers",
"name": "Watchers",
"detail": "12 watchers",
"points": 5.8,
"status": "partial",
"details": [
{
"code": "watchers",
"params": {
"count": 12
}
}
],
"max_points": 15
}
]
},
{
"key": "community_health",
"band": "critical",
"name": "Community health",
"note": null,
"notes": [],
"value": 25,
"inputs": {
"has_readme": true,
"has_license": false,
"has_contributing": false,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 22.5,
"status": "met",
"details": [],
"max_points": 22.5
},
{
"key": "license",
"name": "License",
"detail": "no license file detected",
"points": 0,
"status": "missed",
"details": [
{
"code": "license_absent",
"params": {}
}
],
"max_points": 22.5
},
{
"key": "contributing_guide",
"name": "CONTRIBUTING guide",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 18
},
{
"key": "code_of_conduct",
"name": "Code of conduct",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 13.5
},
{
"key": "issue_template",
"name": "Issue template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.2
},
{
"key": "pr_template",
"name": "PR template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.3
}
]
}
],
"description": "Does the project have users, downloads, attention, and a welcoming setup for contributors?"
},
{
"key": "governance",
"band": "moderate",
"name": "Sustainability & Governance",
"value": 51,
"weight": 0.24,
"metrics": [
{
"key": "maintainer_resilience",
"band": "at_risk",
"name": "Maintainer resilience (bus factor)",
"note": null,
"notes": [],
"value": 35,
"inputs": {
"bus_factor": 1,
"contributors_sampled": 9,
"top_contributor_share": 0.818
},
"components": [
{
"key": "bus_factor",
"name": "Bus factor",
"detail": "1 contributor(s) cover half of all commits",
"points": 9,
"status": "partial",
"details": [
{
"code": "bus_factor",
"params": {
"count": 1
}
}
],
"max_points": 54
},
{
"key": "commit_distribution",
"name": "Commit distribution",
"detail": "top contributor authored 82% of commits",
"points": 4.1,
"status": "partial",
"details": [
{
"code": "top_contributor_share",
"params": {
"share": 82
}
}
],
"max_points": 22.5
},
{
"key": "contributor_breadth",
"name": "Contributor breadth",
"detail": "9 contributors",
"points": 12.2,
"status": "partial",
"details": [
{
"code": "contributors_sampled",
"params": {
"count": 9
}
}
],
"max_points": 13.5
},
{
"key": "openssf_scorecard_contributors",
"name": "OpenSSF Scorecard: Contributors",
"detail": "project has 11 contributing companies or organizations",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "responsiveness",
"band": "moderate",
"name": "Issue & PR responsiveness",
"note": null,
"notes": [],
"value": 64,
"inputs": {
"merged_prs": 215,
"open_issues": 44,
"closed_issues": 52,
"issue_closed_ratio": 0.542,
"closed_unmerged_prs": 16
},
"components": [
{
"key": "issue_resolution",
"name": "Issue resolution",
"detail": "54% of issues closed",
"points": 25.3,
"status": "partial",
"details": [
{
"code": "issues_closed_share",
"params": {
"share": 54
}
}
],
"max_points": 46.75
},
{
"key": "pr_acceptance",
"name": "PR acceptance",
"detail": "215/231 decided PRs merged",
"points": 35.6,
"status": "partial",
"details": [
{
"code": "decided_prs_merged",
"params": {
"merged": 215,
"decided": 231
}
}
],
"max_points": 38.25
},
{
"key": "openssf_scorecard_code_review",
"name": "OpenSSF Scorecard: Code-Review",
"detail": "Found 2/9 approved changesets -- score normalized to 2",
"points": 3,
"status": "partial",
"details": [],
"max_points": 15
}
]
},
{
"key": "stewardship",
"band": "moderate",
"name": "Ownership & stewardship",
"note": null,
"notes": [],
"value": 56,
"inputs": {
"followers": 39,
"owner_type": "Organization",
"is_verified": null,
"owner_login": "rzk-lang",
"public_repos": 15,
"account_age_days": 1115
},
"components": [
{
"key": "ownership_backing",
"name": "Ownership backing",
"detail": "organization-owned",
"points": 30,
"status": "met",
"details": [
{
"code": "owner_organization",
"params": {}
}
],
"max_points": 30
},
{
"key": "verified_domain",
"name": "Verified domain",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 20
},
{
"key": "owner_reach",
"name": "Owner reach",
"detail": "39 followers of rzk-lang",
"points": 11.5,
"status": "partial",
"details": [
{
"code": "owner_followers",
"params": {
"count": 39,
"login": "rzk-lang"
}
}
],
"max_points": 25
},
{
"key": "track_record",
"name": "Track record",
"detail": "15 public repos, account ~3 yr old",
"points": 14.9,
"status": "partial",
"details": [
{
"code": "public_repos",
"params": {
"count": 15
}
},
{
"code": "account_age_years",
"params": {
"years": 3
}
}
],
"max_points": 25
}
]
}
],
"description": "Will the project survive its people — bus factor, responsiveness, who backs it, and package upkeep?"
},
{
"key": "engineering",
"band": "excellent",
"name": "Engineering Quality",
"value": 90,
"weight": 0.2,
"metrics": [
{
"key": "engineering_practices",
"band": "good",
"name": "Engineering practices",
"note": null,
"notes": [],
"value": 84,
"inputs": {
"has_ci": true,
"has_tests": true,
"has_editorconfig": false,
"has_linter_config": true,
"has_precommit_config": false
},
"components": [
{
"key": "ci_workflows",
"name": "CI workflows",
"detail": "8 workflow(s)",
"points": 24,
"status": "met",
"details": [
{
"code": "ci_workflows",
"params": {
"count": 8
}
}
],
"max_points": 24
},
{
"key": "tests_present",
"name": "Tests present",
"detail": null,
"points": 24,
"status": "met",
"details": [],
"max_points": 24
},
{
"key": "linter_config",
"name": "Linter config",
"detail": ".eslintrc.cjs",
"points": 16,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": ".eslintrc.cjs"
}
}
],
"max_points": 16
},
{
"key": "pre_commit_hooks",
"name": "Pre-commit hooks",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 9.6
},
{
"key": "editorconfig",
"name": ".editorconfig",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.4
},
{
"key": "openssf_scorecard_ci_tests",
"name": "OpenSSF Scorecard: CI-Tests",
"detail": "9 out of 9 merged PRs checked by a CI test -- score normalized to 10",
"points": 20,
"status": "met",
"details": [],
"max_points": 20
}
]
},
{
"key": "documentation",
"band": "excellent",
"name": "Documentation",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"topics": [
"category-theory",
"homotopy-type-theory",
"proof-assistant",
"haskell"
],
"has_wiki": true,
"homepage": "https://rzk-lang.github.io/rzk/",
"has_readme": true,
"has_docs_dir": true,
"has_description": true
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 30,
"status": "met",
"details": [],
"max_points": 30
},
{
"key": "documentation_directory",
"name": "Documentation directory",
"detail": null,
"points": 25,
"status": "met",
"details": [],
"max_points": 25
},
{
"key": "documentation_homepage_site",
"name": "Documentation / homepage site",
"detail": "https://rzk-lang.github.io/rzk/",
"points": 15,
"status": "met",
"details": [],
"max_points": 15
},
{
"key": "repository_description",
"name": "Repository description",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "topics",
"name": "Topics",
"detail": "4 topics",
"points": 10,
"status": "met",
"details": [
{
"code": "topics_count",
"params": {
"count": 4
}
}
],
"max_points": 10
},
{
"key": "wiki",
"name": "Wiki",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
}
],
"description": "Are baseline engineering and documentation practices in place?"
},
{
"key": "security",
"band": "critical",
"name": "Security",
"value": 21,
"weight": 0.16,
"metrics": [
{
"key": "security_posture",
"band": "critical",
"name": "Security posture",
"note": "Excluded from scoring (no data or not applicable): Branch-Protection, Packaging. Remaining weights renormalized. High-Risk Jurisdiction Policy applies a 50% multiplier to Security posture and gives it an At risk ceiling of 49.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"branch_protection",
"packaging"
]
}
},
{
"code": "weights_renormalized",
"params": {}
},
{
"code": "jurisdiction_posture_adjustment",
"params": {
"cap": 49,
"pct": 50
}
}
],
"value": 21,
"inputs": {
"source": "openssf_scorecard",
"checks_evaluated": 16,
"scorecard_version": "v5.5.0",
"checks_inconclusive": 2,
"scorecard_aggregate": 4.2,
"high_risk_jurisdiction_cap": 49,
"high_risk_jurisdiction_multiplier": 50,
"security_posture_after_multiplier": 21,
"security_posture_before_jurisdiction": 42
},
"components": [
{
"key": "binary_artifacts",
"name": "Binary-Artifacts",
"detail": "no binaries found in the repo",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "branch_protection",
"name": "Branch-Protection",
"detail": "internal error: error during branchesHandler.setup: internal error: some github tokens can't read classic branch protection rules: https://github.com/ossf/scorecard-action/blob/main/docs/authentication/fine-grained-auth-token.md",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 7.5
},
{
"key": "ci_tests",
"name": "CI-Tests",
"detail": "9 out of 9 merged PRs checked by a CI test -- score normalized to 10",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "cii_best_practices",
"name": "CII-Best-Practices",
"detail": "no effort to earn an OpenSSF best practices badge detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "code_review",
"name": "Code-Review",
"detail": "Found 2/9 approved changesets -- score normalized to 2",
"points": 1.5,
"status": "partial",
"details": [],
"max_points": 7.5
},
{
"key": "contributors",
"name": "Contributors",
"detail": "project has 11 contributing companies or organizations",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "dangerous_workflow",
"name": "Dangerous-Workflow",
"detail": "no dangerous workflow patterns detected",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "dependency_update_tool",
"name": "Dependency-Update-Tool",
"detail": "update tool detected",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "fuzzing",
"name": "Fuzzing",
"detail": "project is not fuzzed",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "license",
"name": "License",
"detail": "license file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "maintained",
"name": "Maintained",
"detail": "30 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "packaging",
"name": "Packaging",
"detail": "packaging workflow not detected",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 5
},
{
"key": "pinned_dependencies",
"name": "Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "sast",
"name": "SAST",
"detail": "SAST tool is not run on all commits -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "security_policy",
"name": "Security-Policy",
"detail": "security policy file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "signed_releases",
"name": "Signed-Releases",
"detail": "Project has not signed or included provenance with any releases.",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "token_permissions",
"name": "Token-Permissions",
"detail": "detected GitHub workflow tokens with excessive permissions",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "vulnerabilities",
"name": "Vulnerabilities",
"detail": "20 existing vulnerabilities detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
}
]
},
{
"key": "high_risk_jurisdiction_exposure",
"band": "moderate",
"name": "High-Risk Jurisdiction Exposure",
"note": "Only high-confidence self-published location evidence affects this multiplier. Ambiguous matches are review-only; country evidence is not proof of nationality, citizenship, legal registration, malicious intent, or sanctions status.",
"notes": [
{
"code": "jurisdiction_evidence_limits",
"params": {}
}
],
"value": 50,
"inputs": {
"meaning": "self-published location evidence; not nationality or citizenship",
"red_flag": true,
"exposures": [
{
"role": "contributor_organization",
"count": 2,
"country": "Russia"
},
{
"role": "top_contributor",
"count": 1,
"country": "Russia"
}
],
"policy_countries": [
"Russia",
"Iran",
"North Korea"
],
"review_only_matches": 0,
"assessed_self_published_locations": 13
},
"components": [
{
"key": "policy_exposure_multiplier",
"name": "Policy exposure multiplier",
"detail": "Russia: contributor_organization (2); Russia: top_contributor (1)",
"points": 50,
"status": "partial",
"details": [
{
"code": "jurisdiction_exposure",
"params": {
"role": "contributor_organization",
"count": 2,
"country": "Russia"
}
},
{
"code": "jurisdiction_exposure_next",
"params": {
"role": "top_contributor",
"count": 1,
"country": "Russia"
}
}
],
"max_points": 100
}
]
}
],
"description": "Are visible security and supply-chain practices strong, with no malicious dependency and no unresolved high-risk jurisdiction exposure?"
},
{
"key": "ai_readiness",
"band": "moderate",
"name": "AI Readiness",
"value": 62,
"weight": 0,
"metrics": [
{
"key": "ai_agent_context",
"band": "at_risk",
"name": "Agent context & guidance",
"note": null,
"notes": [],
"value": 40,
"inputs": {
"has_llms_txt": false,
"legible_history_share": 0.97,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"components": [
{
"key": "agent_instructions",
"name": "Agent instructions",
"detail": "no CLAUDE.md / AGENTS.md / editor rules",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_instructions",
"params": {}
}
],
"max_points": 45
},
{
"key": "machine_readable_docs_llms_txt",
"name": "Machine-readable docs (llms.txt)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "legible_commit_history",
"name": "Legible commit history",
"detail": "97 of 100 human commits state their intent (structured subject or explanatory body)",
"points": 40,
"status": "met",
"details": [
{
"code": "legible_history",
"params": {
"legible": 97,
"sampled": 100
}
}
],
"max_points": 40
}
]
},
{
"key": "ai_verify_loop",
"band": "good",
"name": "Verify loop (build / test / typecheck)",
"note": null,
"notes": [],
"value": 72,
"inputs": {
"has_nix": true,
"has_tests": true,
"lockfiles": [
"package-lock.json"
],
"has_dockerfile": false,
"typed_language": true,
"bootstrap_files": [
"rzk/Makefile",
"rzk/src/Language/Rzk/Makefile"
],
"has_devcontainer": false,
"has_linter_config": true,
"typecheck_configs": [
"rzk-playground/rzk-lezer/tsconfig.json",
"rzk-playground/tsconfig.json"
],
"agent_commit_share": 0,
"toolchain_manifests": [],
"dependency_bot_commit_share": 0
},
"components": [
{
"key": "one_command_bootstrap",
"name": "One-command bootstrap",
"detail": "rzk/Makefile, rzk/src/Language/Rzk/Makefile",
"points": 18,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "rzk/Makefile, rzk/src/Language/Rzk/Makefile"
}
}
],
"max_points": 18
},
{
"key": "automated_tests",
"name": "Automated tests",
"detail": null,
"points": 22,
"status": "met",
"details": [],
"max_points": 22
},
{
"key": "lint_format_config",
"name": "Lint / format config",
"detail": ".eslintrc.cjs",
"points": 11,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": ".eslintrc.cjs"
}
}
],
"max_points": 11
},
{
"key": "static_type_checking",
"name": "Static type checking",
"detail": "rzk-playground/rzk-lezer/tsconfig.json, rzk-playground/tsconfig.json",
"points": 11,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "rzk-playground/rzk-lezer/tsconfig.json, rzk-playground/tsconfig.json"
}
}
],
"max_points": 11
},
{
"key": "reproducible_environment",
"name": "Reproducible environment",
"detail": "Nix, lockfile",
"points": 10,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "Nix, lockfile"
}
}
],
"max_points": 10
},
{
"key": "demonstrated_agent_practice",
"name": "Demonstrated agent practice",
"detail": "no agent-authored commits among the last 100",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_authored_commits",
"params": {
"sampled": 100
}
}
],
"max_points": 10
},
{
"key": "automated_maintenance",
"name": "Automated maintenance",
"detail": "no automated dependency updates observed",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_dependency_automation",
"params": {}
}
],
"max_points": 8
},
{
"key": "openssf_scorecard_pinned_dependencies",
"name": "OpenSSF Scorecard: Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "ai_code_legibility",
"band": "excellent",
"name": "Code legibility for models",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"primary_language": "Haskell",
"largest_source_bytes": 12931,
"source_files_sampled": 14,
"oversized_source_files": 0
},
"components": [
{
"key": "type_checkable_code",
"name": "Type-checkable code",
"detail": "Haskell (statically typed)",
"points": 45,
"status": "met",
"details": [
{
"code": "statically_typed_language",
"params": {
"language": "Haskell"
}
}
],
"max_points": 45
},
{
"key": "manageable_file_sizes",
"name": "Manageable file sizes",
"detail": "0/14 source files over 60KB",
"points": 55,
"status": "met",
"details": [
{
"code": "oversized_source_files",
"params": {
"kb": 60,
"sampled": 14,
"oversized": 0
}
}
],
"max_points": 55
}
]
},
{
"key": "ai_interfaces",
"band": "at_risk",
"name": "Machine-readable interfaces",
"note": null,
"notes": [],
"value": 40,
"inputs": {
"example_dirs": [
"examples"
],
"has_mcp_signal": false,
"api_schema_files": []
},
"components": [
{
"key": "api_schema_openapi_graphql_proto",
"name": "API schema (OpenAPI/GraphQL/proto)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 40
},
{
"key": "mcp_server",
"name": "MCP server",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 20
},
{
"key": "runnable_examples",
"name": "Runnable examples",
"detail": "examples",
"points": 40,
"status": "met",
"details": [
{
"code": "file_list",
"params": {
"files": "examples"
}
}
],
"max_points": 40
}
]
}
],
"description": "How well is the repo equipped to be developed and maintained with AI coding agents? An independent, experimental badge — weight 0.0, so it is surfaced on its own and does not affect the overall health score."
}
],
"metrics_version": "1.13.0"
},
"warnings": [
"Star history unavailable: GitHub GraphQL error: Resource not accessible by personal access token",
"Could not fetch npm package 'rzk-lezer' from its registry",
"GitHub dependency-graph SBOM unavailable (404); the dependency graph may be disabled for this repository"
],
"report_type": "repository",
"generated_at": "2026-07-28T23:50:16.644256Z",
"schema_version": "0.27.0",
"badge_url": "https://raw.githubusercontent.com/inspect-software/badges/main/v1/r/rzk-lang/rzk.svg",
"full_name": "rzk-lang/rzk",
"license_state": "absent",
"license_spdx": null
}
