ci(scripts/detect_errors): try to show info messages in a way github …

…understands (#6493)

I don't actually know if this works, but I know that the previous code was not working:

https://github.com/leanprover-community/mathlib/pull/6485/checks?check_run_id=2006396264#step:7:7



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

scripts/detect_errors.py

@@ -10,11 +10,19 @@ def encode_msg_text_for_github(msg):
 
 def format_msg(msg):
     # Formatted for https://github.com/actions/toolkit/blob/master/docs/commands.md#log-level
+
+    # mapping between lean severity levels and github levels.
+    # github does not support info levels, which are emitted by `#check` etc:
+    # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-a-debug-message
+    severity_map = {'information': 'warning'}
+    severity = msg.get('severity')
+    severity = severity_map.get(severity, severity)
+
     # We include the filename / line number information as both message and metadata, to ensure
     # that github shows it.
     msg_text = f"{msg['file_name']}:{msg.get('pos_line')}:{msg.get('pos_col')}:\n{msg.get('text')}"
     msg_text = encode_msg_text_for_github(msg_text)
-    return f"::{msg.get('severity')} file={msg['file_name']},line={msg.get('pos_line')},col={msg.get('pos_col')}::{msg_text}"
+    return f"::{severity} file={msg['file_name']},line={msg.get('pos_line')},col={msg.get('pos_col')}::{msg_text}"
 
 def write_and_print_noisy_files(noisy_files):
     with open('src/.noisy_files', 'w') as f: