Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: improvements to test_extern command #3075

Merged
merged 7 commits into from
Apr 24, 2024
Merged

feat: improvements to test_extern command #3075

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
847b841
feat: improvements to test_extern command
kim-em Dec 15, 2023
e43d727
add implemented_by test
kim-em Dec 15, 2023
5cc1acc
fix .expected.out
kim-em Dec 15, 2023
8a99675
merge master
kim-em Apr 22, 2024
d74c2e8
Merge remote-tracking branch 'origin/master' into test_extern_update
kim-em Apr 24, 2024
a9364de
fix test
kim-em Apr 24, 2024
d0170cc
fix test
kim-em Apr 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions src/Lean/Util/TestExtern.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,9 @@ import Lean.Elab.SyntheticMVars
import Lean.Elab.Command
import Lean.Meta.Tactic.Unfold
import Lean.Meta.Eval
import Lean.Compiler.ImplementedByAttr

open Lean Elab Meta Command Term
open Lean Elab Meta Command Term Compiler

syntax (name := testExternCmd) "test_extern " term : command

Expand All @@ -12,14 +13,15 @@ syntax (name := testExternCmd) "test_extern " term : command
let t ← elabTermAndSynthesize t none
match t.getAppFn with
| .const f _ =>
if isExtern (← getEnv) f then
let env ← getEnv
if isExtern env f || (getImplementedBy? env f).isSome then
let t' := (← unfold t f).expr
let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq 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: {f} does not have an @[extern] attribute or @[implemented_by] attribute"
| _ => throwError "test_extern: expects a function application"
| _ => throwUnsupportedSyntax
10 changes: 8 additions & 2 deletions tests/lean/test_extern.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,15 @@
import Lean.Util.TestExtern

instance : BEq ByteArray where
beq x y := x.data == y.data
deriving instance DecidableEq for ByteArray

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

def f := 3

@[implemented_by f]
def g := 4

test_extern g
6 changes: 4 additions & 2 deletions tests/lean/test_extern.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
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!
test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
test_extern.lean:8:0-8:86: error: native implementation did not agree with reference implementation!
Compare the outputs of:
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why does the error message say to compare the outputs instead of showing what the outputs are? I think it should actually print the outputs (when possible), because these issues can be OS dependent so it's important to know what value was actually produced in CI since they may not reproduce locally.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a good suggestion, but I'd prefer not to take it on now. Happy to either open an issue, let you do that. Or, for that matter, to accept commits on this PR, or promise to review a new PR! :-)

#eval ByteArray.copySlice { data := #[1, 2, 3] } 1 { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] } 0 6
and
Expand All @@ -9,3 +9,5 @@ Compare the outputs of:
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) }
test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
Compare the outputs of: #eval g and #eval 4