"jobs" section is missing in workflow

unknown Webhook event "Lean_decl_diff". see https://docs.github.com/en/actions/learn-github-actions/events-that-trigger-workflows#webhook-events for list of all Webhook event names

unexpected key "if" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"

unexpected key "name" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"

unexpected key "runs-on" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"

unexpected key "steps" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"

❌ [actionlint] The command ran successfully and some problem was found (found 6 errors, linted 27 files), exit code: 1