Michael Soegtrop (Sep 06 2020 at 07:49): Michael Soegtrop (Sep 06 2020 at 07:49):Out of curiosity I looked at the universe constraints for an arbitrary predefined tactic. A the end of the tactics tutorial I did a Check Intro_cont.
intro_cont@{tactics.14888 tactics.14889 tactics.14890 tactics.14891 tactics.14892
tactics.14893 tactics.14894 tactics.14895 tactics.14896 tactics.14897
tactics.14898 tactics.14899 tactics.14900 tactics.14901 tactics.14902
tactics.14903 tactics.14904 tactics.14905 tactics.14906 tactics.14907
tactics.14908 tactics.14909 tactics.14910 tactics.14911 tactics.14912
tactics.14913 tactics.14914 tactics.14915 tactics.14916 tactics.14917
tactics.14918 tactics.14919 tactics.14920 tactics.14921 tactics.14922
tactics.14923 tactics.14924 tactics.14925 tactics.14926 tactics.14927
tactics.14928 tactics.14929 tactics.14930 tactics.14931 tactics.14932
tactics.14933 tactics.14934 tactics.14935 tactics.14936 tactics.14937
tactics.14938 tactics.14939 tactics.14940 tactics.14941 tactics.14942
tactics.14943 tactics.14944 tactics.14945 tactics.14946 tactics.14947
tactics.14948 tactics.14949 tactics.14950 tactics.14951 tactics.14952
tactics.14953 tactics.14954 tactics.14955 tactics.14956 tactics.14957
tactics.14958 tactics.14959 tactics.14960 tactics.14961 tactics.14962
tactics.14963 tactics.14964 tactics.14965 tactics.14966 tactics.14967
tactics.14968
tactics.14969}
: (?A -> gtactic@{tactics.14906 tactics.14906 tactics.14907 tactics.14906} ?B) ->
gtactic@{tactics.14906 tactics.14906 tactics.14907 tactics.14906} ?B
where
?A : [ |- Type@{tactics.14888}]
?B : [ |- Type@{tactics.14906}]
(* {tactics.14969 tactics.14968 tactics.14967 tactics.14966 tactics.14965 tactics.14964 tactics.14963 tactics.14962 tactics.14961 tactics.14960 tactics.14959 tactics.14958 tactics.14957 tactics.14956 tactics.14955 tactics.14954 tactics.14953 tactics.14952 tactics.14951 tactics.14950 tactics.14949 tactics.14948 tactics.14947 tactics.14946 tactics.14945 tactics.14944 tactics.14943 tactics.14942 tactics.14941 tactics.14940 tactics.14939 tactics.14938 tactics.14937 tactics.14936 tactics.14935 tactics.14934 tactics.14933 tactics.14932 tactics.14931 tactics.14930 tactics.14929 tactics.14928 tactics.14927 tactics.14926 tactics.14925 tactics.14924 tactics.14923 tactics.14922 tactics.14921 tactics.14920 tactics.14919 tactics.14918 tactics.14917 tactics.14916 tactics.14915 tactics.14914 tactics.14913 tactics.14912 tactics.14911 tactics.14910 tactics.14909 tactics.14908 tactics.14907 tactics.14906 tactics.14905 tactics.14904 tactics.14903 tactics.14902 tactics.14901 tactics.14900 tactics.14899 tactics.14898 tactics.14897 tactics.14896 tactics.14895 tactics.14894 tactics.14893 tactics.14892 tactics.14891 tactics.14890 tactics.14889 tactics.14888} |=
Set < tactics.14898
Set < tactics.14904
Set < tactics.14906
Set < tactics.14922
Set < tactics.14937
Set < tactics.14941
Set < tactics.14954
Set < tactics.14967
tactics.14888 < tactics.14893
tactics.14888 < tactics.14925
tactics.14895 < tactics.14898
tactics.14896 < tactics.14897
tactics.14903 < tactics.14892
tactics.14907 < tactics.14906
tactics.14910 < tactics.14909
tactics.14920 < tactics.14921
tactics.14923 < tactics.14922
tactics.14927 < tactics.14926
tactics.14928 < tactics.14926
tactics.14933 < tactics.14932
tactics.14934 < tactics.14932
tactics.14938 < tactics.14937
tactics.14947 < tactics.14946
tactics.14951 < tactics.14954
tactics.14952 < tactics.14953
tactics.14959 < tactics.14941
tactics.14965 < tactics.14966
tactics.14968 < tactics.14967
tactics.14888 <= tactics.14907
tactics.14893 <= tactics.14892
tactics.14893 <= tactics.14909
tactics.14894 <= tactics.14892
tactics.14894 <= tactics.14896
tactics.14898 <= tactics.14896
tactics.14900 <= tactics.14903
tactics.14901 <= tactics.14903
tactics.14902 <= tactics.14903
tactics.14906 <= tactics.14893
tactics.14907 <= tactics.14926
tactics.14907 <= tactics.14932
tactics.14919 <= tactics.14920
tactics.14922 <= tactics.14920
tactics.14937 <= tactics.14893
tactics.14938 <= tactics.14907
tactics.14940 <= tactics.14941
tactics.14942 <= tactics.14941
tactics.14942 <= tactics.14946
tactics.14943 <= tactics.14941
tactics.14943 <= tactics.14952
tactics.14944 <= tactics.14959
tactics.14954 <= tactics.14952
tactics.14960 <= tactics.14959
tactics.14961 <= tactics.14959
tactics.14964 <= tactics.14965
tactics.14967 <= tactics.14965 *)
I wonder how fast this grows and when it becomes performance wise problematic. I have read section 6.3 of your ICFP paper and did expect that the constraint list would be shorter cause of the measures you took.
Janno (Sep 06 2020 at 18:23):8.13 (specifically https://github.com/coq/coq/pull/12449) will address this problem. You can expect the number of universes on general Mtac2 definitions to drop by 30% and on tactics that solve Prop goals by as much as 95%.
Michael Soegtrop (Sep 07 2020 at 07:46):Thanks - nice that issues are fixed before I run into them :-) It guess it needs a bit of experimenting to see where one ends up in terms of universe constraint checking in 8.12 and later in 8.13.
Beta Ziliani (Sep 07 2020 at 13:29):well, I won't say they are fixed. we need to allocate time to better study universes, although Janno did a great job.
Michael Soegtrop (Sep 07 2020 at 13:33):Is there a way to profile how much time is going into universe constraint checking?
Beta Ziliani (Sep 07 2020 at 13:34):@Janno can answer this properly. IIRC the time is definitively measurable.
Janno (Sep 07 2020 at 13:44):It very much depends on the tactic but the overhead of creating new universes (when instantiating a polymorphic tactic) and substituting universes (initially and during reduction) can account for as much as 50% of the entire execution time. Which is why I have been pushing for Coq to reduce the number of (almost entirely useless) universes being generated. Once can easily achieve a double digit speed-up in some Mtac2 code by annotating universes by hand. But that is generally intractable, given the huge number of universes that even basic constructions have.
Michael Soegtrop (Sep 07 2020 at 13:45):I guess even with 8.12 it will under the line still be faster than Ltac1. The main issue with Ltac1 I have, both from a runtime and coding time / complexity point of view is that for each match one first has to bring the goal / whatever term into the right shape to match it. This usually requires a lot of cbn and manual unfolds which is slow and unreliable. I guess I can do a lot of universe constraint checking for the time I save by removing cbn and having the unifier to the work. What I don't know is how it scales with the complexity of the tactics.
Janno (Sep 07 2020 at 13:49):Yes. And even if Mtac2 is a bit slower because of universes I tend to prefer it to Ltac1/Ltac2 simply because the types keep me sane when I need to refactor the tactic. And I always do eventually need to refactor it..
Janno (Sep 07 2020 at 13:51):What I don't know is how it scales with the complexity of the tactics.
The scaling is basically linear but it is hideous in practice because many of our basic constructions have dozens if not hundreds of universes and every single occurrence gets assigned almost entirely fresh universes.
Janno (Sep 07 2020 at 13:53):Also, since you mention reduction: you can easily beat the unification algorithm in terms of performance if you carefully reduce your terms. That is not usually where the performance benefits come from. The real benefit in my code, usually, is that we do not need to re-check the proof term. (Note: I think current master and the 8.11/8.12 branches perform typechecking but I am hopeful we can disable it entirely soon.)
Janno (Sep 07 2020 at 13:54):To clarify: even with the typechecking of the final proof term, Mtac2 still skips all the intermediate typechecking that Ltac1 performs in basically every tactic.
Michael Soegtrop (Sep 07 2020 at 13:57):And I always do eventually need to refactor it.
Yes, this is indeed a major benefit. And I even think that writing the tactics upfront is in the end faster - of cause it is really tough to write this - especially for beginners - but then debugging Ltac1 is also not exactly fun and making Ltac1 tactics robust is always a lot of work. So while it is much faster to get some prototype to work with Ltac1, I guess getting a production system ready is faster with Mtac2.
Janno (Sep 07 2020 at 13:59):I think that matches my experience. Sadly, Ltac2 is hardly any better. (Or maybe I am just unlucky enough to always run into the unsolved problems of every single piece of software I touch.)
Michael Soegtrop (Sep 07 2020 at 14:17):Well Ltac2 is in so far better than Ltac1 that it is a properly typed ML style language - Ltac1 really has rather obscure hacks - like the decision if a tactic returns a tactic or a term. I guess the goal is to get it over time close to OCaml. I would say a heavily algorithmic tactic which mostly works on its own data structures and has a rather light weight interface to Coq terms I would write in Ltac2 - also because I think it is easier to replace it with OCaml later.
The main advantage of Mtac2 I see is writing tactics which wrangle complicated dependently typed Coq terms.
I definitely also see cases where Coq-Elpi is the best choice, say a high end symbolic integrator, although I would probably write the inner most tactics in Mtac2 - if this is possible.
Last updated: Feb 06 2023 at 07:03 UTC