Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
a08ad60
Add proof extraction functionality and example tests
amit9oct Nov 14, 2025
d24d0a1
Refactor data extraction and parsing: update FileDependencyAnalysis h…
amit9oct Nov 14, 2025
faacec6
Added graph data collection tools.
amit9oct Nov 15, 2025
28d9ca1
Added basic app for data exploration. And mathlib data extraction yaml.
amit9oct Nov 15, 2025
4ef1371
Made tactic parsing more efficient.
amit9oct Nov 17, 2025
3d11814
Enhance proof extraction by allowing optional extra content in extrac…
amit9oct Nov 17, 2025
58810a8
Add Ray initialization utilities and configuration for data extraction
amit9oct Nov 17, 2025
0a4ce24
Add error printing function and improve proof extraction logic
amit9oct Nov 17, 2025
3d5b1e9
Update optional dependencies for app to include Streamlit, Plotly, Ne…
amit9oct Nov 17, 2025
c9975f1
Added batteries
amit9oct Nov 18, 2025
087578d
Uncomment unittest.main() in main function and comment out specific L…
amit9oct Nov 18, 2025
b4de787
Simple refactoring.
amit9oct Nov 19, 2025
925ece1
Add build step for lean4_proj and implement log cleanup in CI workflows
amit9oct Nov 19, 2025
911cbce
Migrated all recent Lean code changes to src/itp_interface/lean
amit9oct Nov 19, 2025
ecef84c
Refactor path handling in tactic parser to use 'lean' directory inste…
amit9oct Nov 19, 2025
30008fb
Enhance CI workflows by adding disk cleanup steps and reorganizing te…
amit9oct Nov 19, 2025
c01990b
Remove disk cleanup step from CI workflows for Python build actions
amit9oct Nov 19, 2025
136201c
Add unit tests for Coq and Lean4 project building and proof execution
amit9oct Nov 19, 2025
6a850cd
Enhance Lean parsing and database error handling
amit9oct Nov 19, 2025
debf4f0
Add scipy as an optional dependency; enhance dependency graph functio…
amit9oct Nov 21, 2025
d037f4c
Enhance Lean4 data extraction with dependency mapping and configurati…
amit9oct Nov 21, 2025
40a2e97
Reduce pool size from 2 to 1 in Lean data extraction and generation c…
amit9oct Nov 21, 2025
7efcab4
Update test data paths to include subdirectory for training data
amit9oct Nov 21, 2025
2dcb084
Refine file filtering in pretty_print_file_contents and update train …
amit9oct Nov 21, 2025
d5b6005
Bump version from 1.2.0 to 1.3.0 in pyproject.toml
amit9oct Nov 21, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 75 additions & 17 deletions .github/workflows/github-build-actions-python314t.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:
- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: true # Ensure submodules are checked out
submodules: false # Ensure submodules are checked out

- name: Install Miniconda
shell: bash
Expand Down Expand Up @@ -84,45 +84,103 @@ jobs:
source $HOME/.elan/env
install-itp-interface

- name: Check and Init opam version
run: |
opam --version
opam init --disable-sandboxing --yes

- name: Install Coq
- name: Build lean4_proj
shell: bash
run: |
opam switch create simple_grp_theory 4.14.2
opam switch simple_grp_theory
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add -y coq-lsp 0.1.8+8.18
source $HOME/.elan/env
cd src/data/test/lean4_proj && lake exe cache get && lake build

- name: List repository files (debug step)
run: find . -type f

- name: Run Simple Env Test
- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Run Simple Env Lean Test
shell: bash
run: |
export PATH="$HOME/miniconda/bin:$PATH"
source $HOME/miniconda/bin/activate py314-ft
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_test.py
python src/test/simple_env_lean_test.py

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Run Data Gen Test
shell: bash
run: |
export PATH="$HOME/miniconda/bin:$PATH"
source $HOME/miniconda/bin/activate py314-ft
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_gen_test.py

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Run Data Extraction Test
shell: bash
run: |
export PATH="$HOME/miniconda/bin:$PATH"
source $HOME/miniconda/bin/activate py314-ft
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_extract_test.py

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Clean up .lake in lean4_proj
shell: bash
run: |
rm -rf src/data/test/lean4_proj/.lake
echo "Cleaned .lake directory in lean4_proj for fresh parallel execution test"

- name: Check and Init opam version
run: |
opam --version
opam init --disable-sandboxing --yes

- name: Install Coq
run: |
opam switch create simple_grp_theory 4.14.2
opam switch simple_grp_theory
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add -y coq-lsp 0.1.8+8.18

- name: Run Simple Env Coq Test
shell: bash
run: |
export PATH="$HOME/miniconda/bin:$PATH"
source $HOME/miniconda/bin/activate py314-ft
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_coq_test.py
79 changes: 60 additions & 19 deletions .github/workflows/github-build-actions.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:
- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: true # Ensure submodules are checked out
submodules: false # Ensure submodules are checked out

- name: Install Python and pip
run: |
Expand Down Expand Up @@ -53,41 +53,52 @@ jobs:
source $HOME/.elan/env
install-itp-interface

- name: Check and Init opam version
run: |
opam --version
opam init --disable-sandboxing --yes

- name: Install Coq
- name: Build lean4_proj
shell: bash
run: |
opam switch create simple_grp_theory 4.14.2
opam switch simple_grp_theory
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add -y coq-lsp 0.1.8+8.18
source $HOME/.elan/env
cd src/data/test/lean4_proj && lake exe cache get && lake build

- name: List repository files (debug step)
run: find . -type f

- name: Run Simple Env Test
- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Run Simple Env Lean Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_test.py

python src/test/simple_env_lean_test.py

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Run Data Gen Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_gen_test.py

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
Expand All @@ -96,11 +107,41 @@ jobs:
- name: Run Data Extraction Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_extract_test.py

- name: Clean up logs
run: |
rm -rf .log
echo "Cleaned .log directory for fresh parallel execution test"

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose
rm -rf /tmp/* --verbose

- name: Clean up .lake in lean4_proj
shell: bash
run: |
rm -rf src/data/test/lean4_proj/.lake
echo "Cleaned .lake directory in lean4_proj for fresh parallel execution test"

- name: Check and Init opam version
run: |
opam --version
opam init --disable-sandboxing --yes

- name: Install Coq
run: |
opam switch create simple_grp_theory 4.14.2
opam switch simple_grp_theory
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add -y coq-lsp 0.1.8+8.18

- name: Run Simple Env Coq Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_coq_test.py
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,6 @@
[submodule "src/itp_interface/tools/repl"]
path = src/itp_interface/tools/repl
url = https://github.com/amit9oct/repl.git
[submodule "src/data/test/batteries"]
path = src/data/test/batteries
url = https://github.com/leanprover-community/batteries.git
9 changes: 6 additions & 3 deletions pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ requires = [
build-backend = "hatchling.build"
[project]
name = "itp_interface"
version = "1.2.0"
version = "1.3.0"
authors = [
{ name="Amitayush Thakur", email="[email protected]" },
]
Expand Down Expand Up @@ -47,8 +47,11 @@ dependencies = [

[project.optional-dependencies]
app = [
"flask>=2.3.0",
"flask-cors>=4.0.0"
"streamlit>=1.28.0",
"scipy>=1.16.0",
"plotly>=5.17.0",
"networkx>=3.1",
"pandas>=2.0.0"
]

[project.urls]
Expand Down
Empty file added src/app/__init__.py
Empty file.
Loading