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

Jump to bottom

__FL__ added and tested #3574

Closed
wants to merge 4 commits into from
Closed

__FL__ added and tested #3574

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9b114bd
Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/v…
briangmilnes Oct 16, 2024
6bcf77a
Moved to assert_norm instead of opening tactics and using assert(..) …
briangmilnes Oct 17, 2024
60f36d1
Moved Test.LexemeFL to micro-benchmarks got rid of tests/validation-time
briangmilnes Oct 19, 2024
5b221d0
Merge branch 'master' into milnes-fl
briangmilnes Oct 28, 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
1 change: 1 addition & 0 deletions ocaml/fstar-lib/FStarC_Parser_LexFStar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -473,6 +473,7 @@ match%sedlex lexbuf with
| "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH
| "__SOURCE_FILE__" -> STRING (L.source_file lexbuf)
| "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false)
| "__FL__" -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")")
Copy link
Member

Choose a reason for hiding this comment

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

__FL__ seems a bit obscure to me, should we maybe call this __FILELINE__? But I don't have a strong opinion, would be good if others chime in.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

You have to reference it in every test so long is kind of cumbersome. For example:
let test_system n =
let r = FStar.Unix.system "echo HI" in
match r with
| WEXITED e -> if_test FL (e = 0) n None
| _ -> final_fail FL n None

Copy link
Contributor

Choose a reason for hiding this comment

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

I agree with Guido, I aslo find FL a bit obscure.
IMO, aggregating LINE and SOURCE_FILE in this formatting is quite opinionated and should probably be user-defined.

@briangmilnes why not using a tactic for that here, e.g.:

module Hello
open FStar.Char
open FStar.Tactics

let fl
  (x: unit)
  (#[let sealed_range = range_of_term (quote x) in
     let range = unseal sealed_range in
     let result = FStar.Range.explode range in
     exact (quote result)] loc: string * int * int * int * int)
 = let file, line_start, col_start, _line_end, _col_end = loc in
   file ^ "(" ^ string_of_int line_start ^ ")"

// This is line 14
let file_line: string = fl ()
let _ = assert_norm (file_line == "<input>(15)")

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is for logging and test packages. Nothing should be left to the user. In testing the ocaml wrap of unix and a few other things, I need the file/line 139 times. Terse is good here, although I eschew it in almost all situations.

A tactic that allows a function is a great alternative. The language server in emacs takes that and works but I can't get a command line to compile it. What's the change needed for compilation? It also has the advantage that the strings are not coming back from the lexer with strange UTF8.

Copy link
Contributor

Choose a reason for hiding this comment

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

Well, verbosity or terseness is a choice, right? I tend to prefer verbosity in such cases, but that's only my preference.

Nice! Here it won't work via the command line because of <input>: that's the file name given by the F* interactive protocol used by emacs I believe.
Running that from a file whose path is /tmp/Hello.fst, you should be able to assert_norm (file_line == "/tmp/Hello.fst(15)") (instead of the one I've put above).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The issue I have is it will not compile, not the string back from fl() or FL.

F*orge: VALIDATE _build/fstar/fst/checked/Hello.fst.checked

  • Error 168 at src/Hello.fst(8,8-8,8):
    • Syntax error

1 error was reported (see above)
That's the (# line on my test of it running in OCaml.


| Plus anywhite -> token lexbuf
| newline -> L.new_line lexbuf; token lexbuf
Expand Down
13 changes: 13 additions & 0 deletions tests/micro-benchmarks/Test.LexemeFL.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
/// A new lexeme __FL__ has been added to show file and line (file(line)) to make writing tests easier.
/// This file is line sensitive any edit will change the value of __FL__.
module Test.LexemeFL

open FStar.String
module LT = FStar.List.Tot
// Kinda funky to get a good validation time test, added Strings in other PR will fix this.
// The lexer is sending back some strange character that we have to adjust.
let fl = __FL__
let _ = assert(fl <> "")
let fl' = string_of_list (list_of_string "Test.LexemFL.fst(11)")
let _ = assert_norm((strlen fl') = 20)
let _ = assert_norm(fl' = "Test.LexemFL.fst(11)")
Loading