Skip to content

Commit 5a123dc

Browse files
KhaKha
committed
chore: adjust for stage 2
1 parent 54994f3 commit 5a123dc

4 files changed

Lines changed: 25 additions & 20 deletions

File tree

‎CMakeLists.txt‎

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ foreach(var ${vars})
1212
get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
1313
if("${var}" MATCHES "STAGE0_(.*)")
1414
list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
15+
elseif("${var}" MATCHES "STAGE1_(.*)")
16+
list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
1517
elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
1618
list(APPEND CL_ARGS "-D${var}=${${var}}")
1719
if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
@@ -77,26 +79,29 @@ if (USE_MIMALLOC)
7779
list(APPEND EXTRA_DEPENDS mimalloc)
7880
endif()
7981

80-
ExternalProject_add(stage0
81-
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
82-
SOURCE_SUBDIR src
83-
BINARY_DIR stage0
84-
# do not rebuild stage0 when git hash changes; it's not from this commit anyway
85-
# (however, CI will override this as we need to embed the githash into the stage 1 library built
86-
# by stage 0)
87-
CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
88-
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
89-
INSTALL_COMMAND "" # skip install
90-
DEPENDS ${EXTRA_DEPENDS}
91-
)
82+
if (NOT STAGE1_PREV_STAGE)
83+
ExternalProject_add(stage0
84+
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
85+
SOURCE_SUBDIR src
86+
BINARY_DIR stage0
87+
# do not rebuild stage0 when git hash changes; it's not from this commit anyway
88+
# (however, CI will override this as we need to embed the githash into the stage 1 library built
89+
# by stage 0)
90+
CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
91+
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
92+
INSTALL_COMMAND "" # skip install
93+
DEPENDS ${EXTRA_DEPENDS}
94+
)
95+
list(APPEND EXTRA_DEPENDS stage0)
96+
endif()
9297
ExternalProject_add(stage1
9398
SOURCE_DIR "${LEAN_SOURCE_DIR}"
9499
SOURCE_SUBDIR src
95100
BINARY_DIR stage1
96-
CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
101+
CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
97102
BUILD_ALWAYS ON
98103
INSTALL_COMMAND ""
99-
DEPENDS stage0
104+
DEPENDS ${EXTRA_DEPENDS}
100105
STEP_TARGETS configure
101106
)
102107
ExternalProject_add(stage2

‎src/Init/Prelude.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1840,7 +1840,7 @@ theorem Nat.le_of_succ_le_succ {n m : Nat} : LE.le (succ n) (succ m) → LE.le n
18401840
theorem Nat.le_of_lt_succ {m n : Nat} : LT.lt m (succ n) → LE.le m n :=
18411841
le_of_succ_le_succ
18421842

1843-
protected theorem Nat.eq_or_lt_of_le : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.lt n m)
1843+
protected def Nat.eq_or_lt_of_le : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.lt n m)
18441844
| zero, zero, _ => Or.inl rfl
18451845
| zero, succ _, _ => Or.inr (Nat.succ_le_succ (Nat.zero_le _))
18461846
| succ _, zero, h => absurd h (not_succ_le_zero _)

‎src/Init/WF.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
4040
namespace Acc
4141
variable {α : Sort u} {r : α → α → Prop}
4242

43-
theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
43+
def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
4444
h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
4545

4646
end Acc
@@ -73,7 +73,7 @@ class WellFoundedRelation (α : Sort u) where
7373
wf : WellFounded rel
7474

7575
namespace WellFounded
76-
theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
76+
def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
7777
wf.rec (fun p => p) a
7878

7979
section
@@ -162,10 +162,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
162162
subst x
163163
apply ih (f y) lt y rfl
164164

165-
theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
165+
def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
166166
accAux f ac a rfl
167167

168-
theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
168+
def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
169169
⟨fun a => accessible f (apply h (f a))⟩
170170
end InvImage
171171

‎src/Std/Sat/AIG/RefVec.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
7373
@[simp]
7474
theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len)
7575
(h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size) :
76-
(s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := by rfl
76+
(s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := rfl
7777

7878
@[simp]
7979
theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :

0 commit comments

Comments
 (0)