ReactorJet/Coq-Iris

---
license: bsd-3-clause
task_categories:
- text-generation
- feature-extraction
language:
- en
tags:
- theorem-proving
- formal-methods
- coq
- separation-logic
- iris
- concurrent-programming
size_categories:
- 10K<n<100K
dataset_info:
features:
- name: fact
dtype: string
- name: type
dtype: string
- name: library
dtype: string
- name: imports
list: string
- name: filename
dtype: string
- name: symbolic_name
dtype: string
- name: docstring
dtype: string
splits:
- name: train
num_bytes: 6186201
num_examples: 10229
download_size: 777517
dataset_size: 6186201
configs:
- config_name: default
data_files:
- split: train
path: data/train-*
---

# Coq-Iris

Structured dataset from Iris, a higher-order concurrent separation logic framework for Coq.

## Dataset Description

- **Source:** [gitlab.mpi-sws.org/iris/iris](https://gitlab.mpi-sws.org/iris/iris)
- **Entries:** 10,229
- **Files processed:** 213
- **License:** BSD-3-Clause

## Schema

| Column | Type | Description |
|--------|------|-------------|
| fact | string | Declaration body |
| type | string | Lemma, Definition, Class, Global, Local, etc. |
| library | string | Module (iris, iris_heap_lang, iris_unstable, etc.) |
| imports | list | Require/Import statements |
| filename | string | Source file path |
| symbolic_name | string | Declaration identifier |

## Statistics

### By Type
| Type | Count |
|------|-------|
| Lemma | 4,569 |
| Global | 3,262 |
| Local | 932 |
| Definition | 707 |
| Class | 205 |
| Ltac | 124 |
| Notation | 96 |
| Program | 81 |
| Inductive | 78 |
| Record | 59 |

### By Library
| Library | Count |
|---------|-------|
| iris | 8,278 |
| tests | 981 |
| iris_heap_lang | 657 |
| iris_unstable | 197 |
| iris_deprecated | 116 |

## About Iris

Iris is a framework for higher-order concurrent separation logic, used for reasoning about concurrent and distributed programs. It is widely used in verified systems software research.

## Use Cases

- Retrieval/RAG for Iris/separation logic
- Learning concurrent verification patterns
- Training embeddings for formal proofs
- Verified systems research

## Related Datasets

- [Coq-HoTT](https://huggingface.co/datasets/phanerozoic/Coq-HoTT)
- [Coq-UniMath](https://huggingface.co/datasets/phanerozoic/Coq-UniMath)
- [Coq-Stdlib](https://huggingface.co/datasets/phanerozoic/Coq-Stdlib)