Trigger CI for leanprover/lean4#3835

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

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