Trigger CI for https://github.com/leanprover/lean4/pull/3210 #68900
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
2s
check workflows
7s
Post-CI job
0s
Annotations
10 errors and 5 warnings
|
Build:
Mathlib/Tactic/SimpIntro.lean#L25
application type mismatch
|
|
Build:
Mathlib/Tactic/SimpIntro.lean#L40
application type mismatch
|
|
Build:
Mathlib/Tactic/SimpIntro.lean#L75
application type mismatch
|
|
Build
application type mismatch
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L19
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L29
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L34
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L37
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L40
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Build:
Mathlib/Tactic/Attr/Register.lean#L44
unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'
|
|
Cancel Previous Runs (CI)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: styfle/cancel-workflow-action@0.11.0. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
check workflows
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Check all files imported
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Lint style
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/setup-python@v4. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Build
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, liskin/gh-problem-matcher-wrap@v2. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|