From 1c2640a6ba74d6f888dd970c84d86d6009a8ae7b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Camille=20Favier?= Date: Wed, 1 Jul 2026 19:06:24 +0200 Subject: [PATCH] Add proof assistants (#856) Adds Agda (with alternative Mikan), Lean, and Rocq to the list. [Rendered](https://codeberg.org/ncf/open-slopware/src/commit/proof-assistants/README.md#proof-assistants) Reviewed-on: https://codeberg.org/ethical-foss/open-slopware/pulls/856 Reviewed-by: Ethical FOSS admin --- README.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 6f53bf6..dd6c9ba 100644 --- a/README.md +++ b/README.md @@ -152,6 +152,7 @@ Any other questions? Please check out our [FAQ](./FAQ.md), and if your question * [Alternative GUI crates](#alternative-gui-crates) * [Alternative TUI crates](#alternative-tui-crates) * [Scala](#scala) + * [Proof Assistants](#proof-assistants) * [Remote Desktop](#remote-desktop) * [Reverse Engineering and Debugging](#reverse-engineering-and-debugging) * [Runtime Version Managers](#runtime-version-managers) @@ -830,7 +831,7 @@ This is a section for repos that are similar to this one either because they are ### Continuous Integration Alternatives -- [Forgejo Actions](https://forgejo.org/docs/latest/user/actions/overview/) +- [Forgejo Actions](https://forgejo.org/docs/latest/user/actions/overview/) ## Cryptography @@ -1589,6 +1590,14 @@ Note that Scala (except version 2 and up to 3.3.7 LTS) is itself tainted; see [t |---|:---:|---|---| | [tapir](https://tapir.softwaremill.com/) | [`v1.12.6`](https://github.com/softwaremill/tapir/releases/tag/v1.12.6) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/softwaremill/tapir/commit/19ba37dd80838cb7a8c38e00262c18b014cd8ef7), [2](https://github.com/softwaremill/tapir/commit/3d15edbd6d45b27568244327a52512502d85b8be)) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | +## Proof Assistants + +| Name | Last Untainted Version or Commit ID | Tags and Evidence | Alternative(s) | +|---|:---:|---|---| +| [Agda](https://github.com/agda/agda) | [`2.8.0`](https://github.com/agda/agda/releases/tag/v2.8.0) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/agda/agda/pull/8507)) | [Mikan](https://codeberg.org/1lab/mikan) | +| [Lean](https://leanprover-community.github.io/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/leanprover/lean4/tree/master/.claude), [2](https://github.com/leanprover/lean4/pull/12776))
[![AI sponsored](./badges/ai-sponsored-blue.svg)](#sponsored-by-ai) ([1](https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research), [2](https://lean-lang.org/fro/about/)) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | +| [Rocq](https://rocq-prover.org/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/rocq-prover/rocq/commit/3006a6d65)) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | + ## Remote Desktop | Name | Last Untainted Version or Commit ID | Tags and Evidence | Alternative(s) |