From 7965ba2600810131933eaff427381bafc8e3c96d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 1 Feb 2022 12:23:05 +0000
Subject: [PATCH 1/2] Use github.com Linux kernel mirror in integration test

CI jobs running on github are less likely to temporarily fail when using
mirrors from github.com. The (transient?) failure seen most recently
was:
```
git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10
Cloning into 'linux_5_10'...
remote: aborting due to possible repository corruption on the remote side.
fatal: early EOF
fatal: fetch-pack: invalid index-pack output
```
This commit seeks to address this kind of problem.
---
 integration/linux/compile_linux.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/integration/linux/compile_linux.sh b/integration/linux/compile_linux.sh
index b80c146ba72..cd130a548a9 100755
--- a/integration/linux/compile_linux.sh
+++ b/integration/linux/compile_linux.sh
@@ -21,7 +21,7 @@ make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j$(npr
 [ -d one-line-scan ] || git clone https://github.com/awslabs/one-line-scan.git one-line-scan
 
 # Get Linux v5.10, if we do not have it already
-[ -d linux_5_10 ] || git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10
+[ -d linux_5_10 ] || git clone -b v5.10 --depth=1 https://github.com/torvalds/linux/ linux_5_10
 
 # Prepare compile a part of the kernel with CBMC via one-line-scan
 ln -s goto-cc src/goto-cc/goto-ld

From 3b7b19a50463f73126021ea1e9968a38eb22c8fe Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 1 Feb 2022 11:11:31 +0000
Subject: [PATCH 2/2] Codify grouping and order of includes

clang-format supports describing groups of includes via regular
expressions and assigning priorities to them. The include file
corresponding to an implementation will always have priority 0. Other
priorities are now set in the clang-format configuration. Includes not
specified will be auto-assigned INT_MAX as priority.
---
 .clang-format      | 13 ++++++++++++-
 CODING_STANDARD.md |  2 +-
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/.clang-format b/.clang-format
index 126ce95f40e..bf9c440eae0 100644
--- a/.clang-format
+++ b/.clang-format
@@ -47,7 +47,18 @@ NamespaceIndentation: None
 PenaltyBreakString: 10000
 PointerAlignment: Right
 ReflowComments: 'false'
-SortIncludes: 'true'
+IncludeBlocks: Regroup
+IncludeCategories:
+  - Regex: '<util/'
+    Priority: 1
+  - Regex: '<goto-programs/'
+    Priority: 2
+  - Regex: '<.+/.+>'
+    Priority: 3
+  - Regex: '^"[^/]+"$'
+    Priority: 4
+  - Regex: '<[^/]+>'
+    Priority: 5
 SpaceAfterCStyleCast: 'false'
 SpaceBeforeAssignmentOperators: 'true'
 SpaceBeforeParens: Never
diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md
index 884de1277f1..16e9ec2e80f 100644
--- a/CODING_STANDARD.md
+++ b/CODING_STANDARD.md
@@ -148,7 +148,7 @@ Formatting is enforced using clang-format. For more information about this, see
 - The corresponding header for a given source file should always be the *first*
   include in the source file. For example, given `foo.h` and `foo.cpp`, the
   line `#include "foo.h"` should precede all other include statements in
-  `foo.cpp`.
+  `foo.cpp`. clang-format will enforce this.
 - Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`).
   Some of the C headers use macros instead of functions which can have
   unexpected consequences.