TheoremSearch/.gitignore at main · uw-math-ai/TheoremSearch · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
.env
.env.local
.env.*.local

# Root-level Python virtualenv / caches
.venv/
venv/
__pycache__/
*.json
*.tex
*.bib
*.sty
*.cls
*.png
*.bbl
*.pdf
*.txt
*.pem
downloaded_sources/
parsed_papers/
!requirements.txt
!pipeline/parse_dependencies/models.json
!pipeline/generate_slogans/models.json
!formalized_graph/projects.json
!pipeline/generate_embeddings/models.json
*pyc
*.csv
*.jsonl

# Allow small slogans and validation set CSVs
!data/stacks_slogans.csv
!data/stacks_validation_set.csv

# Allow MATLAS comparison experiment artifacts
!experiments/matlas-comparison/data/*.json
!experiments/matlas-comparison/results/*.csv
!experiments/matlas-comparison/results/*.json.gz

# Allow failure-modes experiment summary CSV
!experiments/failure-modes/failure_modes.csv

# Allow cycle-consistency pilot artifacts
!experiments/cycle_consistency_pilot/*.csv
!experiments/cycle_consistency_pilot/*.json
experiments/cycle_consistency_pilot/lean_typecheck/.lake/
experiments/cycle_consistency_pilot/lean_typecheck/tmp*.lean

# Allow observable dashboard data + config
!experiments/observable_dashboard/src/data/*.json
!experiments/observable_dashboard/package.json
!experiments/observable_dashboard/package-lock.json
data/sources/
DEBUG/
external/stacks-project/
*.out
*gemini.md

# --- Mathlib Graph / Formalized Graph ---
# Project-specific data and DBs
formalized_graph/data/
!formalized_graph/docs/*.md
formalized_graph/**/*.db
formalized_graph/**/*.ast.json

# Lean 4 Build Artifacts
formalized_graph/**/.lake/
formalized_graph/**/build/
formalized_graph/**/*.olean
formalized_graph/**/*.ilean

# Python / Environment
formalized_graph/**/__pycache__/
formalized_graph/**/.venv/
formalized_graph/**/.mypy_cache/
formalized_graph/**/.ruff_cache/

# --- Formalized Graph V2 ---
formalized_graph_v2/data/
formalized_graph_v2/**/*.db
formalized_graph_v2/**/.lake/
formalized_graph_v2/**/build/
formalized_graph_v2/**/*.olean
formalized_graph_v2/**/*.ilean
formalized_graph_v2/**/__pycache__/
formalized_graph/data/

# External reference clones used for paper-writing comparisons (not vendored).
formalized_graph/docs/paper_writing/leansearch_v2_external/

# Allow curated NL↔FL matching CSVs (small) but exclude the giant raw JSONL.
!experiments/nl_fl_matching/data/*.csv

# Preserve LSv2 replication eval results (per-query JSONLs + summary JSONs).
# These back the leansearch_v2_comparison.md headline numbers.
!experiments/leansearch_v2_replication/data/*.json
!experiments/leansearch_v2_replication/data/*.jsonl

# Preserve dated snapshots of Eric's blueprint_matching q1-q4 runs.
!experiments/blueprint_matching/results/**/*.txt

# Aristotle harness — keep code + per-candidate .lean targets, but JSONL
# trajectories and digest files stay local (they can contain raw
# Aristotle output and Claude prompts).
# Ignore JSONL trajectories (large, may contain raw prompts) but keep the
# digest JSONs and the canonical returned-proof archive — those are the
# experimental record we'd cite. Tarballs are kept too; raw unpacked dirs
# are intermediate and excluded.
experiments/nl_fl_matching/harness/runs/*
!experiments/nl_fl_matching/harness/runs/*.digest.json
!experiments/nl_fl_matching/harness/runs/returned_proofs/
experiments/nl_fl_matching/harness/runs/returned_proofs/_raw/