Errors: Introducing '--message_format github', for github actions

mk/diff.sh

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+if [ $# -ne 2 ]; then
+  echo "usage: $0 <actual_output> <expected_output>" >&2
+  exit 1
+fi
+
+ACTUAL="$1"
+EXPECTED="$2"
+
+DIFF="diff -u --strip-trailing-cr"
+
+if $DIFF "$ACTUAL" "$EXPECTED" ; then
+  # OK
+  exit 0
+else
+  # We're gonna fail. If we're running in CI, emit a Github
+  # error message.
+  if [ -v GITHUB_ENV ]; then
+    DIFFTEXT=$($DIFF "$ACTUAL" "$EXPECTED" | sed 's/$/%0A/' | tr -d '\n')
+    ACTUAL=$(realpath "$ACTUAL")
+    ACTUAL="${ACTUAL#$FSTAR_ROOT}"
+    EXPECTED=$(realpath "$EXPECTED")
+    EXPECTED="${EXPECTED#$FSTAR_ROOT}"
+    echo "::error::Diff failed for files $ACTUAL and $EXPECTED:%0A%0A$DIFFTEXT"
+  else
+    echo "error: Diff failed for files $ACTUAL and $EXPECTED" >&2
+  fi
+  exit 1
+fi

mk/test.mk

@@ -119,7 +119,7 @@ $(OUTPUT_DIR)/%.out: $(OUTPUT_DIR)/%.exe
 ### Checking expected output for any kind of file (error output, ml, etc)
 $(OUTPUT_DIR)/%.diff: $(OUTPUT_DIR)/% %.expected
 	$(call msg, "DIFF", $<)
-	diff -u --strip-trailing-cr $^
+	$(FSTAR_ROOT)/mk/diff.sh $^
 	touch $@
 
 $(OUTPUT_DIR)/%.accept: $(OUTPUT_DIR)/%

src/basic/FStarC.Errors.fst

@@ -22,12 +22,13 @@ open FStarC.Compiler.Effect
 open FStarC.Compiler.List
 open FStarC.Compiler.Util
 open FStarC.Compiler.Range
-open FStarC.Class.Monad
 open FStarC.Options
 module List = FStarC.Compiler.List
 module BU = FStarC.Compiler.Util
 module PP = FStarC.Pprint
 
+open FStarC.Class.Monad
+open FStarC.Class.Show
 open FStarC.Errors.Codes
 open FStarC.Errors.Msg
 open FStarC.Json
@@ -175,27 +176,26 @@ let optional_def (f : 'a -> PP.document) (def : PP.document) (o : option 'a) : P
 
 let format_issue' (print_hdr:bool) (issue:issue) : string =
   let open FStarC.Pprint in
-  let level_header = doc_of_string (string_of_issue_level issue.issue_level) in
-  let num_opt =
-    if issue.issue_level = EError || issue.issue_level = EWarning
-    then blank 1 ^^ optional_def (fun n -> doc_of_string (string_of_int n)) (doc_of_string "<unknown>") issue.issue_number
-    else empty
-  in
   let r = issue.issue_range in
-  let atrng : document =
-    match r with
-    | Some r when r <> Range.dummyRange ->
-      blank 1 ^^ doc_of_string "at" ^^ blank 1 ^^ doc_of_string (Range.string_of_use_range r)
-    | _ ->
-      empty
-  in
   let hdr : document =
-    if print_hdr
-    then
+    if print_hdr then (
+      let level_header = doc_of_string (string_of_issue_level issue.issue_level) in
+      let num_opt =
+        if issue.issue_level = EError || issue.issue_level = EWarning
+        then blank 1 ^^ optional_def (fun n -> doc_of_string (string_of_int n)) (doc_of_string "<unknown>") issue.issue_number
+        else empty
+      in
+      let atrng : document =
+        match r with
+        | Some r when r <> Range.dummyRange ->
+          blank 1 ^^ doc_of_string "at" ^^ blank 1 ^^ doc_of_string (Range.string_of_use_range r)
+        | _ ->
+          empty
+      in
       doc_of_string "*" ^^ blank 1 ^^ level_header ^^ num_opt ^^
         atrng ^^
         doc_of_string ":" ^^ hardline
-    else empty
+    ) else empty
   in
   let seealso : document =
     match r with
@@ -230,6 +230,38 @@ let format_issue issue : string = format_issue' true issue
 let print_issue_json issue =
     json_of_issue issue |> string_of_json |> BU.print1_error "%s\n"
 
+(*
+  Printing for nicer display in github actions runs. See
+    https://docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/workflow-commands-for-github-actions
+  for more info. The idea here is basically render it as text and then
+  add a github header. Also we replace newlines by %0A which become
+  newlines in the rendered github annotation, though that does not seem
+  to be very well documented (https://github.com/orgs/community/discussions/26736)
+*)
+let print_issue_github issue =
+  match issue.issue_level with
+  | ENotImplemented
+  | EInfo -> ()
+  | EError
+  | EWarning ->
+    let level = if EError? issue.issue_level then "error" else "warning" in
+    let rng = dflt dummyRange issue.issue_range in
+    let msg = format_issue' true issue in
+    let msg = msg |> BU.splitlines |> String.concat "%0A" in
+    let num =
+      match issue.issue_number with
+      | None -> ""
+      | Some n -> BU.format1 "(%s) " (show n)
+    in
+    BU.print_warning <|
+      BU.format6 "::%s file=%s,line=%s,endLine=%s::%s%s\n"
+        level
+        (Range.file_of_range rng)
+        (show (rng |> Range.start_of_range |> Range.line_of_pos))
+        (show (rng |> Range.end_of_range   |> Range.line_of_pos))
+        num
+        msg
+
 let print_issue_rendered issue =
     let printer =
         match issue.issue_level with
@@ -243,6 +275,7 @@ let print_issue issue =
     match FStarC.Options.message_format () with
     | Human -> print_issue_rendered issue
     | Json -> print_issue_json issue
+    | Github -> print_issue_github issue
 
 let compare_issues i1 i2 =
     match i1.issue_range, i2.issue_range with

src/basic/FStarC.Options.fst

@@ -991,7 +991,7 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
 
   ( noshort,
     "message_format",
-    EnumStr ["human"; "json"],
+    EnumStr ["human"; "json"; "github"],
     text "Format of the messages emitted by F* (default `human`)");
 
   ( noshort,
@@ -1997,6 +1997,7 @@ let message_format               () =
   match get_message_format () with
   | "human" -> Human
   | "json" -> Json
+  | "github" -> Github
   | illegal -> failwith ("print_issue: option `message_format` was expected to be `human` or `json`, not `" ^ illegal ^ "`. This should be impossible: `message_format` was supposed to be validated.")
 let force                        () = get_force                       ()
 let full_context_dependency      () = true

src/basic/FStarC.Options.fsti

@@ -33,7 +33,7 @@ type codegen_t =
 
 type split_queries_t = | No | OnFailure | Always
 
-type message_format_t = | Json | Human
+type message_format_t = | Json | Human | Github
 
 type option_val =
   | Bool of bool