Gallina quotation functions for Template

[JasonGross]

This is currently on top of many other PRs, and hence is a draft PR. But other than that it's basically ready for review. It's unfortunately kind-of slow (timing info coming soon).

Timing

     Time |   Peak Mem | File Name
------------------------------------------------------------------------------------------------------
28m36.07s | 1742960 ko | Total Time / Peak Mem
------------------------------------------------------------------------------------------------------
 3m30.41s | 1335360 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo
 3m21.62s | 1701848 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo
 1m50.32s | 1606248 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo
 1m25.21s | 1283592 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo
 1m21.88s | 1284000 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo
 1m19.88s | 1742960 ko | ToTemplate/Coq/MSets.vo
 1m15.76s | 1282544 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo
 1m12.04s | 1368088 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo
 0m58.84s | 1057848 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo
 0m56.64s | 1034060 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo
 0m56.61s | 1004488 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo
 0m53.50s | 1016636 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo
 0m51.59s | 1138188 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo
 0m49.75s | 1379420 ko | ToTemplate/Coq/FSets.vo
 0m49.74s | 1107368 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo
 0m42.10s | 1256528 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo
 0m37.84s | 1016312 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo
 0m34.52s | 1013440 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo
 0m22.88s |  852064 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo
 0m21.17s |  877048 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo
 0m19.04s | 1263092 ko | ToTemplate/Common/EnvironmentTyping.vo
 0m18.07s |  841212 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo
 0m17.21s |  834976 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo
 0m15.02s | 1075516 ko | ToTemplate/Template/Typing.vo
 0m14.61s |  905324 ko | ToTemplate/Common/Universes.vo
 0m13.40s |  816856 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo
 0m13.34s |  780536 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo
 0m12.93s |  774728 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo
 0m11.78s |  862636 ko | ToTemplate/Common/Kernames.vo
 0m10.00s |  828792 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo
 0m08.93s |  725948 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo
 0m07.23s |  728332 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo
 0m06.99s |  705852 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo
 0m05.96s |  725548 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo
 0m05.11s |  992248 ko | ToTemplate/Template/TermEquality.vo
 0m04.96s |  761740 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo
 0m04.71s |  932436 ko | ToTemplate/Common/Environment.vo
 0m04.53s |  989628 ko | ToTemplate/Template/WfAst.vo
 0m03.78s |  769156 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo
 0m03.18s |  713016 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo
 0m02.95s |  701344 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo
 0m02.90s |  756624 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo
 0m02.86s |  703056 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo
 0m02.64s |  698816 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo
 0m02.53s |  922916 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo
 0m02.49s |  699500 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo
 0m02.12s |  984776 ko | ToTemplate/Template/Ast.vo
 0m02.01s |  700412 ko | ToTemplate/Coq/Init.vo
 0m01.99s |  701512 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo
 0m01.98s |  704288 ko | ToTemplate/Utils/utils.vo
 0m01.87s |  709068 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo
 0m01.82s |  696724 ko | ToTemplate/Utils/MCUtils.vo
 0m01.63s |  713200 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo
 0m01.62s |  695876 ko | ToTemplate/Init.vo
 0m01.53s |  696780 ko | ToTemplate/Coq/Lists.vo
 0m01.49s |  699684 ko | ToTemplate/Utils/All_Forall.vo
 0m01.43s |  695080 ko | ToTemplate/Utils/MCProd.vo
 0m01.34s |  696508 ko | ToTemplate/Utils/ReflectEq.vo
 0m01.27s |  697288 ko | ToTemplate/Utils/MCOption.vo
 0m01.26s |  980920 ko | ToTemplate/Template/AstUtils.vo
 0m01.23s |  693944 ko | ToTemplate/Coq/Bool.vo
 0m01.22s |  755464 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo
 0m01.20s |  757612 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo
 0m01.19s |  710540 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo
 0m01.18s |  694060 ko | ToTemplate/Utils/MCList.vo
 0m01.15s |  697976 ko | CommonUtils.vo
 0m01.12s |  955240 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo
 0m01.12s |  706104 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo
 0m01.08s |  867856 ko | ToTemplate/Common/BasicAst.vo
 0m01.07s |  695148 ko | ToTemplate/Utils/bytestring.vo
 0m01.06s |  693992 ko | ToTemplate/Utils/MCArith.vo
 0m01.03s |  703564 ko | ToTemplate/Coq/Floats.vo
 0m00.98s |  700584 ko | ToTemplate/Coq/Numbers.vo
 0m00.98s |  694564 ko | ToTemplate/Utils/MCReflect.vo
 0m00.88s |  756228 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo
 0m00.87s |  695256 ko | ToTemplate/Coq/Strings.vo
 0m00.86s |  766292 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo
 0m00.84s |  696340 ko | ToTemplate/Coq/ssr.vo
 0m00.83s |  694736 ko | ToTemplate/Common/Primitive.vo
 0m00.83s |  698224 ko | ToTemplate/Common/config.vo
 0m00.81s |  745564 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo
 0m00.80s |  700668 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo
 0m00.20s |   63332 ko | ToTemplate/Utils/monad_utils.vo
 0m00.08s |   64744 ko | ToTemplate/Utils/MCRelations.vo
 0m00.06s |   64376 ko | ToTemplate/Utils/MCString.vo
 0m00.05s |   64560 ko | ToTemplate/Common/Reflect.vo
 0m00.05s |   63284 ko | ToTemplate/Template/ReflectAst.vo
 0m00.05s |   65008 ko | ToTemplate/Utils/MCPrelude.vo
 0m00.05s |   65068 ko | ToTemplate/Utils/MCSquash.vo
 0m00.04s |   64248 ko | ToTemplate/Template/Induction.vo
 0m00.04s |   64996 ko | ToTemplate/Template/LiftSubst.vo
 0m00.04s |   64736 ko | ToTemplate/Template/UnivSubst.vo
 0m00.04s |   64308 ko | ToTemplate/Utils/MCCompare.vo
 0m00.04s |   63324 ko | ToTemplate/Utils/MCEquality.vo
 0m00.04s |   65020 ko | ToTemplate/Utils/wGraph.vo
 0m00.03s |   64724 ko | ToTemplate/Utils/ByteCompare.vo
 0m00.03s |   63432 ko | ToTemplate/Utils/ByteCompareSpec.vo
 0m00.03s |   64856 ko | ToTemplate/Utils/LibHypsNaming.vo
 0m00.03s |   64768 ko | ToTemplate/Utils/MCPred.vo
 0m00.02s |   65064 ko | ToTemplate/Common/Transform.vo
 0m00.01s |   64484 ko | ToTemplate/Utils/ByteCompare_opt.vo

This is the easier half of establishing the quotation function (required, e.g., for proving Löb's theorem). The ultimate goal is, where x : □X means roughly Σ ;;; [] |- x : X, to prove □(□X → X) → □X. The quotation function should ultimately be □X → □□X, and this PR establishes the ability to go from Σ ;;; [] |- x : X to Ast.term (in Template land; we could probably do the same in PCUIC land without much difficulty).

There's one additional wart, which is that the universe constraints introduced here are inconsistent with those in Template.TypingWf. This also prevents us from writing a quotation function for wf_inductive_body. Working out this kink might require #893, which is still a work in progress, so I figure I'll try to get this merged first, while I try to work out that kink on the side.

Currently blocked on coq/coq#17462, but once I finish minimizing that I expect it should be pretty easy to fix this to work with -vos.

[tabareau]

@JasonGross it seems it is ready to merge now. Is it right ?

[JasonGross]

Yes, indeed, this is ready for merge, assuming there's no objection to the 30 minutes added to build time nor to me adding myself to the authors lists in the .opam files. And thank you for reviewing and merging all my PRs!

[tabareau]

Have you found any obvious bottleneck in compilation time that we can try to understand and fix, or is it more uniformly slow compilation time ?

[JasonGross]

There are some obvious bottlenecks that unfortunately live inside TemplateMonad code that I'm not sure how to profile. (The secondary bottlenecks are functor instantiation lines, where I do Module Foo := Bar ...., which seem even harder to debug.) (The tertiary bottlenecks seem to be in typeclass resolution, when there's one more-or-less obvious solution to the typeclass problem, but resolution spends forever in conversion(?) trying out hundreds of instances that end up not being convertible with the goal. I've done what I can to mitigate this problem already.)

More than 2/3 of the time is spent in the TemplateMonad code for taking a module name, getting the list of identifiers under that module name, and emitting, effectively, Instance q<name> : @quotation_of <type of name> <name> := tConst <string of name>..

The files taking more than 50s are

 3m30.41s | 1335360 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo
 3m21.62s | 1701848 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo
 1m50.32s | 1606248 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo
 1m25.21s | 1283592 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo
 1m21.88s | 1284000 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo
 1m19.88s | 1742960 ko | ToTemplate/Coq/MSets.vo
 1m15.76s | 1282544 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo
 1m12.04s | 1368088 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo
 0m58.84s | 1057848 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo
 0m56.64s | 1034060 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo
 0m56.61s | 1004488 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo
 0m53.50s | 1016636 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo
 0m51.59s | 1138188 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo

I can probably speed up ToTemplate/Coq/MSets.vo a bit by doing some judicious refactoring, maybe shave off 30s. Let me prepare a PR that sets up the infrastructure for doing that. (I'll move all the not-specific-to-quotation code to a new file Utils.MCMSets, and then will just quote some names rather than having to quote bodies. This is probably just kicking the problem down the road; I expect when I get around to trying to prove typing for all the quoted objects, one bottleneck is going to be Quote Recursively on large proofs, but it'll save us some time now.)

The other files are all of roughly the same shape, though. Consider the second slowest, ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v, whose contents is just this:

From Coq.FSets Require Import FMapAVL.
From Coq.Structures Require Import Equalities OrdersAlt.
From MetaCoq.Quotation.ToTemplate Require Import Init.
From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig.
From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapList.Sig.
Import List.ListNotations.
Local Open Scope list_scope.

Module FMapAVL.
  Module Type MakeSig (T : OrderedTypeOrig) := Nop <+ FMapAVL.Make T.

  Module Type QuotationOfMake (T : OrderedTypeOrig) (M : MakeSig T).
    Module qRaw.
      Module qProofs.
        Module qMX := Nop <+ QuotationOfOrderedTypeOrigFacts T M.Raw.Proofs.MX.
        Module qPX := Nop <+ QuotationOfKeyOrderedTypeOrig T M.Raw.Proofs.PX.
        Module qL := Nop <+ FMapList.QuotationOfRaw T M.Raw.Proofs.L.
        Export (hints) qMX qPX qL.
        MetaCoq Run (tmDeclareQuotationOfModule (all_submodules_except [["MX"]; ["PX"]; ["L"]]%bs) (Some export) "M.Raw.Proofs").
      End qProofs.
      Export (hints) qProofs.
      MetaCoq Run (tmDeclareQuotationOfModule (all_submodules_except [["Proofs"]]%bs) (Some export) "M.Raw").
    End qRaw.
    Export (hints) qRaw.
    MetaCoq Run (tmDeclareQuotationOfModule (all_submodules_except [["Raw"]]%bs) (Some export) "M").
  End QuotationOfMake.
End FMapAVL.

The template program tmDeclareQuotationOfModule does a couple of things:

• it gets a list of all identifiers under a given prefix
• it quotes the types of all these identifiers
• it spends a bunch of time hacking around tmDefinition says that MetaCoq tactics are bugged and fail to declare universes #853 and tmUnquote (or tmDefinition) fails to propagate universe constraints  #842, and then some more time trying to find universe replacements that don't result in universe inconsistencies (maybe there's a better strategy involving Unset MetaCoq Strict Unquote Universe Mode and munging the universes systematically rather than in an ad-hoc fashion? I can try reworking this bit of the code)
• based on ad-hoc printf debugging, I think it might also be spending a bunch of time reducing monad_map on very long lists, i.e., in

  metacoq/template-coq/src/template_monad.ml

  Line 255 in 708c53b

  let pgm = Reduction.whd_all env pgm in

  (does this line do fixpoint refolding a la simpl/cbn?)
• it might also be the case that a lot of time is spent in string comparison, to determine which identifiers have a functor in their dirpath and are thus not valid global constants. The code I currently use for doing this is

code for checking if a kername is globalizable

(* returns true if a modpath is suitable for quotation, i.e., does not mention functor-bound arguments *)
Fixpoint modpath_is_absolute (mp : modpath) : bool
  := match mp with
     | MPfile _ => true
     | MPbound _ _ _ => false
     | MPdot mp _ => modpath_is_absolute mp
     end.
Definition kername_is_absolute (kn : kername) : bool
  := modpath_is_absolute (fst kn).
(* gives the dirpath and the reversed list of idents, or None if bound *)
Fixpoint split_common_prefix_ls (mp1 mp2 : list ident) :=
  match mp1, mp2 with
  | [], _ | _, [] => ([], mp1, mp2)
  | i1 :: mp1, i2 :: mp2
    => if i1 == i2
       then let '(common, mp1, mp2) := split_common_prefix_ls mp1 mp2 in
            (i1 :: common, mp1, mp2)
       else ([], mp1, mp2)
  end.
Definition common_prefix_ls (mp1 mp2 : list ident) :=
  let '(common, _, _) := split_common_prefix_ls mp1 mp2 in common.
Fixpoint split_modpath (mp : modpath) : (list ident * (dirpath * option (ident * nat)))
  := match mp with
     | MPfile f => ([], (f, None))
     | MPbound f i idx => ([], (f, Some (i, idx)))
     | MPdot mp i => let '(l, d) := split_modpath mp in (i :: l, d)
     end.
(* returns None if either [mp] shares no prefix with [mp] or either modpath is bound, otherwise returns the list of idents of the common prefix *)
Definition split_common_prefix (mp1 mp2 : modpath) : option ((dirpath * option (ident * nat)) * (list ident * list ident * list ident))
  := match split_modpath mp1, split_modpath mp2 with
     | (mp1, f1), (mp2, f2)
       => if f1 == f2
          then Some (f1, split_common_prefix_ls (rev mp1) (rev mp2))
          else None
     end.
Definition common_prefix (mp1 mp2 : modpath) : option ((dirpath * option (ident * nat)) * list ident)
  := option_map (fun '(f, (common, _, _)) => (f, common)) (split_common_prefix mp1 mp2).
(* Kludge for not having https://github.com/MetaCoq/metacoq/issues/839 *)
Definition modpath_is_okay (cur_modpath : modpath) (mp : modpath) : bool
  := andb (modpath_is_absolute mp)
       match mp with
       | MPfile _ => true
       | MPbound _ _ _ => false
       | MPdot _ _
         => match common_prefix cur_modpath mp with
            | None => true (* it's not part of the current module, so it's fine *)
            | Some (_, []) => true (* only share the top-level, so it can't be a functor *)
            | Some _ => false
            end
       end.
Definition kername_is_okay (cur_modpath : modpath) (kn : kername) : bool
  := modpath_is_okay cur_modpath (fst kn).

I don't know how to really profile template monad code, though, so I didn't spend much time trying to performance optimize this routine.

[JasonGross]

(Also, do @mattam82 @yforster @TheoWinterhalter @MevenBertrand want to weigh in?)

[yforster]

I don't have anything to contribute in profiling I fear.

Regarding the content of the PR, I'm very much in favour. We've been discussing a proof like that for a while and I've been scared that it might be very hard. This PR shows it's indeed very hard, but doable :)

On the other hand, the almost doubled build time is a bit of a problem. We spent a lot of energy on getting MetaCoq's build time down. In the end, it wouldn't be a problem for users installing MetaCoq, because it's in its own package (which is a bit oddly named btw, if I'd just read quotation I wouldn't expect this development I think). But CI is slowed down dramatically. Maybe it's time to figure out a MetaCoq CI similar to Coq's CI that we run before merging PRs, but that's not run on every push?

[TheoWinterhalter]

I was scared for a minute that it would slow down install for users or compile time for developers of other bits, but if not then I guess it's not so terrible.
Maybe we can merge and improve later?

[tabareau]

Ok, changing the CI so that it does run on every push is something we should do anyway.
Let's merge then and change the CI at least.
@JasonGross you need to rebase on your recent refactoring first ?

[MevenBertrand]

I don't have a lot more to add, I think. I'm very happy too that someone took up the challenge of doing this quotation work, well done Jason! And if the slowdown is confined to CI that we run less aggressively than we currently do, but does not affect users or developers that don't touch this new addition it seems like a reasonable price to pay to me – that me can try and mitigate later.

[JasonGross]

@JasonGross you need to rebase on your recent refactoring first ?

No, the recent refactorings are preparatory and do not conflict with this PR. I'll make some follow-up PRs for improving performance, etc.

[JasonGross]

Thank you for merging! 🎉

Maybe it's time to figure out a MetaCoq CI similar to Coq's CI that we run before merging PRs, but that's not run on every push?

It's also possible to make pushes cancel previous instances of the CI that are still running by adding something like

concurrency:
      group: ${{ github.workflow }}-${{ matrix.target }}-${{ github.head_ref || github.run_id }}
      cancel-in-progress: true

(remove ${{ matrix.target }} for the nix builds, which don't use the matrix strategy). cf what we do in Fiat Crypto