{ "_id": "6accad9aa14063b82c3a7c8a", "Package": "leanknit", "Title": "A 'knitr' Engine for Lean 4 Proof Chunks", "Version": "0.0.0.9000", "Authors@R": "c(\nperson(\ngiven = \"Sounkou Mahamane\",\nfamily = \"Toure\",\nemail = \"sounkoutoure@gmail.com\",\nrole = c(\"aut\", \"cre\")\n)\n)", "Description": "Provides a 'knitr' language engine that compiles and\nchecks Lean 4 code chunks against a 'lake' project, capturing\nproof output (including the result of '#print axioms') into\nrendered documents. Modeled on the 'duckknit' engine. Because a\nfailing Lean check fails the render, a generated document\ncannot claim a proof that does not actually check. Also\nprovides install_lean() to provision a Lean toolchain through\n'elan', in the spirit of torch::install_torch().", "License": "GPL (>= 3)", "URL": "https://github.com/sounkou-bioinfo/leanknit", "BugReports": "https://github.com/sounkou-bioinfo/leanknit/issues", "VignetteBuilder": "knitr", "Encoding": "UTF-8", "Roxygen": "list(markdown = TRUE)", "RoxygenNote": "7.3.3", "SystemRequirements": "Lean 4 toolchain (elan/lake) available on PATH", "Repository": "https://sounkou-bioinfo.r-universe.dev", "Date/Publication": "2026-06-10 23:07:02 UTC", "RemoteUrl": "https://github.com/sounkou-bioinfo/leanknit", "RemoteRef": "HEAD", "RemoteSha": "0fc77e836c10df0405b923405672455687091987", "NeedsCompilation": "no", "Packaged": { "Date": "2026-10-12 09:48:40 UTC", "User": "root" }, "Author": "Sounkou Mahamane Toure [aut, cre]", "Maintainer": "Sounkou Mahamane Toure ", "_user": "sounkou-bioinfo", "_type": "src", "_file": "leanknit_0.0.0.9000.tar.gz", "_fileid": "https://r2.ropensci.org/ad0e46a23ca3e28c3a6d01417412368a7e99a154aa078cd300088eec14555d80", "_filesize": 105447, "_sha256": "ad0e46a23ca3e28c3a6d01417412368a7e99a154aa078cd300088eec14555d80", "_expires": "2027-01-20T09:51:20.000Z", "_created": "2026-10-12T09:48:40.000Z", "_published": "2026-10-12T09:51:22.127Z", "_buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877", "_status": "success", "_host": "GitHub-Actions", "_jobs": [ { "job": 114754486879, "time": 101, "config": "linux-devel-x86_64", "r": "4.7.0", "check": "OK", "artifact": "11739665517" }, { "job": 114754486823, "time": 98, "config": "linux-release-x86_64", "r": "4.6.1", "check": "OK", "artifact": "11739092910" }, { "job": 114754487283, "time": 97, "config": "macos-oldrel-arm64", "r": "4.5.3", "check": "OK", "artifact": "11738808700" }, { "job": 114754486884, "time": 111, "config": "macos-release-arm64", "r": "4.6.1", "check": "OK", "artifact": "11739356315" }, { "job": 114753600394, "time": 150, "config": "source", "r": "4.6.1", "check": "OK", "artifact": "11739221193" }, { "job": 114754486790, "time": 87, "config": "wasm-release", "r": "4.6.0", "check": "OK", "artifact": "11738543865" }, { "job": 114754486781, "time": 67, "config": "windows-devel-x86_64", "r": "4.7.0", "check": "OK", "artifact": "11739501054" }, { "job": 114754486808, "time": 65, "config": "windows-oldrel-x86_64", "r": "4.5.3", "check": "OK", "artifact": "11738353838" }, { "job": 114754486829, "time": 70, "config": "windows-release-x86_64", "r": "4.6.1", "check": "OK", "artifact": "11738933456" } ], "_upstream": "https://github.com/sounkou-bioinfo/leanknit", "_commit": { "id": "0fc77e836c10df0405b923405672455687091987", "author": "sounkou-bioinfo ", "committer": "sounkou-bioinfo ", "message": "leanknit: a knitr engine for Lean 4 proof chunks\n\nA knitr language engine that compiles and checks Lean 4 code chunks against\na lake project (lake env lean), accumulating definitions across chunks in a\nsession and showing per-chunk output deltas. A failing Lean check fails the\nrender, so a generated document cannot claim a proof that does not check.\n\n- eng_lean() with eval/error/session/timeout/axioms chunk options\n- install_lean() provisions a toolchain via elan (cf. torch::install_torch)\n- session helpers, find_lake(), leanknit_available(), lean_version(),\n lean_sitrep(), leanknit_example_project()\n- bundled example lake project, tinytest suite, vignette, README from Rmd\n- GitHub Actions R-CMD-check (installs Lean on non-Windows)\n\nModeled on rundel/duckknit.\n", "time": 1781132822 }, "_maintainer": { "name": "Sounkou Mahamane Toure", "email": "sounkoutoure@gmail.com", "login": "sounkou-bioinfo", "mastodon": "@bioinfhotep@genomic.social", "description": "Sequences and Consequences.", "uuid": 56392505 }, "_distro": "resolute", "_registered": true, "_dependencies": [ { "package": "R", "version": ">= 4.1.0", "role": "Depends" }, { "package": "knitr", "role": "Imports" }, { "package": "processx", "role": "Imports" }, { "package": "utils", "role": "Imports" }, { "package": "rmarkdown", "role": "Suggests" }, { "package": "tinytest", "role": "Suggests" } ], "_owner": "sounkou-bioinfo", "_selfowned": true, "_usedby": 0, "_updates": [ { "week": "2026-24", "n": 1 } ], "_tags": [], "_stars": 0, "_contributors": [ { "user": "sounkou-bioinfo", "count": 1, "uuid": 56392505 } ], "_userbio": { "uuid": 56392505, "type": "user", "name": "Sounkou Mahamane Toure", "followers": 57, "description": "Sequences and Consequences." }, "_downloads": { "count": 0, "source": "https://cranlogs.r-pkg.org/downloads/total/last-month/leanknit" }, "_devurl": "https://github.com/sounkou-bioinfo/leanknit", "_searchresults": 4, "_rbuild": "4.6.1", "_assets": [ "extra/citation.cff", "extra/citation.html", "extra/citation.json", "extra/citation.txt", "extra/contents.json", "extra/leanknit.html", "extra/manual.pdf", "extra/NEWS.html", "extra/NEWS.txt", "extra/readme.html", "extra/readme.md" ], "_cranurl": false, "_exports": [ "eng_lean", "find_lake", "install_lean", "lean_sitrep", "lean_version", "leanknit_available", "leanknit_example_project", "leanknit_exec", "leanknit_get_session", "leanknit_list_sessions", "leanknit_start_session" ], "_help": [ { "page": "eng_lean", "title": "The 'lean' knitr engine", "topics": [ "eng_lean" ] }, { "page": "find_lake", "title": "Locate the 'lake' binary", "topics": [ "find_lake" ] }, { "page": "install_lean", "title": "Install the Lean 4 toolchain", "topics": [ "install_lean" ] }, { "page": "lean_sitrep", "title": "Report the leanknit / Lean toolchain situation", "topics": [ "lean_sitrep" ] }, { "page": "lean_version", "title": "Report the installed Lean version", "topics": [ "lean_version" ] }, { "page": "leanknit_available", "title": "Is a usable Lean toolchain available?", "topics": [ "leanknit_available" ] }, { "page": "leanknit_example_project", "title": "A disposable copy of the bundled example lake project", "topics": [ "leanknit_example_project" ] }, { "page": "leanknit_exec", "title": "Compile a Lean source string against a lake project", "topics": [ "leanknit_exec" ] }, { "page": "leanknit_get_session", "title": "Get a leanknit session, creating it if absent", "topics": [ "leanknit_get_session" ] }, { "page": "leanknit_list_sessions", "title": "List active leanknit sessions", "topics": [ "leanknit_list_sessions" ] }, { "page": "leanknit_start_session", "title": "Start (or reset) a leanknit session", "topics": [ "leanknit_start_session" ] } ], "_readme": "https://github.com/sounkou-bioinfo/leanknit/raw/HEAD/README.md", "_rundeps": [ "evaluate", "highr", "knitr", "processx", "ps", "R6", "xfun", "yaml" ], "_vignettes": [ { "source": "leanknit.Rmd", "filename": "leanknit.html", "title": "Checking Lean proofs in knitr documents", "engine": "knitr::rmarkdown", "headings": [ "Running Lean", "Asserting the axiom base", "Expected errors", "Why this matters" ], "created": "2026-06-10 23:07:02", "modified": "2026-06-10 23:07:02", "commits": 1 } ], "_score": 2.6989700043360187, "_indexed": true, "_nocasepkg": "leanknit", "_universes": [ "sounkou-bioinfo" ], "_binaries": [ { "r": "4.7.0", "os": "linux", "version": "0.0.0.9000", "date": "2026-10-12T09:50:27.000Z", "distro": "resolute", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/042cfebd14293e858f2fa27563dd7e5f2c17d3870c82618845e10e6c90a0f85b", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.6.1", "os": "linux", "version": "0.0.0.9000", "date": "2026-10-12T09:50:19.000Z", "distro": "resolute", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/158f4e544ec3a9ac6b11b39914754fdba56797a9e7baf6c33bde8cb8fdcdd1fb", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.5.3", "os": "mac", "version": "0.0.0.9000", "date": "2026-10-12T09:50:22.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/19f9a16779732642f24920b13a73ecd1a73683be8343e38e91a0e4673e89aa52", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.6.1", "os": "mac", "version": "0.0.0.9000", "date": "2026-10-12T09:50:36.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/773bc7ab93ce1f1958d2c096713c6753d32a61996fb117f728ff837342462cda", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.6.0", "os": "wasm", "version": "0.0.0.9000", "date": "2026-10-12T09:50:21.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/1bab7944d46ce12888aa2f6c378ff750c05e495c8fafbc19a70b47f43402b0d8", "status": "success", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.7.0", "os": "win", "version": "0.0.0.9000", "date": "2026-10-12T09:49:43.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/f356dee93e754a24f1aa9be4142ba4efb812cb508e4f2e4b7e7040acc4d4e31f", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.5.3", "os": "win", "version": "0.0.0.9000", "date": "2026-10-12T09:49:46.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/07f0b047057d115adce12638324d21f4636ccd14f889ea72450a8e33b4b4888b", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" }, { "r": "4.6.1", "os": "win", "version": "0.0.0.9000", "date": "2026-10-12T09:49:50.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "https://r2.ropensci.org/5097af55c157baedbd607bfc9dfb4fd4e91f8c60f33f2705937476b7435cae6a", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/38232002877" } ] }