kill imp, mv everythign up a dir

quinn-dougherty · Sep 13, 2024 · 34b2bca · 34b2bca
1 parent 74ed9ef
commit 34b2bca
Show file tree

Hide file tree

Showing 33 changed files with 44 additions and 995 deletions.
diff --git a/llmfv/.envrc → .envrc b/llmfv/.envrc → .envrc
diff --git a/.gitignore b/.gitignore
@@ -1 +1,23 @@
-.vscode/
+# test outputs
+artefacts/hypothesis/*.py
+artefacts/lean/*.lean
+
+# hypotheses
+.hypothesis/
+
+# env
+.env
+
+# python generated files
+__pycache__/
+*.py[oc]
+build/
+dist/
+wheels/
+*.egg-info
+
+
+# venv
+.venv
+
+.ipynb_checkpoints/
diff --git a/llmfv/.python-version → .python-version b/llmfv/.python-version → .python-version
diff --git a/README.md b/README.md
@@ -1,3 +1,24 @@
+# LLM-FV: Toward Scaling Formal Verification Schemes via LLMs
+
+Describe your project here.
+
+
+# Setup
+
+```
+rye sync
+```
+
+Create a `.env` file in `nb/` next to this README with the following:
+```
+ANTHROPIC_API_KEY="YOUR_KEY_HERE"
+```
+
+
+# Basic Run
+You can try to run `python example_agent_run.py`. This will attempt to create tests using claude for the example function in `test/example_func.py`.
+
+Once it completes (successfully), you can re-test the final output with `pytest test/test_example_func.py`. 
 # Formally Verified APPS
 
 ## Conceptually 1

diff --git a/llmfv/artefacts/hypothesis/.gitkeep → artefacts/hypothesis/.gitkeep b/llmfv/artefacts/hypothesis/.gitkeep → artefacts/hypothesis/.gitkeep
diff --git a/llmfv/artefacts/lean/.gitkeep → artefacts/lean/.gitkeep b/llmfv/artefacts/lean/.gitkeep → artefacts/lean/.gitkeep
diff --git a/imp/.gitignore b/imp/.gitignore
diff --git a/imp/Imp.lean b/imp/Imp.lean
diff --git a/imp/Imp/Expr.lean b/imp/Imp/Expr.lean
diff --git a/imp/Imp/Expr/Basic.lean b/imp/Imp/Expr/Basic.lean
diff --git a/imp/Imp/Expr/Delab.lean b/imp/Imp/Expr/Delab.lean
diff --git a/imp/Imp/Expr/Eval.lean b/imp/Imp/Expr/Eval.lean