search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

BLOCKED: refactor: reimplement initNextStep without evalTactic #219

Open alexkeizer opened 1 month ago

alexkeizer commented 1 month ago

Description:

Work in progress: this currently causes a slowdown, more investigation is needed.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

alexkeizer commented 1 month ago

I'm going a bit mad with this instantiateMVars nonsense. Compare a profile from #214 with a profile from the current PR --- both are running the SHA512_225 benchmark.

You'll notice the former takes 8 seconds in total, of which 1.2 is spent on init_next_step. That was the motivation for this PR. Indeed, in the profile for this PR, initNextStep doesn't even make the profiler's threshold, but we can see that we spend much less time executing the tactic (the Elab.step: tacticSym_n___ node was about 3.3 seconds before, and is 1.1 seconds now; a difference of exactly 1.2 seconds).

However, all of that is lost on the metavariable instantiation. This profile was made with a toolchain version that doesn't have a node for instantiatMVar, but we can deduce how much is spent on it from the self time of Elab.command: this was 3.8 seconds, and has now blown up to 11.7 seconds.

alexkeizer commented 3 weeks ago

This is currently blocked, waiting on a diagnosis of https://github.com/leanprover/lean4/issues/5610