feat: test_extern command (#2970)

This adds a `test_extern` command.

Usage:
```
import Lean.Util.TestExtern

test_extern Nat.add 17 37
```

This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.

Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.

src/Lean/Util.lean

@@ -23,6 +23,7 @@ import Lean.Util.ForEachExprWhere
 import Lean.Util.ReplaceLevel
 import Lean.Util.FoldConsts
 import Lean.Util.SCC
+import Lean.Util.TestExtern
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo

src/Lean/Util/TestExtern.lean

@@ -0,0 +1,25 @@
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Command
+import Lean.Meta.Tactic.Unfold
+import Lean.Meta.Eval
+
+open Lean Elab Meta Command Term
+
+syntax (name := testExternCmd) "test_extern " term : command
+
+@[command_elab testExternCmd] unsafe def elabTestExtern : CommandElab
+  | `(test_extern $t:term) => liftTermElabM do
+    let t ← elabTermAndSynthesize t none
+    match t.getAppFn with
+    | .const f _ =>
+      if isExtern (← getEnv) f then
+        let t' := (← unfold t f).expr
+        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        if ! (← evalExpr Bool (.const ``Bool []) r) then
+          throwError
+            ("native implementation did not agree with reference implementation!\n" ++
+            m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
+      else
+        throwError "test_extern: {f} does not have an @[extern] attribute"
+    | _ => throwError "test_extern: expects a function application"
+  | _ => throwUnsupportedSyntax

tests/lean/test_extern.lean

@@ -0,0 +1,9 @@
+import Lean.Util.TestExtern
+
+instance : BEq ByteArray where
+  beq x y := x.data == y.data
+
+test_extern Nat.add 12 37
+test_extern 4 + 5
+
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6

tests/lean/test_extern.lean.expected.out

@@ -0,0 +1,11 @@
+test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
+test_extern.lean:9:0-9:86: error: native implementation did not agree with reference implementation!
+Compare the outputs of:
+#eval ByteArray.copySlice { data := #[1, 2, 3] } 1 { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] } 0 6
+ and
+#eval {
+  data :=
+    Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data 0 0 ++
+        Array.extract { data := #[1, 2, 3] }.data 1 (1 + 6) ++
+      Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data (0 + 6)
+        (Array.size { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data) }

tests/pkg/test_extern/TestExtern.lean

@@ -0,0 +1,5 @@
+import Lean.Util.TestExtern
+import TestExtern.BadExtern
+
+test_extern Nat.add 4 5
+test_extern Nat.not_add 4 5

tests/pkg/test_extern/TestExtern/BadExtern.lean

@@ -0,0 +1,3 @@
+@[extern "lean_nat_add"]
+protected def Nat.not_add : (@& Nat) → (@& Nat) → Nat
+  | _, _ => 0

tests/pkg/test_extern/expected.txt

@@ -0,0 +1,7 @@
+error: stdout:
+./././TestExtern.lean:5:0: error: native implementation did not agree with reference implementation!
+Compare the outputs of:
+#eval Nat.not_add 4 5
+ and
+#eval match 4, 5 with
+| x, x_1 => 0

tests/pkg/test_extern/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test_extern where
+  precompileModules := true
+
+@[default_target] lean_lib TestExtern

tests/pkg/test_extern/test.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+
+# We need a package test because we need multiple files with imports.
+# Currently the other package tests all succeed,
+# but here we need to check for a particular error message.
+# This is just an ad-hoc text mangling script to extract the error message
+# and account for some OS differences.
+# Ideally there would be a more principled testing framework
+# that took care of all this!
+
+rm -rf .lake/build
+
+# Function to process the output
+verify_output() {
+    # Normalize path separators from backslashes to forward slashes
+    sed 's#\\#/#g' |
+    awk '/error: stdout:/, /error: external command/' |
+    sed '/error: external command/d'
+}
+
+lake build 2>&1 | verify_output > produced.txt
+
+# Compare the actual output with the expected output
+if diff --strip-trailing-cr -q produced.txt expected.txt > /dev/null; then
+    echo "Output matches expected output."
+    rm produced.txt
+    exit 0
+else
+    echo "Output differs from expected output:"
+    diff --strip-trailing-cr produced.txt expected.txt
+    rm produced.txt
+    exit 1
+fi