Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add timing profiling to the new compiler #2187

Merged
merged 1 commit into from
Apr 18, 2023

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Apr 9, 2023

No description provided.

@hargoniX hargoniX force-pushed the hbv_compiler_timing branch 2 times, most recently from a3f7354 to 1fe52ec Compare April 9, 2023 13:42
@Kha
Copy link
Member

Kha commented Apr 16, 2023

I would suggest keeping the trace class as Compiler for now, the new output doesn't seem very helpful when enabling specific classes

@Kha
Copy link
Member

Kha commented Apr 16, 2023

Speaking from a profiling PoV, we should also have a trace node for the entire compiler invocation

@hargoniX
Copy link
Contributor Author

hargoniX commented Apr 16, 2023

I fixed the first part (didn't correct the test traces yet because:) for the second we have:

@[export lean_lcnf_compile_decls]
def main (declNames : List Name) : CoreM Unit := do
  profileitM Exception "compilation new" (← getOptions) do
    CompilerM.run <| discard <| PassManager.run declNames.toArray

right now. What is our policy when the thing already has a profileitM call attach? Do I just trace node it anyways? Do I remove profileit?

@Kha
Copy link
Member

Kha commented Apr 17, 2023

Do I just trace node it anyways?

Yes, the two profilers are completely separate currently

@Kha
Copy link
Member

Kha commented Apr 18, 2023

Then I'll merge this as an improvement to profiling that should not otherwise significantly affect compiler dev experience

@Kha Kha merged commit 36f0acf into leanprover:master Apr 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants