update

gd · gd · commit 4c27d6886fd2 · 2025-05-11T10:32:31.000-04:00
diff --git a/.dockerignore b/.dockerignore
@@ -0,0 +1,2 @@
+.git
+build
diff --git a/.github/workflows/actionlint.yml b/.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
diff --git a/.github/workflows/awaiting-mathlib.yml b/.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;
diff --git a/.github/workflows/backport.yml b/.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
       && (
diff --git a/.github/workflows/build-template.yml b/.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: |
diff --git a/.github/workflows/check-prelude.yml b/.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 }}
diff --git a/.github/workflows/check-stage0.yml b/.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;
diff --git a/.github/workflows/ci.yml b/.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
diff --git a/.github/workflows/copyright-header.yml b/.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: |
diff --git a/.github/workflows/labels-from-comments.yml b/.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: |
diff --git a/.github/workflows/nix-ci.yml b/.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 }}
diff --git a/.github/workflows/pr-body.yml b/.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;
diff --git a/.github/workflows/pr-release.yml b/.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 }}
diff --git a/.github/workflows/pr-title.yml b/.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;
diff --git a/.github/workflows/stale.yml b/.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
diff --git a/.github/workflows/update-stage0.yml b/.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 }}
diff --git a/Dockerfile b/Dockerfile
@@ -0,0 +1,21 @@
+FROM debian
+
+RUN apt update -y
+#RUN apt get install -y cmake 
+#RUN apt-get build-dep lean4
+RUN apt-get install -y git libgmp-dev libuv1-dev cmake ccache clang pkgconf
+
+
+WORKDIR /opt/lean4
+#ADD . /opt/lean4
+ADD src /opt/lean4/src/
+ADD script /opt/lean4/script
+ADD tests /opt/lean4/tests/
+ADD stage0 /opt/lean4/stage0/
+ADD CMakeLists.txt /opt/lean4/CMakeLists.txt
+ADD CMakePresets.json /opt/lean4/CMakePresets.json
+ADD lean-toolchain /opt/lean4/lean-toolchain
+ADD lean.code-workspace /opt/lean4/lean.code-workspace
+
+RUN cmake --preset release
+RUN make -C build/release -j20
diff --git a/src/Lean/Server/Completion/LeanServer3.code-workspace b/src/Lean/Server/Completion/LeanServer3.code-workspace
@@ -0,0 +1,11 @@
+{
+	"folders": [
+		{
+			"path": "../../../../../LeanServer3"
+		},
+		{
+			"path": "../../../.."
+		}
+	],
+	"settings": {}
+}
