error when executing port status script

Stream: mathlib4

[Jakob von Raumer]

@Scott Morrison The python script now gives me a

(base) javra@wollaton:~/Dokumente/kit/mathlib$ ./scripts/port_status.py
Traceback (most recent call last):
  File "/home/javra/Dokumente/kit/mathlib/./scripts/port_status.py", line 38, in <module>
    data = yaml.safe_load(urlopen('https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md'))
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/__init__.py", line 125, in safe_load
    return load(stream, SafeLoader)
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/__init__.py", line 81, in load
    return loader.get_single_data()
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/constructor.py", line 49, in get_single_data
    node = self.get_single_node()
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/composer.py", line 35, in get_single_node
    if not self.check_event(StreamEndEvent):
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/parser.py", line 98, in check_event
    self.current_event = self.state()
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/parser.py", line 142, in parse_implicit_document_start
    if not self.check_token(DirectiveToken, DocumentStartToken,
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/scanner.py", line 116, in check_token
    self.fetch_more_tokens()
  File "/home/javra/.local/lib/python3.9/site-packages/yaml/scanner.py", line 258, in fetch_more_tokens
    raise ScannerError("while scanning for the next token", None,
yaml.scanner.ScannerError: while scanning for the next token
found character '`' that cannot start any token
  in "<file>", line 10, column 1

on execution :sad:

[Scott Morrison]

Try again in a moment. Someone helpfully added backticks at the start and end of the list to try to make it format nicely, but that breaks the yaml parser.

[Scott Morrison]

(@Yakov Pechersky, unfortunately this change broke the script. I guess we could have port_status.py attempt to strip from the file before it parses?)

[Yakov Pechersky]

I apologize for breaking userspace! Will update the script accordingly

[Scott Morrison]

Thanks!

[Yakov Pechersky]

#17076