Generate a LeanEval workspace for a Formal Conjectures declaration

.github/actions/build-lean-eval-generator/action.yml

@@ -0,0 +1,40 @@
+# Copyright 2026 The Formal Conjectures Authors.
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     https://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: Build the pinned lean-eval-generator
+description: >-
+  Clone and build leanprover/lean-eval-generator at the revision
+  comparator/tools.toml pins under [generator], and export
+  LEAN_EVAL_GENERATOR_BIN. The package depends on nothing, so this is a
+  small Lean build, not a Mathlib one. Requires elan on PATH and a
+  checked-out Formal Conjectures tree.
+
+runs:
+  using: composite
+  steps:
+    - name: Clone and build the pinned revision
+      shell: bash
+      run: |
+        read -r GEN_REPO GEN_REV <<< "$(python3 - <<'PY'
+        import tomllib
+
+        with open("comparator/tools.toml", "rb") as handle:
+            generator = tomllib.load(handle)["generator"]
+        print(generator["repository"], generator["rev"])
+        PY
+        )"
+        git clone "$GEN_REPO" "$RUNNER_TEMP/lean-eval-generator"
+        git -C "$RUNNER_TEMP/lean-eval-generator" checkout "$GEN_REV"
+        (cd "$RUNNER_TEMP/lean-eval-generator" && lake build)
+        echo "LEAN_EVAL_GENERATOR_BIN=$RUNNER_TEMP/lean-eval-generator/.lake/build/bin/lean-eval-generator" >> "$GITHUB_ENV"

.github/actions/install-elan/action.yml

@@ -0,0 +1,31 @@
+# Copyright 2026 The Formal Conjectures Authors.
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     https://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: Install elan
+description: >-
+  Install elan and put it on PATH, with no default toolchain: every job here
+  builds in a checkout whose `lean-toolchain` decides the version. The elan
+  release is pinned in one place so two jobs cannot install two different
+  installers.
+
+runs:
+  using: composite
+  steps:
+    - name: Install elan
+      shell: bash
+      run: |
+        set -o pipefail
+        curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

.github/actions/prepare-extractor/action.yml

@@ -0,0 +1,44 @@
+# Copyright 2026 The Formal Conjectures Authors.
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     https://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: Prepare the comparator extractor
+description: >-
+  Install elan at this repository's toolchain, restore the Mathlib cache,
+  build the comparator_facts extractor together with the source modules a
+  job needs elaborated, and run the extractor's self-test. The facts the
+  importer reads (ranges, binder boundaries, answer-slot types, category
+  tags) come from an elaborated environment, so every module a job imports
+  from has to be built first.
+
+inputs:
+  modules:
+    description: Space-separated Lake targets to build beside the extractor.
+    required: false
+    default: ""
+
+runs:
+  using: composite
+  steps:
+    - name: Install elan
+      uses: ./.github/actions/install-elan
+
+    - name: Build the extractor and the source modules
+      shell: bash
+      env:
+        MODULES: ${{ inputs.modules }}
+      run: |
+        lake exe cache get
+        # shellcheck disable=SC2086
+        lake build comparator_facts $MODULES
+        lake exe comparator_facts --self-test

.github/workflows/build-and-docs.yml

@@ -51,7 +51,9 @@ jobs:
           python-version: '3.12.9'
 
       - name: Run script tests
-        run: python3 -m unittest discover -s scripts -p 'test_*.py' -v
+        run: |
+          python3 -m unittest discover -s scripts -p 'test_*.py' -v
+          python3 -m unittest discover -s comparator/adapter -p 'test_*.py' -v
 
   build:
     runs-on: ubuntu-latest
@@ -111,11 +113,7 @@ jobs:
 
       - name: Install elan
         if: steps.mode.outputs.website_only != 'true'
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+        uses: ./.github/actions/install-elan
 
       - name: Restore ~/.cache/mathlib
         if: steps.mode.outputs.website_only != 'true'