Lean4
/-- The main function to validate the copyright string.
The input is the copyright string, the output is an array of `Syntax × String` encoding:
* the `Syntax` factors are atoms whose ranges are "best guesses" for where the changes should
take place; the embedded string is the current text that the linter flagged;
* the `String` factor is the linter message.
The linter checks that
* the first and last line of the copyright are a `("/-", "-/")` pair, each on its own line;
* the first line is begins with `Copyright (c) 20` and ends with `. All rights reserved.`;
* the second line is `Released under Apache 2.0 license as described in the file LICENSE.`;
* the remainder of the string begins with `Authors: `, does not end with `.` and
contains no ` and ` nor a double space, except possibly after a line break.
-/
def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) :=
Id.run
(do
-- First, we merge lines ending in `,`: two spaces after the line-break are ok,
-- but so is only one or none. We take care of *not* adding more consecutive spaces, though.
-- This is to allow the copyright or authors' lines to span several lines.
let preprocessCopyright :=
(copyright.replace ",\n " ", ").replace ",\n"
","
-- Filter out everything after the first isolated `-/`.
let pieces := preprocessCopyright.splitOn "\n-/"
let copyright := (pieces.getD 0 "") ++ "\n-/"
let stdText (s : String) := s! "Malformed or missing copyright header: `{s}` should be alone on its own line."
let mut output := #[]
if (pieces.getD 1 "\n").take 1 != "\n" then
output := output.push (toSyntax copyright "-/", s! "{stdText "-/"}")
let lines := copyright.splitOn "\n"
let closeComment := lines.getLastD ""
match lines with
| openComment :: copyrightAuthor :: license :: authorsLines =>
-- The header should start and end with blank comments.
match openComment, closeComment with
| "/-", "-/" =>
output := output
| "/-", _ =>
output := output.push (toSyntax copyright closeComment, s! "{stdText "-/"}")
| _, _ =>
output :=
output.push
(toSyntax copyright openComment, s! "{stdText ("/".push '-')}")
-- Validate the first copyright line.
let copStart := "Copyright (c) 20"
let copStop := ". All rights reserved."
if !copyrightAuthor.startsWith copStart then
output :=
output.push
(toSyntax copyright (copyrightAuthor.take copStart.length),
s!"Copyright line should start with 'Copyright (c) YYYY'")
if !copyrightAuthor.endsWith copStop then
output :=
output.push
(toSyntax copyright (copyrightAuthor.takeRight copStop.length),
s!"Copyright line should end with '. All rights reserved.'")
-- Validate the authors line(s). The last line is the closing comment: trim that off right away.
let authorsLines := authorsLines.dropLast
if authorsLines.length == 0 then
output := output.push (toSyntax copyright "-/", s!"Copyright too short!")
else
-- If the list of authors spans multiple lines, all but the last line should end with a trailing
-- comma. This excludes e.g. other comments in the copyright header.
let authorsLine := "\n".intercalate authorsLines
let authorsStart := (("\n".intercalate [openComment, copyrightAuthor, license, ""])).endPos
if authorsLines.length > 1 && !authorsLines.dropLast.all (·.endsWith ",") then
output :=
output.push
((toSyntax copyright authorsLine),
"If an authors line spans multiple lines, \
each line but the last must end with a trailing comma")
output := output.append (authorsLineChecks authorsLine authorsStart)
let expectedLicense := "Released under Apache 2.0 license as described in the file LICENSE."
if license != expectedLicense then
output :=
output.push (toSyntax copyright license, s! "Second copyright line should be \"{expectedLicense}\"")
| _ =>
output := output.push (toSyntax copyright "-/", s!"Copyright too short!")
return output)
