diff --git a/README.md b/.github/README.md similarity index 89% rename from README.md rename to .github/README.md index 8055699..63e6ccf 100644 --- a/README.md +++ b/.github/README.md @@ -19,8 +19,9 @@ The entire proof is formalized in Coq, providing a machine-checked verification ## Repository Structure -- `The Formalized UOR H1 HPO Candidate and Proofs.tex`: The main LaTeX document containing the narrative of the proof. -- `appendix.tex`: An appendix with additional details and proofs. +- `UOR-H1-HPO-Candidate.tex`: The main LaTeX document containing the narrative of the proof. +- `Appendix-1-Structures.tex`: An appendix with additional details and proofs. +- `Appendix-2-Principles.tex`: An appendix with the complete UOR construction of the UOR H1 HPO Candidate. - `coq/`: The directory containing the Coq formalization of the proof. ## Usage diff --git a/.github/package.json b/.github/package.json new file mode 100644 index 0000000..a164f84 --- /dev/null +++ b/.github/package.json @@ -0,0 +1,15 @@ +{ + "name": "latex-project", + "version": "1.0.0", + "description": "A project for compiling and publishing LaTeX documents as GitHub packages.", + "scripts": { + "build": "pdflatex src/main.tex && pdflatex src/appendix.tex", + "publish": "npm run build && npm publish" + }, + "dependencies": { + "latex": "^1.0.0" + }, + "devDependencies": { + "gh-pages": "^3.2.3" + } +} \ No newline at end of file diff --git a/.github/workflows/latex.yml b/.github/workflows/latex.yml new file mode 100644 index 0000000..3c7b6c0 --- /dev/null +++ b/.github/workflows/latex.yml @@ -0,0 +1,55 @@ +name: Compile and Publish LaTeX + +on: + push: + branches: + - main + pull_request: + branches: + - main + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v2 + + - name: Set up LaTeX + run: sudo apt-get install texlive-full + + - name: Create output directory + run: mkdir -p pdf_output + + - name: Compile LaTeX documents + run: | + # Find all .tex files and compile them + for file in $(find . -name "*.tex" -type f); do + filename=$(basename "$file" .tex) + # First pass + pdflatex -interaction=nonstopmode "$filename.tex" + # Second pass for references + pdflatex -interaction=nonstopmode "$filename.tex" + # Move PDF to output directory + mv "$filename.pdf" ./pdf_output/ + done + + - name: Create Release + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + run: | + # Create a timestamp for the version + VERSION="v$(date +'%Y%m%d%H%M%S')" + + # Create release with all PDFs + gh release create "$VERSION" \ + --title "LaTeX Documents $(date +'%Y-%m-%d')" \ + --notes "Automatically generated PDFs from LaTeX sources" \ + pdf_output/*.pdf + + - name: Upload Release Artifacts + uses: actions/upload-artifact@v4 + with: + name: latex-pdfs + path: pdf_output/*.pdf diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1d74e21 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.vscode/ diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..dd45b31 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,16 @@ +{ + "files.exclude": { + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.aux": true, + "**/*.glob": true, + "**/.git": true, + "**/.svn": true, + "**/.hg": true, + "**/CVS": true, + "**/.DS_Store": true, + "**/Thumbs.db": true, + "**/*.crswap": true + } +} \ No newline at end of file diff --git a/appendix.tex b/Appendix-1-Structures.tex similarity index 100% rename from appendix.tex rename to Appendix-1-Structures.tex diff --git a/appendix2.tex b/Appendix-2-Principles.tex similarity index 100% rename from appendix2.tex rename to Appendix-2-Principles.tex diff --git a/The Formalized UOR H1 HPO Candidate and Proofs.tex b/UOR-H1-HPO-Candidate.tex similarity index 100% rename from The Formalized UOR H1 HPO Candidate and Proofs.tex rename to UOR-H1-HPO-Candidate.tex diff --git a/CompactResolvent.v b/coq/CompactResolvent.v similarity index 100% rename from CompactResolvent.v rename to coq/CompactResolvent.v diff --git a/Eigenfunctions.v b/coq/Eigenfunctions.v similarity index 100% rename from Eigenfunctions.v rename to coq/Eigenfunctions.v diff --git a/Integration.v b/coq/Integration.v similarity index 100% rename from Integration.v rename to coq/Integration.v diff --git a/InverseSpectralTheory.v b/coq/InverseSpectralTheory.v similarity index 100% rename from InverseSpectralTheory.v rename to coq/InverseSpectralTheory.v diff --git a/MellinTransform.v b/coq/MellinTransform.v similarity index 100% rename from MellinTransform.v rename to coq/MellinTransform.v diff --git a/SelfAdjointness.v b/coq/SelfAdjointness.v similarity index 100% rename from SelfAdjointness.v rename to coq/SelfAdjointness.v diff --git a/ThetaInversion.v b/coq/ThetaInversion.v similarity index 100% rename from ThetaInversion.v rename to coq/ThetaInversion.v