all your bases belong to us

.dockerignore

@@ -0,0 +1,2 @@
+.git
+build

.github/workflows/actionlint.yml

@@ -15,8 +15,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v4
+      uses: meta-introspector/checkout@v4
     - name: actionlint
-      uses: raven-actions/actionlint@v2
+      uses: raven-meta-introspector/actionlint@v2
       with:
         pyflakes: false # we do not use python scripts

.github/workflows/awaiting-mathlib.yml

@@ -11,7 +11,7 @@ jobs:
     steps:
       - name: Check awaiting-mathlib label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             const { labels } = context.payload.pull_request;

.github/workflows/backport.yml

@@ -10,7 +10,7 @@ jobs:
     name: Backport
     runs-on: ubuntu-latest
     # Only react to merged PRs for security reasons.
-    # See https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request_target.
+    # See https://docs.github.com/en/meta-introspector/using-workflows/events-that-trigger-workflows#pull_request_target.
     if: >
       github.event.pull_request.merged
       && (

.github/workflows/build-template.yml

@@ -69,7 +69,7 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
@@ -99,7 +99,7 @@ jobs:
         if: matrix.cmultilib
       - name: Cache
         id: restore-cache
-        uses: actions/cache/restore@v4
+        uses: meta-introspector/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below
           path: |
@@ -179,7 +179,7 @@ jobs:
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v4
+      - uses: meta-introspector/upload-artifact@v4
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -237,7 +237,7 @@ jobs:
           done
       - name: Save Cache
         if: always() && steps.restore-cache.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v4
+        uses: meta-introspector/cache/save@v4
         with:
           # NOTE: must be in sync with `restore` above
           path: |

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/check-stage0.yml

@@ -8,7 +8,7 @@ jobs:
   check-stage0-on-queue:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v4
+    - uses: meta-introspector/checkout@v4
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         filter: blob:none
@@ -31,7 +31,7 @@ jobs:
 
     - if: github.event_name == 'pull_request'
       name: Set label
-      uses: actions/github-script@v7
+      uses: meta-introspector/github-script@v7
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -54,7 +54,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
       - name: Set Nightly
@@ -130,7 +130,7 @@ jobs:
 
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
@@ -212,7 +212,7 @@ jobs:
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
-                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+                "tar": "gtar" // https://github.com/meta-introspector/runner-images/issues/2619
               },
               {
                 "name": "macOS aarch64",
@@ -223,7 +223,7 @@ jobs:
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
-                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
+                "tar": "gtar", // https://github.com/meta-introspector/runner-images/issues/2619
                 // Special handling for MacOS aarch64, we want:
                 // 1. To run it in PRs so Mac devs get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the Linux build and adds
@@ -338,9 +338,9 @@ jobs:
         topic: "Github actions"
         type: "stream"
         content: |
-          A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
+          A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/meta-introspector/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v7
+      uses: meta-introspector/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -353,7 +353,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v4
+      - uses: meta-introspector/download-artifact@v4
         with:
           path: artifacts
       - name: Release
@@ -378,12 +378,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           # needed for tagging
           fetch-depth: 0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v4
+      - uses: meta-introspector/download-artifact@v4
         with:
           path: artifacts
       - name: Prepare Nightly Release

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v4
+    - uses: meta-introspector/checkout@v4
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/docker-image.yml

@@ -0,0 +1,18 @@
+name: Docker Image CI
+
+on:
+  push:
+  #  branches: [ "master" ]
+  pull_request:
+  #  branches: [ "master" ]
+
+jobs:
+
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: meta-introspector/checkout@v4
+    - name: Build the Docker image
+      run: docker build . --file Dockerfile --tag my-image-name:$(date +%s)

.github/workflows/labels-from-comments.yml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v7
+      uses: meta-introspector/github-script@v7
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/nix-ci.yml

@@ -21,7 +21,7 @@ jobs:
     steps:
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             let large = ${{ github.repository == 'leanprover/lean4' }};
@@ -50,12 +50,12 @@ jobs:
       NIX_BUILD_ARGS: --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Set Up Nix Cache
-        uses: actions/cache@v4
+        uses: meta-introspector/cache@v4
         with:
           path: nix-store-cache
           key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
@@ -79,7 +79,7 @@ jobs:
           sudo mkdir -m0770 -p /nix/var/cache/ccache
           sudo chown -R $USER /nix/var/cache/ccache
       - name: Setup CCache Cache
-        uses: actions/cache@v4
+        uses: meta-introspector/cache@v4
         with:
           path: /nix/var/cache/ccache
           key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}

.github/workflows/pr-body.yml

@@ -11,7 +11,7 @@ jobs:
     steps:
       - name: Check PR body
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             const { title, body, labels, draft } = context.payload.pull_request;

.github/workflows/pr-release.yml

@@ -13,7 +13,7 @@
 name: PR release
 
 on:
-  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
+  workflow_run: # https://docs.github.com/en/meta-introspector/using-workflows/events-that-trigger-workflows#workflow_run
     workflows: [CI]
     types: [completed]
 
@@ -23,7 +23,7 @@ jobs:
     if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
     steps:
       - name: Retrieve information about the original workflow
-        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
+        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/meta-introspector/get-workflow-origin
         # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number
         # see https://github.com/orgs/community/discussions/25220 for some discussion
         id: workflow-info
@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/meta-introspector/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -75,7 +75,7 @@ jobs:
 
       - name: Report release status
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -89,7 +89,7 @@ jobs:
 
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             await github.rest.issues.addLabels({
@@ -227,7 +227,7 @@ jobs:
 
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             const description =
@@ -254,7 +254,7 @@ jobs:
       # Checkout the Batteries repository with all branches
       - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
@@ -311,7 +311,7 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v4
+        uses: meta-introspector/checkout@v4
         with:
           repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/pr-title.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR title
-        uses: actions/github-script@v7
+        uses: meta-introspector/github-script@v7
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v9
+      - uses: meta-introspector/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.github/workflows/update-stage0.yml

@@ -23,7 +23,7 @@ jobs:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v4
+    - uses: meta-introspector/checkout@v4
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -47,7 +47,7 @@ jobs:
     #  uses: DeterminateSystems/magic-nix-cache-action@v2
     - if: env.should_update_stage0 == 'yes'
       name: Restore Build Cache
-      uses: actions/cache/restore@v4
+      uses: meta-introspector/cache/restore@v4
       with:
         path: nix-store-cache
         key: Nix Linux-nix-store-cache-${{ github.sha }}

.gitignore

@@ -32,3 +32,7 @@ fwOut.txt
 wdErr.txt
 wdIn.txt
 wdOut.txt
+/build2/
+changes.zip
+.changes/**
+

.vscode/settings.json

@@ -0,0 +1,14 @@
+{
+    "files.exclude": {
+        "**/*.vo": true,
+        "**/*.vok": true,
+        "**/*.vos": true,
+        "**/*.aux": true,
+        "**/*.glob": true,
+        "**/.git": true,
+        "**/.svn": true,
+        "**/.hg": true,
+        "**/.DS_Store": true,
+        "**/Thumbs.db": true
+    }
+}