Skip to content
CI

aarch64 orphanage: increase use of automation #2892

Sign in to view logs

aarch64 orphanage: increase use of automation

aarch64 orphanage: increase use of automation #2892

GitHub Actions / File annotations for theory linter succeeded Mar 13, 2024 in 1s

File annotations for theory linter

Annotations

Check failure on line 1755 in proof/crefine/AARCH64/Fastpath_C.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Unfinished proof 

This command indicates an unfinished or aborted proof.

Check failure on line 2571 in proof/crefine/AARCH64/Fastpath_C.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Unfinished proof 

This command indicates an unfinished or aborted proof.

Check failure on line 549 in proof/crefine/AARCH64/Fastpath_Equiv.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Unfinished proof 

This command indicates an unfinished or aborted proof.

Check failure on line 1423 in proof/crefine/AARCH64/Fastpath_Equiv.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Unfinished proof 

This command indicates an unfinished or aborted proof.

Check failure on line 17 in proof/crefine/AARCH64/Init_C.thy

See this annotation in the file changed.

@github-actions github-actions / File annotations for theory linter

Axioms 

Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.
View more details on GitHub Actions