test: make 1697 Linux-Debug safe

leanprover · Jul 25, 2024 · 2fe82fe · 2fe82fe
1 parent 93fa9c8
commit 2fe82fe
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean
@@ -27,10 +27,19 @@ info: 3
 #guard_msgs in
 #eval! #[1,2,3][2]'sorry
 
+
+/-
+
+With this test I wanted to show that `#eval!` can be used to do unsafe operations. Under
+normal circumstances this actually works with the output below, but the `Linux Debug` CI build
+catches it and complains. Maybe too bold to have this in the test suite.
+
 /--
 warning: declaration uses 'sorry'
 ---
 info: 3
 -/
 #guard_msgs in
 #eval! (#[1,2,3].pop)[2]'sorry
+
+-/