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.

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

Add support for unit tests via $[test] attribute #928

Draft
wants to merge 2 commits into
base: sail2
Choose a base branch
from

Conversation

Timmmm
Copy link
Contributor

@Timmmm Timmmm commented Jan 30, 2025

Draft for #919, just checking if this approach makes sense.

Still TODO:

  • Documentation
  • Verify the type is unit -> unit for functions where this is applied.
  • Tests
  • Other backends??
  • Output formatting isn't quite right; not sure why.

Still TODO:

* Documentation
* Verify the type is `unit -> unit` for functions where this is applied.
* Tests
* Other backends??
* Output formatting isn't quite right; not sure why.
Copy link

github-actions bot commented Jan 30, 2025

Test Results

   12 files  ± 0     24 suites  ±0   0s ⏱️ ±0s
  768 tests + 9    762 ✅ + 3  0 💤 ±0  0 ❌ ±0   6 🔥 + 6 
2 525 runs  +22  2 513 ✅ +10  0 💤 ±0  0 ❌ ±0  12 🔥 +12 

For more details on these errors, see this check.

Results for commit 59d29e3. ± Comparison against base commit e7f1262.

♻️ This comment has been updated with latest results.

@Alasdair
Copy link
Collaborator

Yes, that looks like the right way to go.

@@ -4630,6 +4630,14 @@ let check_fundef_lazy env def_annot (FD_aux (FD_function (recopt, tannot_opt, fu
| Some vs_l -> check_tannot_opt ~def_type:"function" vs_l env vtyp_ret tannot_opt
| None -> ()
end;
(* Check $[test] functions have type unit -> unit. *)
(* TODO: Does the annotation go on the type declaration or the function definition? *)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think in general we put these annotations on the val type declarations. That's where $[property] and $[counterexample] are expected to be.

If you have a function with an inline annotation:

$[annot]
function f(x : int) -> unit = ...

it'll get expanded to

$[annot]
val f : int -> unit
$[annot]
function f(x) = ...

with the annotation on both.

@@ -2225,6 +2225,7 @@ let compile_ast env effect_info output_chan c_includes ast =
let end_extern_cpp = separate hardline (List.map string [""; "#ifdef __cplusplus"; "}"; "#endif"]) in
let hlhl = hardline ^^ hardline in

(* TODO: Formatting here isn't quite right. What are the arguments to jump? *)
Copy link
Collaborator

Choose a reason for hiding this comment

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

@Alasdair
Copy link
Collaborator

Alasdair commented Feb 5, 2025

I think this change has probably broken this PR: #960 I can fix if you like?

@Timmmm
Copy link
Contributor Author

Timmmm commented Feb 7, 2025

Ah that's a nice change. Don't worry, I'll try and figure it out. You have more important things to do!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants