{ "_id": "6a2a00227b7a29ca60035ecd", "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-06-11 00:21:35 UTC", "User": "root" }, "Author": "Sounkou Mahamane Toure [aut, cre]", "Maintainer": "Sounkou Mahamane Toure ", "MD5sum": "54775e5bc5ff79309de09f474b89a656", "_user": "sounkou-bioinfo", "_type": "src", "_file": "leanknit_0.0.0.9000.tar.gz", "_fileid": "1e1af018e2ff87cf2ed53c4475c476a57abb0c0feff3a461a3b08ec1554b837d", "_filesize": 103694, "_sha256": "1e1af018e2ff87cf2ed53c4475c476a57abb0c0feff3a461a3b08ec1554b837d", "_created": "2026-06-11T00:21:35.000Z", "_published": "2026-06-11T00:24:02.305Z", "_distro": "noble", "_jobs": [ { "job": 80694059195, "time": 97, "config": "linux-devel-x86_64", "r": "4.7.0", "check": "OK", "artifact": "7551759264" }, { "job": 80694059203, "time": 112, "config": "linux-release-x86_64", "r": "4.6.0", "check": "OK", "artifact": "7551762196" }, { "job": 80694059186, "time": 96, "config": "macos-oldrel-arm64", "r": "4.5.3", "check": "OK", "artifact": "7551758744" }, { "job": 80694059193, "time": 94, "config": "macos-release-arm64", "r": "4.6.0", "check": "OK", "artifact": "7551758223" }, { "job": 80693733401, "time": 170, "config": "source", "r": "4.6.0", "check": "OK", "artifact": "7551737503" }, { "job": 80694059165, "time": 113, "config": "wasm-release", "r": "4.6.0", "check": "OK", "artifact": "7551762470" }, { "job": 80694059204, "time": 67, "config": "windows-devel", "r": "4.7.0", "check": "OK", "artifact": "7551752842" }, { "job": 80694059200, "time": 68, "config": "windows-oldrel", "r": "4.5.3", "check": "OK", "artifact": "7551752780" }, { "job": 80694059197, "time": 76, "config": "windows-release", "r": "4.6.0", "check": "OK", "artifact": "7551754636" } ], "_buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759", "_status": "success", "_host": "GitHub-Actions", "_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", "uuid": 56392505 }, "_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", "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": 6, "_rbuild": "4.6.0", "_assets": [ "extra/citation.cff", "extra/citation.html", "extra/citation.json", "extra/citation.txt", "extra/contents.json", "extra/leanknit.html", "extra/NEWS.html", "extra/NEWS.txt", "extra/readme.html", "extra/readme.md", "manual.pdf" ], "_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-06-11T00:23:18.000Z", "distro": "noble", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "9dffd9c022ecda01b5b754953dd925258146bb7a95bde4be37da5f36b3557571", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.6.0", "os": "linux", "version": "0.0.0.9000", "date": "2026-06-11T00:23:31.000Z", "distro": "noble", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "9a38fa5ee72cc0719bb5e161bb754d307ab90bd51c4052fcba44caf7e4848558", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.5.3", "os": "mac", "version": "0.0.0.9000", "date": "2026-06-11T00:23:14.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "d26179e4d5f72ebe0e070ed47f24c4fe07de3a87122a5be5cf6720d1568c3c22", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.6.0", "os": "mac", "version": "0.0.0.9000", "date": "2026-06-11T00:23:17.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "09a9b8772e7c04e5c7e4822fe10446df5823cae41a4adb74401a25b95c7be933", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.6.0", "os": "wasm", "version": "0.0.0.9000", "date": "2026-06-11T00:23:45.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "0a8f3be64ebd347dff0e48dbad6e6612d75b2177e7334accb5bf93647bae235c", "status": "success", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.7.0", "os": "win", "version": "0.0.0.9000", "date": "2026-06-11T00:22:45.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "5ccf5c49f874d38a7e53345dffa299dd3a9e68e1d74414f06bb034b31c4297c3", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.5.3", "os": "win", "version": "0.0.0.9000", "date": "2026-06-11T00:22:43.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "056b46d791dd2184c6cd89fa60d198cee036fcbe8d7bc1581c786e526ad2f6b9", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" }, { "r": "4.6.0", "os": "win", "version": "0.0.0.9000", "date": "2026-06-11T00:22:52.000Z", "commit": "0fc77e836c10df0405b923405672455687091987", "fileid": "fa9b7db32725c3925fe5395e88eb52f1f4121fe5569b9fddec9902151231ee9a", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/sounkou-bioinfo/actions/runs/27315059759" } ] }