Skip to main content

stage2-olean-test

Diagnose a spurious stage1 test failure caused by olean-persisted compiler changes. Use when a stage1 test fails unexpectedly and the change adds or modifies an environment extension or other information persisted into .olean files.

Informações da origem

Repositório
leanprover/lean4
Última atividade na origem
10 de junho de 2026 às 11:48
Idioma detectado do SKILL.md
inglês
Estrelas
9.551
Forks
1.044

Opções de instalação

Por padrão, está selecionado o prompt que primeiro revisa a origem. Você pode mudar para um comando direto ou baixar uma cópia local.

Revise os arquivos de origem

Leia o SKILL.md e os arquivos complementares exibidos pelo SkillsMP antes de decidir se vai instalar.

Exibindo SKILL.md

SKILL.md
Instruções da origem · Visualização somente leitura
name
stage2-olean-test
description
Diagnose a spurious stage1 test failure caused by olean-persisted compiler changes. Use when a stage1 test fails unexpectedly and the change adds or modifies an environment extension or other information persisted into .olean files.
allowed-tools
Bash, Read
# Stage2 Is Required for Changes to Olean-Persisted Compiler Information When a change alters information that is *persisted into `.olean` files* (e.g. a new or changed environment extension that the compiler reads back), a stage1 test run can fail spuriously: stage1's `src/` (including `Init`) is compiled by the **stage0** compiler, which lacks the change, so the stage1 `lean` binary imports oleans that predate the change. In that situation the relevant tests must be run against **stage2** instead, where the new compiler compiles everything consistently. So: on a test failure, if the change depends on changed olean information, test stage2 instead. ## Procedure Building stage2 is expensive, so **confirm with the user before switching to a stage2 build.** For the actual build/test commands (`make stage2`, `clean-stdlib`, per-module Lake builds, and running tests against stage2), use the **`stage2-build`** skill.
Ver no GitHub