Major refactoring of cooking.ml #14727

herbelin · 2021-07-30T20:02:01Z

Kind: Refactoring

Depends on #14726 (merged).

In this PR, all technical code is concentrated in a few functions with the rest of the code simply calling the core functions compositionally.

These functions are:

expand_subst which itself includes:
- expand_constr: expansion of global constants
- subst_univs_level_constr: name-to-de-Bruijn universe renaming
- subst_vars: name-to-de-Bruijn term renaming
abstract_as_type/abstract_as_body: actual generalization

It relies on the following data structures:

universe graph (abstr_uctx, or G)
term context (abstr_ctx, or Δ)
name-to-de-Bruijn universe substitution (abstr_usubst, or τ)
name-to-de-Bruijn term substitution (abstr_subst, or σ)
instance of universe graph (abstr_uinst, or |G|)
instance of term context (abstr_inst, or |Δ|)
expansion maps (expand_info, mapping a c generalized over G' and Δ' to c |G'| |Δ'|)

These data are enough to turn judgements of the form G, Δ ⊢ J into judgements of the form ⊢ ΠG.ΠΔ.(J[σ][τ]).

It includes:

lift_poly_univs: to absorb a universe context in the transformation, that is to reduce the admissibiliy of a rule going from G, Δ ⊢ ΠG'.J to ⊢ ΠG.ΠΔ.(ΠG'.J)[σ][τ]) to the admissibiliy of a rule going from G(G'[ττ']), Δ ⊢ J to ⊢ ΠG(G'[ττ']).ΠΔ.(J[σ][τ]) for a well-chosen τ'
abstract_context: to absorb a term context in the transformation, that is to reduce the admissibiliy of a rule going from G, Δ ⊢ ΠΩ.J to ⊢ ΠG.ΠΔ.((ΠΩ.J)[σ][τ]) to the admissibiliy of a rule going from G, Δ, Ω[σ][τ] ⊢ J to ⊢ ΠG.ΠΔ.Π(Ω[σ][τ]).(J[σ'][τ]) for a well-chosen σ'

Note that the new cooking is "incremental": the cooking data is not global to the section but attached to each declaration. So, in theory, it would be direct to precook all generalizations of a constant/inductive at the time of its declaration (and hence to use them in the section!).

Added / updated documentation of the code

Overlays (relative to the change in PrivatePolymorphic):

herbelin · 2021-07-31T07:46:32Z

kernel/cooking.mli

-val cook_constant : recipe -> cooking_info Opaqueproof.opaque result
-val cook_constr : cooking_info list ->
-  (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
+val cook_opaque_proofterm : cooking_info list ->
+  Opaqueproof.opaque_proofterm -> Opaqueproof.opaque_proofterm
+
+val cook_constant :
+  recipe -> cooking_info Opaqueproof.opaque result

 val cook_inductive :
  cooking_info -> mutual_inductive_body -> mutual_inductive_body

-(** {6 Utility functions used in module [Discharge]. } *)
+val make_cooking_info : expand_info -> named_context -> Univ.UContext.t -> cooking_info
+  (** Abstract a context assumed to be de-Bruijn free for terms and universes *)
+
+val lift_poly_univs : cooking_info -> Univ.AbstractContext.t -> cooking_info * Univ.AbstractContext.t
+
+val abstract_rel_context : cooking_info -> rel_context -> rel_context

-val expmod_constr : work_list -> constr -> constr
+val discharge_proj_repr : abstr_inst_info -> Names.Projection.Repr.t -> Names.Projection.Repr.t


The terminology, cook, or discharge, or abstract, or lift should probably be simplified.

lift_poly_univs and abstract_rel_context do morally the same: they traverse an already-quantified context, respectively a context of universe and a context of terms, updating the cooking info for the remainder of the judgement, and "cooking" this context at the same time.

herbelin · 2021-07-31T07:57:27Z

kernel/cooking.ml

+  | Opaqueproof.PrivateMonomorphic () as priv ->
+    let () = assert (AbstractContext.is_empty info.abstr_info.abstr_uctx) in
+    let () = assert (is_empty_level_subst info.abstr_info.abstr_usubst) in
+    priv


Can't there be private universes also for monomorphic constants?

We don't pass them to cook_constr (see drop_mono in opaqueproof)

I don't understand well the story about PrivateMonomorphic. Is the apparentl loss of information in drop_mono to be related to the extraction of delayed_cst in Safe_typing.add_constant, so that the information is actually not lost?

This data is redundant for the kernel, and only used for vio computation. I have a series of patches that modify this area of the code but I've not submitted them yet because they break weird invariants in Declare that I need to fix first.

herbelin · 2021-08-30T07:22:23Z

I added two further "cleaning" commits. We could do more cleaning, like completely bypassing the type Cooking.result for instance, or imposing more unity in naming.

@ppedrot: would you like to assign?

SkySkimmer

Seems ok overall

SkySkimmer · 2021-09-16T09:46:17Z

kernel/section.ml


 type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
+type section_entry =
+| SecDefinition of Constant.t * constant_body
+| SecInductive of MutInd.t * mutual_inductive_body


I'm not sure it makes sense to have the bodies here. It seems to be used to have access to them in close_section instead of getting them from the revstruct, but couldn't we just look them up in the env0?

We need the hyps of the declaration in Section.segment_entry but not the full bodies. We could indeed use an access to the env instead. I can change it if you insist.

Please change

Commit 9cfdd1e implements your suggestion. It looks a bit strange to recompute a data which we can have at hand for free, but I agree that it makes sense also to have the bodies stored in a unique place, even if there is a cost to get them back.

@SkySkimmer: I'm still a bit afraid of the extra time needed to find again the constant_body and mutual_inductive_body in the environment. Probably not more than a dozen of steps per definition for an environment of several thousands of declarations, so it is maybe a bit unjustified fear, especially considering how lax we are on factorizing the accesses to the environment in many parts of the code, but would you be ok if I would cache back the bodies in the section_entry?

I am only OK if you can show an impact in the bench.

I don't think I could. That would require a huge environment and short definitions so that the time for looking in the environment dominates.

Well, ok, this is globally non-significant, so I leave the PR without the "cache".

kernel/univ.mli

SkySkimmer · 2021-09-16T09:47:59Z

kernel/univ.mli

@@ -484,6 +484,8 @@ val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t ->

 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
+val lift_level_subst : int -> universe_level_subst -> universe_level_subst
+val merge_level_subst : universe_level_subst -> universe_level_subst -> universe_level_subst


This should state the precondition (no common elements, even if they're mapped to the same value) explicitly.
I'm also not sure if it makes sense to have a function with such a precondition in the general API rather than having it defined near its (unique) user.

I don't know. Both approaches are ok to me. In the meantime, I documented it.

SkySkimmer · 2021-09-16T09:51:47Z

kernel/names.ml

@@ -916,14 +916,15 @@ struct
    module HashRepr = Hashcons.Make(Self_Hashcons)
    let hcons = Hashcons.simple_hcons HashRepr.generate HashRepr.hcons (hcons_ind,Id.hcons)

-    let map_npars f p =
+    let map_ind_npars f p =


If this isn't exposed then it should be inlined in map_npars and map

But this would lead to a duplication. Is that what you mean?

I don't think it's really duplication

I tried and I agree that this is clearer by splitting them.

SkySkimmer · 2021-09-16T09:56:47Z

kernel/declarations.ml

+  (** Canonical renaming represented by its domain made of the
+      actual names of the abstracted term variables (e.g. [a,c]);
+      the codomain made of de Bruijn indices is implicit *)
+  abstr_usubst : Univ.universe_level_subst;


Is this not always make_instance_subst abstr_uctx?

The name abstr_uctx is misleading. It is an AbstractContext and, if I'm correct, the orginal uctx levels have been lost. Maybe should it be renamed to abstr_auctx?

SkySkimmer · 2021-09-16T10:05:05Z

kernel/cooking.ml

@@ -315,7 +315,7 @@ let cook_constant env info cb =
 (********************************)
 (* Discharging mutual inductive *)

-let abstract_rel_context cache info ctx =
+let cook_rel_context cache info ctx =


IMO I prefer abstract to cook but it's not a strong preference.

I like abstract also but cook is used many times already.

I like abstract also but cook is used many times already.

Naming isn't a democracy, we can be tyrannical here

SkySkimmer · 2021-09-16T10:10:32Z

The "adding" commits should be merged with the commits introducing the use of the new API imo

herbelin · 2021-09-16T14:01:02Z

@SkySkimmer Thanks a lot for the comments. Next weeks are dense for me but I'll try to reply within a couple of days.

ppedrot · 2021-09-20T08:31:06Z

kernel/declarations.ml

+  expand_info : expand_info;
+  abstr_info : abstr_info;
+  abstr_inst_info : abstr_inst_info; (* relevant for recursive types *)
+  names_info : Id.Set.t; (* set of generalized names *)
 }


I think that there is too much stuff exposed in this API. The datatypes used to live in Cooking and were moved here by @SkySkimmer IIRC but now that we're supposed to preserve more invariants I believe this should be move back under an opaque interface. How doable is this?

It was in opaqueproof, not cooking
b1675a6

Right, right. But now that Opaqueproof is parameterized by this data, it should be easier to put it in Cooking, shouldn't it?

Dependency order goes opaqueproof <- declarations <- cooking so I guess no

This should still be tried nonetheless, I really don't like having all these internal bits exposed to everybody.

A possibility would be to split cooking.ml into two parts:

the low-level infrastructure up to subst_private_univs (and with an abstract export of cooking_info), coming before opaqueproof.ml

the high-level commands cook_constant and cook_inductive coming after declarations (with possible integration to term_typing.ml if we don't want creating an extra file)

At worst, in the higher levels (vernac, tactics, ...) only the field abstr_inst really needs to be visible (and it could as well be hidden behind an access function).

I pushed a commit in this directon, providing a better abstraction of cooking_info. We could abstract even a bit further, depending on feedback.

coqbot-app · 2022-02-07T07:03:41Z

🔴 CI failure at commit cb6d6fc without any failure in the test-suite

✔️ Corresponding job for the base commit 7c608fe succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-fcsl_pcm

You can also pass me a specific list of targets to minimize as arguments.

herbelin · 2022-02-08T20:12:44Z

It seems that the slowdown due to vo size increase (presumably loss of sharing in files) has been magically solved (due to #14924 maybe??) and that the PR is now saving some cycles. Re-running a bench to be sure.

herbelin · 2022-02-09T14:24:04Z

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬─────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]   │   mem faults    │
│                             │                         │                                       │                                       │                          │                 │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD   PDIFF │ NEW  OLD  PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤
│       coq-mathcomp-fingroup │   23.44    23.90  -1.92 │   106805940920    109030214819  -2.04 │   156617263857    156355281519   0.17 │  492776   483636    1.89 │   0    0    nan │
│              coq-coquelicot │   34.12    34.73  -1.76 │   153414999308    155205512585  -1.15 │   202802719577    202093224621   0.35 │  756360   746900    1.27 │   0    0    nan │
│           coq-iris-examples │  419.76   426.83  -1.66 │  1901963591861   1932779022537  -1.59 │  2912478866430   2907160631046   0.18 │ 1179768  1168668    0.95 │   0    0    nan │
│       coq-mathcomp-solvable │   87.39    88.80  -1.59 │   398917190747    404992118468  -1.50 │   612695822822    611691323579   0.16 │  665096   658220    1.04 │   0    0    nan │
│         coq-category-theory │ 1595.94  1615.87  -1.23 │  7289460792992   7381749753737  -1.25 │ 15272287002218  15265692532719   0.04 │ 1491856  1319056   13.10 │   0    0    nan │
│               coq-perennial │ 3951.51  4000.56  -1.23 │ 17915307138687  18139072891573  -1.23 │ 29814680824608  29800333829589   0.05 │ 2631012  2595764    1.36 │   0    0    nan │
│               coq-fiat-core │   55.26    55.83  -1.02 │   235149961848    237472562140  -0.98 │   331329293133    329126657680   0.67 │  481804   477624    0.88 │   0    0    nan │
│                   coq-verdi │   47.93    48.41  -0.99 │   216469840896    218962436658  -1.14 │   323187097116    322533677424   0.20 │  840088   834312    0.69 │   0    0    nan │
│                  coq-flocq3 │   76.36    77.12  -0.99 │   346941211462    349608014580  -0.76 │   456757482737    456073340914   0.15 │  990340   987092    0.33 │   0    0    nan │
│             coq-fiat-crypto │ 2801.57  2828.99  -0.97 │ 12623211416614  12748867114693  -0.99 │ 23285749144716  23305118307774  -0.08 │ 3851392  3851188    0.01 │   0    0    nan │
│                 coq-coqutil │   34.89    35.23  -0.97 │   155973351364    157473446404  -0.95 │   209805834695    208855730940   0.45 │  605640   602028    0.60 │   0    0    nan │
│            coq-fiat-parsers │  336.09   339.17  -0.91 │  1488162454735   1502441971027  -0.95 │  2456687826204   2457388572887  -0.03 │ 2695836  3443080  -21.70 │   0    0    nan │
│      coq-mathcomp-character │   76.48    77.14  -0.86 │   349040052934    352215332474  -0.90 │   530386229317    526227888337   0.79 │  846980   736600   14.99 │   0    0    nan │
│            coq-math-classes │   90.28    90.99  -0.78 │   407411393641    410150389584  -0.67 │   573189761727    572009403315   0.21 │  502944   496004    1.40 │   0    0    nan │
│                    coq-corn │  753.28   758.77  -0.72 │  3414052035393   3438305405424  -0.71 │  5290934018917   5283457995001   0.14 │  876408   874644    0.20 │   0    0    nan │
│      coq-mathcomp-ssreflect │   26.15    26.32  -0.65 │   118299168991    119298867398  -0.84 │   149535244969    149215647035   0.21 │  543648   531424    2.30 │   0    0    nan │
│              coq-verdi-raft │  557.62   561.13  -0.63 │  2538054990629   2553738330443  -0.61 │  3937497714163   3934797022564   0.07 │ 1238008  1230960    0.57 │   0    0    nan │
│       coq-engine-bench-lite │  178.54   179.48  -0.52 │   766529634499    770444905208  -0.51 │  1501005465141   1498003023517   0.20 │ 1304560  1174188   11.10 │   0    0    nan │
│          coq-mathcomp-field │  111.94   112.48  -0.48 │   510821493812    513849502285  -0.59 │   841983738897    837904153362   0.49 │  713016   653856    9.05 │   0    0    nan │
│      coq-mathcomp-odd-order │  552.37   554.77  -0.43 │  2526350741065   2537043994278  -0.42 │  4285944899933   4257070661209   0.68 │ 1216152   933208   30.32 │   0    0    nan │
│                coq-rewriter │  373.61   375.22  -0.43 │  1691198989236   1698620311956  -0.44 │  2775554411492   2776209799708  -0.02 │ 1060812  1060304    0.05 │   0    0    nan │
│                   coq-color │  210.65   211.31  -0.31 │   943988614189    946793583469  -0.30 │  1332544333095   1326284389908   0.47 │ 1113700  1145212   -2.75 │   0    0    nan │
│                  coq-stdlib │  403.56   404.66  -0.27 │  1635006877438   1632747098560   0.14 │  1417093712260   1413418374991   0.26 │  610900   604992    0.98 │   0    0    nan │
│                 coq-bignums │   27.83    27.88  -0.18 │   126333997430    126419819408  -0.07 │   173386626813    173042000047   0.20 │  468944   466460    0.53 │   0    0    nan │
│                     coq-vst │ 1054.79  1056.17  -0.13 │  4778893268602   4785190760743  -0.13 │  7815752108161   7797022841616   0.24 │ 2027156  2071936   -2.16 │   0    0    nan │
│                    coq-hott │  162.12   162.28  -0.10 │   728595888280    731518132588  -0.40 │  1148512666001   1150004602628  -0.13 │  576584   589884   -2.25 │   0    0    nan │
│        coq-mathcomp-algebra │   64.00    64.06  -0.09 │   291202174345    291335724354  -0.05 │   401077289288    398639226267   0.61 │  603284   556124    8.48 │   0    0    nan │
│                    coq-core │   98.70    98.63   0.07 │   394319518909    390056343365   1.09 │   440874824342    440975522738  -0.02 │  273400   274276   -0.32 │   0    0    nan │
│                coq-compcert │  282.14   281.84   0.11 │  1268668769850   1267114404524   0.12 │  1898238385466   1894609928141   0.19 │ 1106008  1097172    0.81 │   0    0    nan │
│                coq-coqprime │   59.94    59.87   0.12 │   271276783711    270596244556   0.25 │   445914237821    445209774748   0.16 │  765068   758036    0.93 │   0    0    nan │
│               coq-fourcolor │ 1497.60  1495.46   0.14 │  6609041479914   6611631136538  -0.04 │ 12116730950312  12087038324002   0.25 │  759664   706812    7.48 │   0    0    nan │
│  coq-performance-tests-lite │  783.51   781.57   0.25 │  3519196159594   3511137536724   0.23 │  5979272809534   5973814259925   0.09 │ 1824604  1825008   -0.02 │   0    0    nan │
│                 coq-unimath │ 3951.56  3940.02   0.29 │ 17966069978711  17920847020480   0.25 │ 35847011675268  35844603379789   0.01 │ 3102220  3322920   -6.64 │   0    0    nan │
│                  coq-geocoq │  692.29   689.91   0.34 │  3147352869258   3137697764730   0.31 │  4958179517993   4951178931605   0.14 │ 1077812  1077856   -0.00 │   0    0    nan │
│ coq-rewriter-perf-SuperFast │  937.12   932.52   0.49 │  4217783112423   4198587366524   0.46 │  7302050701082   7298336157057   0.05 │ 1145584  1148944   -0.29 │   0    0    nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴─────────────────┘
(bedrock2 and metacoq could not be tested)

herbelin · 2022-02-11T08:01:43Z

There is still room for improvement. For instance, the cooking of the variance of universes is still treated separatedly. Also, one may probably want that there is a computation of the actual dependencies in the universe variables of the section, the same way as it is done for declarations of variables. But this can probably go in other PRs.

So, if nothing happens new on this PR by a fews days, I believe it can be considered ready.

kernel/opaqueproof.mli

Includes a suggestion from Gaëtan Gilbert.

All technical code is now concentrated in a few functions with the rest of the code simply calling the core functions compositionally. The functions are: - expand_subst = - expand_constr: expansion of global constants - subst_univs_level_constr: name-to-de-Bruijn universe renaming - subst_vars: name-to-de-Bruijn term renaming - abstract_as_type/abstract_as_body: actual generalization It relies on the following data structures: - universe graph (abstr_auctx, or G) - term context (abstr_ctx, or Δ) - name-to-de-Bruijn universe substitution (abstr_ausubst, or τ) - name-to-de-Bruijn term substitution (abstr_subst, or σ) - instance of universe graph (abstr_uinst, or |G|) - instance of term context (abstr_inst, or |Δ|) - expansion maps (expand_info, mapping a c generalized over G' and Δ' to c |G'| |Δ'|) These data are enough to turn judgements of the form [G, Δ ⊢ J] into judgements of the form [⊢ ΠG.ΠΔ.(J[σ][τ])] It includes: - lift_poly_univs: to absorb a universe context in the transformation, that is to reduce the admissibiliy of a rule going from [G, Δ ⊢ ΠG'.J] to [⊢ ΠG.ΠΔ.(ΠG'.J)[σ][τ])] to the admissibiliy of a rule going from [G(G'[ττ']), Δ ⊢ J] to [⊢ ΠG(G'[ττ']).ΠΔ.(J[σ][τ])] for a well-chosen τ' - abstract_context: to absorb a term context in the transformation, that is to reduce the admissibiliy of a rule going from [G, Δ ⊢ ΠΩ.J] to [⊢ ΠG.ΠΔ.((ΠΩ.J)[σ][τ])] to the admissibiliy of a rule going from [G, Δ, Ω[σ][τ] ⊢ J] to [⊢ ΠG.ΠΔ.Π(Ω[σ][τ]).(J[σ'][τ])] for a well-chosen σ' Note: includes suggestions from Gaëtan Gilbert.

…ency.

…oking_info. New dependency chain: cooking.ml <- opaqueproof.ml <- declarations.ml <- discharge.ml

…step.

ppedrot · 2022-02-13T13:06:45Z

Merging soon.

ppedrot · 2022-02-14T11:25:00Z

@coqbot merge now

coqbot-app · 2022-02-14T11:25:03Z

@ppedrot: Please take care of the following overlays:

14727-herbelin-master+major-refactoring-cooking.sh

herbelin added kind: cleanup Code removal, deprecation, refactorings, etc. part: kernel labels Jul 30, 2021

herbelin added this to the 8.15+rc1 milestone Jul 30, 2021

herbelin requested review from a team as code owners July 30, 2021 20:02

herbelin added the needs: merge of dependency This PR depends on another PR being merged first. label Jul 30, 2021

herbelin force-pushed the master+major-refactoring-cooking branch 2 times, most recently from 8f40105 to f2d4fce Compare July 31, 2021 07:30

herbelin commented Jul 31, 2021

View reviewed changes

herbelin force-pushed the master+major-refactoring-cooking branch from f2d4fce to a778cb2 Compare July 31, 2021 08:02

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 18, 2021

herbelin force-pushed the master+major-refactoring-cooking branch from a778cb2 to 810105a Compare August 18, 2021 15:33

herbelin requested a review from a team as a code owner August 18, 2021 15:33

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 18, 2021

herbelin force-pushed the master+major-refactoring-cooking branch from 810105a to df00348 Compare August 18, 2021 16:09

herbelin removed the needs: merge of dependency This PR depends on another PR being merged first. label Aug 28, 2021

herbelin force-pushed the master+major-refactoring-cooking branch from df00348 to cc583bd Compare August 28, 2021 16:20

ppedrot self-assigned this Aug 30, 2021

SkySkimmer approved these changes Sep 16, 2021

View reviewed changes

ppedrot reviewed Sep 20, 2021

View reviewed changes

herbelin force-pushed the master+major-refactoring-cooking branch from 53f77e9 to fcee31c Compare September 20, 2021 15:21

coqbot-app bot removed the stale This PR will be closed unless it is rebased. label Feb 6, 2022

herbelin force-pushed the master+major-refactoring-cooking branch from 1b4080e to 9c1aa5f Compare February 7, 2022 18:57

herbelin force-pushed the master+major-refactoring-cooking branch from 9c1aa5f to 4ef9d13 Compare February 10, 2022 09:17

Alizter reviewed Feb 11, 2022

View reviewed changes

kernel/opaqueproof.mli Outdated Show resolved Hide resolved

herbelin added 11 commits February 11, 2022 12:36

Small simplification of close_section.

46da9c0

Adding Term.it_mkProd_wo_LetIn.

d905ae2

Adding lift and merge of universe level substitutions.

c69b688

Adapting Projection.map_npars to its actual usage and name.

e6a473b

Includes a suggestion from Gaëtan Gilbert.

Removing useless universe context quantifier size in PrivatePolymorphic.

af28709

Symmetrizing the role of cook_constant and cook_inductive for consist…

f514126

…ency.

More terminology unity in cooking.mli.

1713db5

New file discharge.ml out of cooking.ml, allowing abstracting over co…

de682a2

…oking_info. New dependency chain: cooking.ml <- opaqueproof.ml <- declarations.ml <- discharge.ml

Cooking: expansion of globals and substitution of variables into one …

da87488

…step.

Overlay for elpi and metacoq.

cb1b0ba

herbelin force-pushed the master+major-refactoring-cooking branch from 4ef9d13 to cb1b0ba Compare February 11, 2022 11:43

ppedrot added this to the 8.16+rc1 milestone Feb 12, 2022

coqbot-app bot merged commit b356287 into coq:master Feb 14, 2022

ppedrot mentioned this pull request Feb 14, 2022

Small follow-up of the cooking cleanup #15678

Merged

LasseBlaauwbroek mentioned this pull request Sep 17, 2022

Expose a bit more of the structures in Cooking #16503

Closed

LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Sep 20, 2022

Adapt to coq/coq#14727

d1f4968

LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Sep 20, 2022

Adapt to coq/coq#14727 with help of Pierre-Marie Pédrot in coq/coq#16503

c6ed819

herbelin mentioned this pull request Sep 19, 2023

Discharge on the fly in the kernel #18065

Closed

Major refactoring of cooking.ml #14727

Major refactoring of cooking.ml #14727

Conversation

herbelin commented Jul 30, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

herbelin commented Aug 30, 2021

SkySkimmer left a comment

Choose a reason for hiding this comment

SkySkimmer Sep 16, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

SkySkimmer commented Sep 16, 2021

herbelin commented Sep 16, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

coqbot-app bot commented Feb 7, 2022

herbelin commented Feb 8, 2022

herbelin commented Feb 9, 2022

herbelin commented Feb 11, 2022

ppedrot commented Feb 13, 2022

ppedrot commented Feb 14, 2022

coqbot-app bot commented Feb 14, 2022

herbelin commented Jul 30, 2021 •

edited

Loading

SkySkimmer Sep 16, 2021 •

edited

Loading