sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: update to c++20 (#12117)

Browse Source 
This PR upgrades Lean's internal toolchain to use C++20 as a preparatory
step for #12044.
This commit is contained in:
Henrik Böving
2026-02-11 02:17:40 +01:00
committed by GitHub
parent d886be121e
commit e5f0d6283a
8 changed files with 17 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
.github/workflows/ci.yml vendored
View File

@@ -260,7 +260,7 @@ jobs:
{ {
"name": "Linux fsanitize", "name": "Linux fsanitize",
// Always run on large if available, more reliable regarding timeouts // Always run on large if available, more reliable regarding timeouts
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest", "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
"enabled": level >= 2, "enabled": level >= 2,
// do not fail nightlies on this for now // do not fail nightlies on this for now
"secondary": level <= 2, "secondary": level <= 2,
@@ -277,7 +277,7 @@ jobs:
// * `grind_guide` always times out. // * `grind_guide` always times out.
// * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
// failures? // failures?
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'" "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|grind_bitvec2|grind_constProp|grind_indexmap|grind_list|grind_lint|grind_array_attach|grind_ite_trace|pkg/|lake/'"
}, },
{ {
"name": "macOS", "name": "macOS",

8
flake.lock generated
View File

@@ -2,11 +2,11 @@
"nodes": { "nodes": {
"nixpkgs": { "nixpkgs": {
"locked": { "locked": {
"lastModified": 1745636243, "lastModified": 1769018530,
"narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=", "narHash": "sha256-S/5RU76BdQ32bbE99a+G9gMuatpVWEvIfeSjEqyoFS4=",
"rev": "f771eb401a46846c1aebd20552521b233dd7e18b", "rev": "88d3861acdd3d2f0e361767018218e51810df8a1",
"type": "tarball", "type": "tarball",
"url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz" "url": "https://releases.nixos.org/nixos/unstable/nixos-26.05pre931542.88d3861acdd3/nixexprs.tar.xz"
}, },
"original": { "original": {
"type": "tarball", "type": "tarball",

2
flake.nix
View File

@@ -18,7 +18,7 @@
# An old nixpkgs for creating releases with an old glibc # An old nixpkgs for creating releases with an old glibc
pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; }; pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
llvmPackages = pkgs.llvmPackages_15; llvmPackages = pkgs.llvmPackages_19;
devShellWithDist = pkgsDist: pkgs.mkShell.override { devShellWithDist = pkgsDist: pkgs.mkShell.override {
stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang; stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;

2
src/CMakeLists.txt
View File

@@ -250,7 +250,7 @@ else()
endif() endif()
if(NOT MSVC) if(NOT MSVC)
set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++14 ${CMAKE_CXX_FLAGS}") set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++20 ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}") set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# smallest+slower | -Oz .. -Os .. -O3 | largest+faster # smallest+slower | -Oz .. -Os .. -O3 | largest+faster

2
src/library/time_task.cpp
View File

@@ -57,7 +57,7 @@ void finalize_time_task() {
time_task::time_task(std::string const & category, options const & opts, name decl) : time_task::time_task(std::string const & category, options const & opts, name decl) :
m_category(category) { m_category(category) {
if (get_profiler(opts)) { if (get_profiler(opts)) {
m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable { m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=, this](second_duration duration) mutable {
sstream ss; sstream ss;
ss << m_category; ss << m_category;
if (decl) if (decl)

4
src/runtime/buffer.h
View File

@@ -72,7 +72,7 @@ public:
m_buffer(reinterpret_cast<T *>(m_initial_buffer)), m_buffer(reinterpret_cast<T *>(m_initial_buffer)),
m_pos(0), m_pos(0),
m_capacity(INITIAL_SIZE) { m_capacity(INITIAL_SIZE) {
std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); }); std::for_each(source.begin(), source.end(), [=, this](T const & e) { push_back(e); });
} }
void ensure_capacity(size_t new_capacity) { void ensure_capacity(size_t new_capacity) {
@@ -85,7 +85,7 @@ public:
buffer & operator=(buffer const & source) { buffer & operator=(buffer const & source) {
clear(); clear();
std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); }); std::for_each(source.begin(), source.end(), [=, this](T const & e) { push_back(e); });
return *this; return *this;
} }

2
src/runtime/interrupt.cpp
View File

@@ -64,7 +64,7 @@ void check_interrupted() {
if (g_cancel_tk) { if (g_cancel_tk) {
inc_ref(g_cancel_tk); inc_ref(g_cancel_tk);
if (lean_io_cancel_token_is_set(g_cancel_tk) && if (lean_io_cancel_token_is_set(g_cancel_tk) &&
!std::uncaught_exception()) { !std::uncaught_exceptions()) {
throw interrupted(); throw interrupted();
} }
} }

10
src/util/list_fn.h
View File

@@ -125,7 +125,7 @@ list<T> append(list<T> const & l1, list<T> const & l2) {
/** \brief Given list <tt>(a_0, ..., a_k)</tt>, return list <tt>(f(a_0), ..., f(a_k))</tt>. */ /** \brief Given list <tt>(a_0, ..., a_k)</tt>, return list <tt>(f(a_0), ..., f(a_k))</tt>. */
template<typename To, typename From, typename F> template<typename To, typename From, typename F>
list<To> map2(list<From> const & l, F && f) { list<To> map2(list<From> const & l, F && f) {
static_assert(std::is_same<typename std::result_of<F(From const &)>::type, To>::value, static_assert(std::is_same<typename std::invoke_result<F(From const &)>::type, To>::value,
"map: return type of f is not equal to input type"); "map: return type of f is not equal to input type");
if (is_nil(l)) { if (is_nil(l)) {
return list<To>(); return list<To>();
@@ -271,7 +271,7 @@ list<T> map_reuse(list<T> const & l, F && f, Eq const & eq = Eq()) {
/** \brief Given list <tt>(a_0, ..., a_k)</tt>, exec f(a_0); f(a_1); ... f(a_k)</tt>. */ /** \brief Given list <tt>(a_0, ..., a_k)</tt>, exec f(a_0); f(a_1); ... f(a_k)</tt>. */
template<typename T, typename F> template<typename T, typename F>
void for_each(list<T> const & l, F && f) { void for_each(list<T> const & l, F && f) {
static_assert(std::is_same<typename std::result_of<F(T const &)>::type, void>::value, static_assert(std::is_same<typename std::invoke_result<F(T const &)>::type, void>::value,
"for_each: return type of f is not void"); "for_each: return type of f is not void");
typedef typename list<T>::cell cell; typedef typename list<T>::cell cell;
cell * it = l.raw(); cell * it = l.raw();
@@ -285,7 +285,7 @@ void for_each(list<T> const & l, F && f) {
exec f(a_0, b_0); f(a_1, b_1); ... f(a_k, b_k)</tt>. */ exec f(a_0, b_0); f(a_1, b_1); ... f(a_k, b_k)</tt>. */
template<typename T1, typename T2, typename F> template<typename T1, typename T2, typename F>
void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) { void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
static_assert(std::is_same<typename std::result_of<F(T1 const &, T2 const &)>::type, void>::value, static_assert(std::is_same<typename std::invoke_result<F(T1 const &, T2 const &)>::type, void>::value,
"for_each2: return type of f is not void"); "for_each2: return type of f is not void");
typedef typename list<T1>::cell cell1; typedef typename list<T1>::cell cell1;
typedef typename list<T2>::cell cell2; typedef typename list<T2>::cell cell2;
@@ -303,7 +303,7 @@ void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
exec f(a_0, b_0, c_0); f(a_1, b_1, c_1); ... f(a_k, b_k, c_k)</tt>. */ exec f(a_0, b_0, c_0); f(a_1, b_1, c_1); ... f(a_k, b_k, c_k)</tt>. */
template<typename T1, typename T2, typename T3, typename F> template<typename T1, typename T2, typename T3, typename F>
void for_each3(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F && f) { void for_each3(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F && f) {
static_assert(std::is_same<typename std::result_of<F(T1 const &, T2 const &, T3 const &)>::type, void>::value, static_assert(std::is_same<typename std::invoke_result<F(T1 const &, T2 const &, T3 const &)>::type, void>::value,
"for_each2: return type of f is not void"); "for_each2: return type of f is not void");
typedef typename list<T1>::cell cell1; typedef typename list<T1>::cell cell1;
typedef typename list<T2>::cell cell2; typedef typename list<T2>::cell cell2;
@@ -322,7 +322,7 @@ void for_each3(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F
/** \brief Compare two lists using the binary predicate p. */ /** \brief Compare two lists using the binary predicate p. */
template<typename T, typename P> template<typename T, typename P>
bool compare(list<T> const & l1, list<T> const & l2, P && p) { bool compare(list<T> const & l1, list<T> const & l2, P && p) {
static_assert(std::is_same<typename std::result_of<P(T const &, T const &)>::type, bool>::value, static_assert(std::is_same<typename std::invoke_result<P(T const &, T const &)>::type, bool>::value,
"compare: return type of f is not bool"); "compare: return type of f is not bool");
auto it1 = l1.begin(); auto it1 = l1.begin();
auto it2 = l2.begin(); auto it2 = l2.begin();