[micromega] fix efficiency regression #11263
Conversation
Zimmi48
added
kind: fix
|
@maximedenes , here is the efficiency fix separated from the rest of PR #11047 . |
Thanks a lot, launching a bench! |
|
A bench was already running here: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/818/console |
The numbers look very good, but they don't seem immediately related to the slowdown seen after #11263: some developments are still slower (flocq, coqutil, coquelicot), while some others which were not impacted are now faster (fiat-core). So I'm wondering a bit if this is fixing the introduced performance regression, or just applying another, independent optimization. |
maximedenes
added
the
needs: changelog entry
|
@fajb would you mind adding a changelog entry? Then I can merge it. Thanks a lot for your work! |
|
@maximedenes , I have also modified the standard library to avoid a bootstrapping cycle. PS: I have just rebased adding a changelog. |
|
It seems that the changelog entry fails to compile. It does not seem to follow the standard model. |
|
I wonder why the |
|
fixed changelog. |
plugins/micromega/vect.mli
Outdated
| @@ -22,6 +23,9 @@ type t (** The type of vectors or equivalently linear expressions. | |||
| Moreover, the representation is spare and variables with a zero coefficient | |||
| are not represented. | |||
| *) | |||
| type t | |||
There was a problem hiding this comment.
Why are two aliased types defined here?
There was a problem hiding this comment.
Because otherwise, t gets shadowed in the module Bound module (end of vect.mli)
The problem is that we have reached a limit in the number of stdlib files (this PR adds a new one). #9185 suffered from the same problem and @SkySkimmer fixed it there with commit b4c6277. Such commit could also be cherry-picked in this PR to make the CI pass. @SkySkimmer it would be good to submit as an independent PR that can be merged ASAP too. |
|
OK see #11283 |
|
Ok this should be ready for review [last commit] |
maximedenes
added
part: micromega
|
When I rebase the last commit on top of master, there are conflicts (with the reformatting). I thought we were precisely trying to avoid that, not sure what happened, @ejgallego @Zimmi48 ? |
|
If the rebase is done with |
|
Should be fixed now; should we mark |
ejgallego
force-pushed
the
micromega-fix
branch
from
7c7e935
to
315a3b3
Compare
|
Re-launching a bench to ensure we didn't mess with anything essential in the rebases: https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/822/ |
In the current situation, it isn't exactly one as the extraction command is commented out. Maybe we can reconsider this when we move entirely to Dune and the Dune support for Coq extraction has progressed. |
|
@maximedenes I have just rebased (after removing the dead code you mentioned) |
PR coq#9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes coq#11063 and fixes coq#11242 and fixes coq#11270
maximedenes
force-pushed
the
micromega-fix
branch
from
96603e8
to
7d961a9
Compare
|
@coq/ci-maintainers what are these failing complexity tests? Are they new? They don't seem related to |
|
The open pretyper PR is also having complexity failure, I don't know why though |
|
@coq/ci-maintainers should I ignore the CI failures here? |
|
ping @herbelin (who maintains these complexity tests IIUC) |
|
I'll ignore what looks like a spurious failure and merge. |
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242