Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit 463c4f0

Browse files
committed
fix: include moreLeanArgs in module trace
closes #50
1 parent 3595a56 commit 463c4f0

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

Diff for: Lake/Build/Module.lean

+5-4
Original file line numberDiff line numberDiff line change
@@ -124,10 +124,10 @@ def OleanAndCTarget.activate (self : OleanAndCTarget) : SchedulerM ActiveOleanAn
124124
def moduleTarget
125125
[CheckExists i] [GetMTime i] [ComputeHash i m] [MonadLiftT m BuildM] (info : i)
126126
(leanFile traceFile : FilePath) (contents : String) (depTarget : BuildTarget x)
127-
(build : BuildM PUnit) : BuildTarget i :=
127+
(argTrace : BuildTrace) (build : BuildM PUnit) : BuildTarget i :=
128128
Target.mk info <| depTarget.bindOpaqueSync fun depTrace => do
129129
let srcTrace : BuildTrace := ⟨Hash.ofString contents, ← getMTime leanFile⟩
130-
let fullTrace := (← getLeanTrace).mix <| srcTrace.mix depTrace
130+
let fullTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
131131
let upToDate ← fullTrace.checkAgainstFile info traceFile
132132
unless upToDate do
133133
build
@@ -138,16 +138,17 @@ def moduleOleanAndCTarget
138138
(leanFile cFile oleanFile traceFile : FilePath)
139139
(contents : String) (depTarget : BuildTarget x)
140140
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : OleanAndCTarget :=
141+
let info := OleanAndC.mk oleanFile cFile
141142
let ileanFile := oleanFile.withExtension "ilean"
142-
moduleTarget (OleanAndC.mk oleanFile cFile) leanFile traceFile contents depTarget do
143+
moduleTarget info leanFile traceFile contents depTarget (pureHash leanArgs) do
143144
compileLeanModule leanFile oleanFile ileanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
144145

145146
def moduleOleanTarget
146147
(leanFile oleanFile traceFile : FilePath)
147148
(contents : String) (depTarget : BuildTarget x)
148149
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : FileTarget :=
149150
let ileanFile := oleanFile.withExtension "ilean"
150-
let target := moduleTarget oleanFile leanFile traceFile contents depTarget do
151+
let target := moduleTarget oleanFile leanFile traceFile contents depTarget (pureHash leanArgs) do
151152
compileLeanModule leanFile oleanFile ileanFile none (← getOleanPath) rootDir leanArgs (← getLean)
152153
target.withTask do target.bindSync fun oleanFile depTrace => do
153154
return mixTrace (← computeTrace oleanFile) depTrace

0 commit comments

Comments
 (0)