From 7043432b844ee3b24064387ac80456a025cc5f5e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 10 Nov 2026 12:17:39 +0100 Subject: [PATCH] fix: public import to get olean in cache No-Changelog: bug fix --- src/errata/Errata/Golden.lean | 3 +++ src/errata/Errata/Runner.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean index 8d3df6a49..dbe29e39a 100644 --- a/src/errata/Errata/Golden.lean +++ b/src/errata/Errata/Golden.lean @@ -7,6 +7,9 @@ module public import Errata.TestM import Lean.Util.Diff +-- This line ensures that downstream clients get the cached olean correctly. Everything in the +-- module is private, so this doesn't affect this module's interface. +public import Errata.FS import all Errata.FS public section diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean index 269763ff7..ce564e1b0 100644 --- a/src/errata/Errata/Runner.lean +++ b/src/errata/Errata/Runner.lean @@ -9,6 +9,9 @@ public import Errata.TestM public import Errata.IsTest public import Errata.Report public import Cli +-- This line ensures that downstream clients get the cached olean correctly. Everything in the +-- module is private, so this doesn't affect this module's interface. +public import Errata.FS import all Errata.FS public section