DocsArtifact.yml

on:
    schedule:
        - cron: '0 2,14 * * *'  # Run twice a day (public repo, no minutes limit)
    workflow_dispatch:       # Allows manual triggering from the GitHub Actions tab

  
name: Archive site files and documentation from Physlib
  
permissions:
  contents: read
  pages: write
  id-token: write
  
jobs:
  build_project:
      if: github.repository == 'kernel-science/physlib-website'
      runs-on: ubuntu-latest
      name: Build project
      steps:
        - name: Checkout project
          uses: actions/checkout@v4
          with:
            repository: leanprover-community/physlib
            fetch-depth: 0
  
        - name: Install Graphviz
          run: sudo apt-get update && sudo apt-get install -y graphviz
  
        - name: Verify Graphviz Installation
          run: dot -V
        ##################
        # Remove this section if you don't want docs to be made
        - name: Install elan
          run: |
            set -o pipefail
            curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
            ~/.elan/bin/lean --version
            echo "$HOME/.elan/bin" >> $GITHUB_PATH
  
        - name: Get Mathlib cache
          run: lake -Kenv=dev exe cache get || true
  
        - name: Build project
          run: lake -Kenv=dev build
        
        - name: Ensure docs data directory exists
          run: mkdir -p docs/_data
          
        - name: make TODO list
          run : lake exe TODO_to_yml mkFile

        - name: Fetch GitHub issues into TODO list
          run: |
            curl -sf \
              "https://api.github.com/repos/leanprover-community/physlib/issues?state=open&per_page=100" \
              -o /tmp/gh_issues.json || { echo "Failed to fetch GitHub issues, skipping."; exit 0; }
            python3 - /tmp/gh_issues.json docs/_data/TODO.yml << 'PYEOF'
            import json, sys, yaml
            issues_path, todo_path = sys.argv[1], sys.argv[2]
            with open(issues_path) as f:
                issues = [i for i in json.load(f) if "pull_request" not in i]
            if not issues:
                print("No GitHub issues found, skipping.", file=sys.stderr)
                sys.exit(0)
            with open(todo_path) as f:
                data = yaml.safe_load(f)
            if not any(c["name"] == "GitHub Issues" for c in data["Category"]):
                data["Category"].append({"name": "GitHub Issues", "num": 0, "emoji": "📋"})
            for issue in issues:
                data["TODOItem"].append({
                    "file": "",
                    "githubLink": issue["html_url"],
                    "line": 0,
                    "isInformalDef": False,
                    "isInformalLemma": False,
                    "isSemiFormalResult": False,
                    "isSorryfulResult": False,
                    "isGitHubIssue": True,
                    "category": "GitHub Issues",
                    "name": issue["title"],
                    "tag": f"GH-{issue['number']}",
                    "content": (issue.get("body") or "").strip(),
                })
            with open(todo_path, "w") as f:
                yaml.dump(data, f, allow_unicode=True, sort_keys=False, default_flow_style=False)
            print(f"Added {len(issues)} GitHub issue(s) to TODO list.", file=sys.stderr)
            PYEOF

        - name: make list of informal proofs and lemmas
          run : lake exe informal mkFile mkDot mkHTML
  
        - name: make stats page
          run : lake exe stats mkHTML
  
        - name: Generate svg from dot
          run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot
  
        - name: Replace template file with custom
          run : cp ./scripts/Template.lean .lake/packages/doc-gen4/DocGen4/Output/Template.lean
  
        - name: Build documentation
          run: lake -Kenv=dev build Physlib:docs QuantumInfo:docs
        #End Section
        ##################

        #Moving important files to the

        - name: Create doc-artifact directory
          run: mkdir -p doc-artifact
        
        - name : Move the data sets
          run: mv docs/_data doc-artifact/_data
        
        - name : Move the stats file 
          run : mv docs/Stats.html doc-artifact/Stats.html    
        
        - name : Move the informal proofs and lemmas dot file
          run : mv docs/InformalDot.dot doc-artifact/InformalDot.dot

        - name : Move the informal proofs and lemmas
          run : mv docs/InformalGraph.html doc-artifact/InformalGraph.html

        - name: Copy documentation to `doc-artifact/docs`
          run: |
            mv .lake/build/doc doc-artifact/docs
        
        # Upload the documentation artifact
        - name: Upload documentation artifact
          uses: actions/upload-artifact@v4
          with:
            name: documentation
            path: doc-artifact/
            retention-days: 90

        - name: Trigger Vercel Deploy Hook
          env:
            VERCEL_DEPLOY_HOOK_URL: ${{ secrets.VERCEL_DEPLOY_HOOK_URL }}
          run: |
            if [ -n "$VERCEL_DEPLOY_HOOK_URL" ]; then
              curl -X POST "$VERCEL_DEPLOY_HOOK_URL"
              echo "Vercel deploy hook triggered."
            else
              echo "VERCEL_DEPLOY_HOOK_URL is not set. Skipping Vercel trigger."
            fi