From e5450096b074b32faf8bb81d0d3bb16a691335c1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Apr 2024 07:25:49 +0000 Subject: [PATCH] chore: remove the ProofWidgets import (#11877) This follows on from #11350, following an alternative suggestion by @digama0. One argument for this pattern is that it also works for tests that import `ProofWidgets.Demos.*`, and any other auxiliary content in upstream packages that is not part of the top-level package. --- GNUmakefile | 8 ++++++-- Mathlib/Tactic/Common.lean | 5 ----- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/GNUmakefile b/GNUmakefile index 285de9c0091d2..cbb2051369518 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,16 +2,20 @@ SHELL=/usr/bin/env -S bash -o pipefail TESTS := $(shell find test -name '*.lean') -.PHONY: all build test lint +.PHONY: all build test lint testdeps all: build test build: lake build +testdeps: build + # add any extra targets that tests depend on here + lake build ProofWidgets + test: $(addsuffix .run, $(TESTS)) -test/%.run: build +test/%.run: testdeps lake env lean test/$* | scripts/check_silent.sh test/$*.log lint: build diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 7afe4a2e6fd56..70a43a3d06a60 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -11,11 +11,6 @@ import Qq -- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ... import ImportGraph.Imports --- Currently we don't need to import all of ProofWidgets, --- but without this, if you don't run `lake build ProofWidgets` then `make test` will fail. --- Hopefully `lake` will be able to handle tests later. -import ProofWidgets - -- Now import all tactics defined in Mathlib that do not require theory files. import Mathlib.Mathport.Rename import Mathlib.Tactic.ApplyCongr