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

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

__FL__ added and tested #3574

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 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
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
1 change: 1 addition & 0 deletions tests/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale
ALL_TEST_DIRS += hacl
ALL_TEST_DIRS += simple_hello
ALL_TEST_DIRS += dune_hello
ALL_TEST_DIRS += validation-time
Copy link
Member

Choose a reason for hiding this comment

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

The new single test here is not related to time at all? I think you can just drop Text.LexemeFL.fst in tests/micro-benchmarks and not add any new Makefiles.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

validation-time is the name of the phase right? Nothing to do with time. I didn't put it in micro-benchmarks as it is a correctness test. For Unix I added a run-time test directory that I'm working on right now.

Copy link
Member

Choose a reason for hiding this comment

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

micro-benchmarks is a bad name really.. we use that directory for a whole bunch of unit tests. I'll rename it soon.

HAS_OCAML := $(shell which ocamlfind 2>/dev/null)

ifneq (,$(HAS_OCAML))
Expand Down
22 changes: 22 additions & 0 deletions tests/validation-time/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
#
# This does nothing but the default validation as these are validation time test modules.
# Most are let _ = assert(...) which is extremely cool to test at validation time!
#

WARN_ERROR=--warn_error -321
FSTAR_HOME=../..
FSTAR_FILES=$(wildcard *.fst)
FSTAR_EXAMPLES=$(realpath ../../examples)
include $(FSTAR_EXAMPLES)/Makefile.include

all: verify-all

include $(FSTAR_HOME)/examples/Makefile.common

verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))

clean:
$(call msg, "CLEAN")
$(Q)rm -f .depend
$(Q)rm -rf _cache
$(Q)rm -rf _output
5 changes: 5 additions & 0 deletions tests/validation-time/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@

This directory contains tests that run on Make all which only validate F* files.
This allows validation time tests. If any validation fails, the file's tests fail.

Tests for an F* module FStar.M can be named Test.FStar.M.fst by default.
13 changes: 13 additions & 0 deletions tests/validation-time/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.Tactics.V2
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((strlen fl') = 20) by compute()
let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()
Copy link
Member

Choose a reason for hiding this comment

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

Using assert_norm breaks the dependency on tactics (and is maybe more idiomatic).

Copy link
Member

Choose a reason for hiding this comment

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

Also what is this testing? Seems to be just that 1) fl is nonempty and 2) that string_of_list and list_of_string are inverses.
(Note the missing 'e' from 'Test.LexemFL.fst(11)'.)

Copy link
Contributor Author

@briangmilnes briangmilnes Oct 17, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

No what the darn string_of_list (list_of_string is doing is getting rid of oddball characters that prevent line 13 from working to show that FL is working. See the comment line 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.

I have a commit pushed with the assert_norm changes. Do I need another PR?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

So I have Test.FLLexeme moved to the directory to be renamed later, micro-benchmarks and validaton-time deleted and out of the makefile.

And this FStar revision will compile Luke's fl(), which is two characters shorter and more obvious than FL. I have no idea that reflection would do this for me as it is not in the book.

It would obviate this entire PR.

Guido which way do you want it? Lexeme or Tactics?

Loading