You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
provides the experimental `postprocess_traces tracePostprocessor in cmd` command, which is useful for working with large trees of trace nodes. It runs the command `cmd` and then transforms the traces using a function `tracePostprocessor`. The transformation can affect which nodes are expanded or collaped by default, it can change messages of the trace nodes, and it can add or delete nodes.
220
223
Example:
@@ -434,6 +437,9 @@ Relatedly, [#13637](https://github.com/leanprover/lean4/pull/13637) splits the o
fixes a `grind` regression on goals that use a bit-vector literal written with `#` syntax under a quantifier, such as `example (f g : Nat → BitVec 2) (h : ∀ n, f n = g n ||| 1#2) : f 0 = g 0 ||| 1#2 := by grind`. The tactic failed with a kernel error instead of closing the goal.
makes `infer_lambda` and `infer_let` check a binder's type, and for `let` also its value, before adding the corresponding declaration to the local context, which is what `infer_pi` already did. No valid declaration changes behavior.
is a hardening pass over the kernel. None of these commits fixes a bug reachable from ordinary Lean code: each one takes an invariant the kernel already depends on and checks it locally instead of assuming it holds elsewhere. The intent is that a future mistake in a neighbouring part of the kernel surfaces as a clean error rather than being amplified.
makes the kernel compare the structurenamewhendecidingwhethertwoprojectionexpressionsaredefinitionallyequal.Both `type_checker::is_def_eq_core` and `equiv_manager::is_equiv_core` compared only the projection index and the projected expression, ignoring `proj_sname`.
fixes a kernel bug: an inductivedeclarationcouldreferenceoneoftheauxiliarytypesthekernelgenerateswheneliminatingnestedinductives,andendupwith a stored constructor type that is ill typed. Such a declaration can only be produced with metaprogramming.
makes the inductivecheckertestaresultinguniverseforzerouptonormalization,sothat `Sort (imax 10)` and `Sort0` describe the same inductivetype.Thetwospellingspreviouslydisagreedonwhetheraconstructorfieldmaycarrydata,onwhethertherecursoreliminatesonlyinto `Prop`,andonwhetherthetypeisaK-likereductiontarget.Onlydeclarationsproducedwith metaprogramming are affected, since the elaborator normalizes levels before the kernel sees them.
fixes a kernel bug: a type whose sort is `Prop` only after universe normalization, such as `Sort (imax 10)`, was not recognized as a proposition, so the kernel allowed a non-proof field to be projected out of a proof. Such a declaration cannot be written in surface syntax and can only be produced with metaprogramming, and `nanoda` rejects it.
fixes a soundness bug in the module system. A `partial` definition lost its `partial` marking when it crossed a module boundary, so downstream modules could use it from safe declarations. This issue can only be exploited usingmeta-programming.
checks that declarations in a mutual block use the same universe parameters. The elaborator already enforces this invariant, but meta-programming can bypass it.
adds a missing `check_no_metavar_no_fvar` checks to the kernel inductivetypemodule.Withoutit,userscouldusemetaprogrammingtosneakinnestedinductivedeclarationscontainingfreevariablesormetavariables.NotethatComparatorwouldcatchthisexploit,sincelean4exportrefusestoexportdeclarationscontainingfreevariablesormetavariables.
implements a minor optimization at `withExporting/withoutExporting`. When they call `modifyEnv` to toggle `Environment.isExporting`, and `MonadEnv` `MetaM`'s `modifyEnv` wipes all `Core` and `Meta` caches.
0 commit comments