remote/open-slopware
1
0
Fork 0
mirror of https://codeberg.org/small-hack/open-slopware.git synced 2026-09-28 04:44:38 +02:00
Code Issues Projects Releases Packages Wiki Activity

Add proof assistants (#856)

Browse source 
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 <ethical-foss-admin@noreply.codeberg.org>
This commit is contained in:
Naïm Camille Favier 2026-07-01 19:06:24 +02:00 • committed by Ethical FOSS admin
commit 1c2640a6ba
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
README.md
View file

@ -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)) <br /> [![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) |