chore: bench build/server-mode open in import Lean (#14111)

All but direct cmdline uses pass `--setup`, so do that too for a more
meaningful benchmark

Author: Kha

tests/misc_bench/import Lean.sh

@@ -1,3 +1,3 @@
 cd ../../src
 "$TEST_DIR/measure.py" -t "$TOPIC" -d -o "$OUT" -- \
-  lean Lean.lean
+  lean --setup="$BUILD_DIR/lib/temp/Lean.setup.json" Lean.lean