Collapse NonLogical thunks in the logic monad. #21247
Conversation
ppedrot
added
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 95.3 96.6 1.2699 1.33% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 95.5 96.7 1.1811 1.24% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 36.4 37.0 0.6153 1.69% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 3.12 3.65 0.5309 17.03% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 16.1 16.6 0.4573 2.83% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 38.1 38.4 0.3773 0.99% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 33.572 33.942 0.3700 1.10% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 34.578 34.934 0.3560 1.03% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 38.7 39.0 0.3421 0.88% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 0.00225 0.336 0.3339 14871.05% 152 coq-mathcomp-analysis/theories/trigo.v.html │ │ 1.16 1.50 0.3339 28.70% 1142 rocq-stdlib/theories/FSets/FMapAVL.v.html │ │ 11.5 11.8 0.3234 2.81% 324 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 11.5 11.8 0.3126 2.72% 388 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 1.55 1.83 0.2842 18.37% 313 rocq-stdlib/theories/Strings/Byte.v.html │ │ 1.06 1.343 0.2830 26.70% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 18.8 19.1 0.2777 1.47% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 0.928 1.20 0.2720 29.29% 408 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 16.2 16.5 0.2655 1.64% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 0.0201 0.282 0.2621 1306.66% 384 coq-mathcomp-analysis/theories/topology_theory/compact.v.html │ │ 0.386 0.648 0.2620 67.93% 249 rocq-stdlib/theories/Structures/OrdersEx.v.html │ │ 0.150 0.400 0.2499 166.92% 592 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.348 0.588 0.2394 68.79% 1 rocq-stdlib/theories/Zmod/ZstarDef.v.html │ │ 4.55 4.78 0.2340 5.14% 2861 rocq-metarocq-safechecker/safechecker/theories/PCUICTypeChecker.v.html │ │ 0.319 0.552 0.2336 73.28% 17 rocq-stdlib/theories/micromega/Env.v.html │ │ 24.9 25.1 0.2214 0.89% 12 coq-fourcolor/theories/proof/job227to230.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 1.81 1.14 -0.6646 -36.75% 330 rocq-metarocq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html │ │ 7.61 7.03 -0.5753 -7.56% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 1.44 1.08 -0.3577 -24.83% 73 rocq-stdlib/theories/Numbers/HexadecimalString.v.html │ │ 0.298 0.00117 -0.2967 -99.61% 202 coq-mathcomp-analysis/theories/normedtype_theory/ereal_normedtype.v.html │ │ 11.6 11.3 -0.2936 -2.54% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 1.46 1.17 -0.2835 -19.47% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 8.56 8.29 -0.2725 -3.18% 1331 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 1.982 1.714 -0.2680 -13.52% 411 coq-vst/veric/mapsto_memory_block.v.html │ │ 0.265 0.000474 -0.2641 -99.82% 383 coq-mathcomp-analysis/theories/topology_theory/compact.v.html │ │ 0.426 0.171 -0.2549 -59.84% 374 rocq-stdlib/theories/Sorting/SetoidList.v.html │ │ 0.603 0.353 -0.2505 -41.52% 17 rocq-stdlib/theories/Logic/IndefiniteDescription.v.html │ │ 7.65 7.40 -0.2484 -3.25% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 2.39 2.14 -0.2431 -10.19% 382 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERCategory.v.html │ │ 0.527 0.292 -0.2351 -44.58% 11 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 28.3 28.1 -0.2332 -0.82% 12 coq-fourcolor/theories/proof/job107to164.v.html │ │ 3.04 2.81 -0.2280 -7.51% 509 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialLam.v.html │ │ 10.1 9.85 -0.2238 -2.22% 279 coq-category-theory/Theory/Metacategory.v.html │ │ 0.222 0.000182 -0.2222 -99.92% 233 rocq-mathcomp-field/field/closed_field.v.html │ │ 0.221 0.000561 -0.2200 -99.75% 558 rocq-mathcomp-field/field/closed_field.v.html │ │ 0.227 0.00864 -0.2189 -96.20% 336 coq-mathcomp-odd-order/theories/BGsection9.v.html │ │ 0.468 0.250 -0.2180 -46.59% 11 rocq-stdlib/theories/Strings/HexString.v.html │ │ 4.87 4.65 -0.2152 -4.42% 121 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 0.216 0.00103 -0.2152 -99.52% 512 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html │ │ 0.534 0.321 -0.2137 -40.01% 1 rocq-stdlib/theories/ZArith/ZNsatz.v.html │ │ 0.220 0.00746 -0.2123 -96.60% 403 coq-mathcomp-odd-order/theories/BGsection5.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
I think there is a (perhaps) unintended change here that allows Ltac2 panics ( AFAICT this PR changes only the behavior of Ltac2 panics produced in |
|
@Janno it's not clear to me what's the intended semantics of the interaction between backtracking and IO, but I'd have naively expected the converse from TC resolution. That is, panics always abort the search and propagate to toplevel, regardless of their origin. In any case, the behaviour should be uniform, even if we decided to catch panics thrown by extern hints in TC search. |
|
I agree with the expectation that panics should always bubble up to the top-level and it seems to me like this PR would achieve this. I cannot come up with another constellation outside of tactics in terms in |
| let run = fun x -> | ||
| try x () with Exception e as src -> | ||
| let (src, info) = Exninfo.capture src in | ||
| Exninfo.iraise (e, info) |
There was a problem hiding this comment.
IIUC the change is because we stop calling this in Proofview.apply, so the Logic_monad.Exception isn't turned into whatever exn we gave to throw, and Proofview.Goal.enter doesn't catch Logic_monad.Exception but did catch the throw exn (it doesn't check fatal_flag, and can't since fatal_flag is currently internal to ltac2).
There is no real point in exposing this implementation detail, all callers immediately evaluate the resulting thunk.
We leverage the fact that a ~> unit -> b ≅ a -> b where ~> stands for a hypothetical pure arrow type. This allows replacing all instances of the NonLogical.t monad in the logic monad type with basically nothing, leaving effects implicits in the rightmost arrow type. Since all clients evaluate the thunk directly, the new code should be equivalent to the previous one. Actually, it may even be more correct given that we already implicitly use the function space in the monadic bind operator to perform side-effects.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
logic-monad-collapse-nonlogical
branch
from
79616bc to
dd3766e
Compare
coqbot-app
bot
removed
the
request: full CI
|
I tweaked Proofview.apply accordingly. The new behaviour should be unchanged, up to the fact that it is now really legal to call effectful thunks in monadic binds. |
| { iolist : 'r. 'i ~> ('e -> 'r) ~> ('a ~> 'o ~> ('e -> 'r) -> 'r) -> 'r } | ||
| Alternatively we could use records but then it would incur a runtime | ||
| overhead. |
There was a problem hiding this comment.
There is another possibility: tuples.
Indeed, as far as the OCaml compiler is concerned, there is no difference between a function taking a single tuple argument and a function taking several arguments. For example, the same machine code is generated for f and g below. (Said otherwise, f actually receives 4 separate arguments, in the same order as g.)
let f (a,b,c,d) = a + b + c + d
let g a b c d = a + b + c + dSo, there is no runtime overhead when using tuples. (Obviously, there is some overhead whenever the caller of f needs to destruct the tuple argument on the fly. But it only happens if the argument comes from outside the caller of f. If the tuple is created before the call to f, the compiler recognizes it and optimizes it away.)
In case you wonder how it can even work when f is used as a closure, that is where the infamous caml_tuplify function comes into play. And since caml_tuplify is generally faster than caml_curry (because the resulting closure cannot be partially applied), there is no runtime overhead either when using closures.
There was a problem hiding this comment.
I checked on return and the OCaml compiler doesn't seem to be able to perform this analysis. It does allocate a tuple and performs projections here and there. It's not so surprising either, all these functions are only known at runtime and there is no way it is going to inline all of them... So maybe it helps in some cases, but most of the combinators defined in this file are not going to be optimized.
We discussed the matter with OCaml experts recently, and it seems that OxCaml lets you write such "pure functions" in a way that is tracked by the type system. Basically you have to write a tuplified function and annotate the type with unboxed to achieve this.
There was a problem hiding this comment.
I do not understand. Are you talking about this kind of code?
type ('a, 'i, 'o, 'e) t = { iolist : 'r. 'i * ('e -> 'r) * ('a -> 'o -> ('e -> 'r) -> 'r) -> 'r }
let return x = { iolist = fun (s, nil, cons) -> cons x s nil }The OCaml compiler does not perform any projection inside the closure stored in iolist. As I explained, it produces the exact same code as if fun s nil cons -> cons x s nil had been written.
There was a problem hiding this comment.
No, I also turned the inner arrow type into tuples.
type ('a, 'i, 'o, 'e) t =
{ iolist : 'r. ('i * ('e -> 'r) * ('a * 'o * ('e -> 'r) -> 'r)) -> 'r }
let return x =
{ iolist = fun (s, nil, cons) -> cons (x, s, nil) }There was a problem hiding this comment.
I see. In that case, there will indeed be some overhead. But do you actually need to turn the inner arrow type into a tuple? You should have complete control over all the callers of this inner function since the type of iolist is not exported. So, you can make sure that it is never partially applied.
4 participants
We leverage the fact that a ~> unit -> b ≅ a -> b where ~> stands for a hypothetical pure arrow type. This allows replacing all instances of the NonLogical.t monad in the logic monad type with basically nothing, leaving effects implicits in the rightmost arrow type. Since all clients evaluate the thunk directly, the new code should be equivalent to the previous one.
Actually, it may even be more correct given that we already implicitly use the function space in the monadic bind operator to perform side-effects.