Guard against parser modification in interp phase #20674
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
stronger-synterp-flag
branch
from
8829df4 to
3b084a5
Compare
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
|
@gares I get this error in elpi tests which does seem like a bug in elpi: full backtrace The object https://github.com/LPCIC/coq-elpi/blob/fa88643771a2a37eb351f714b04289b73f277b4d/src/rocq_elpi_builtins.ml#L1016-L1018 changes the grammar but is declared Interp and I guess is called from Interp code. Failure in hb_test goes through the same code |
|
🏁 Bench results: 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 12.9 13.7 0.8213 6.38% 571 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 10.3 10.9 0.5898 5.75% 559 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 44.6 45.1 0.5248 1.18% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 1.53 2.03 0.5035 32.90% 42 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 43.0 43.4 0.4507 1.05% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 78.4 78.8 0.4295 0.55% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 9.11 9.44 0.3285 3.60% 434 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 5.30 5.62 0.3248 6.13% 705 rocq-mathcomp-field/field/algebraics_fundamentals.v.html │ │ 15.2 15.5 0.2880 1.89% 620 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │ │ 5.90 6.18 0.2811 4.76% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v.html │ │ 8.54 8.80 0.2636 3.09% 199 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 21.0 21.3 0.2600 1.24% 479 rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html │ │ 15.4 15.7 0.2465 1.60% 618 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │ │ 4.33 4.58 0.2438 5.63% 603 rocq-mathcomp-field/field/algebraics_fundamentals.v.html │ │ 7.73 7.97 0.2411 3.12% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 28.6 28.8 0.2366 0.83% 146 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 58.3 58.5 0.2330 0.40% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 17.8 18.0 0.2234 1.26% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 26.7 27.0 0.2231 0.83% 149 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 0.468 0.690 0.2223 47.55% 340 coq-mathcomp-analysis/theories/lebesgue_measure.v.html │ │ 23.1 23.3 0.2022 0.88% 12 coq-fourcolor/theories/proof/job554to562.v.html │ │ 3.13 3.33 0.2008 6.41% 674 rocq-mathcomp-field/field/algebraics_fundamentals.v.html │ │ 0.486 0.683 0.1978 40.74% 10 rocq-mathcomp-character/character/vcharacter.v.html │ │ 17.1 17.3 0.1817 1.06% 12 coq-fourcolor/theories/proof/job623to633.v.html │ │ 9.84 10.0 0.1794 1.82% 279 coq-category-theory/Theory/Metacategory.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 201 199 -2.0299 -1.01% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 22.1 21.4 -0.7556 -3.41% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 17.9 17.4 -0.5267 -2.94% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 236 236 -0.5159 -0.22% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 92.2 91.8 -0.3793 -0.41% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 19.3 18.9 -0.3767 -1.95% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 117 117 -0.3607 -0.31% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 21.0 20.6 -0.3570 -1.70% 40 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html │ │ 19.0 18.7 -0.3092 -1.63% 708 coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html │ │ 54.0 53.7 -0.3042 -0.56% 424 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 65.2 64.9 -0.2821 -0.43% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 21.6 21.3 -0.2784 -1.29% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 11.8 11.6 -0.2635 -2.23% 388 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 24.0 23.7 -0.2617 -1.09% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 15.4 15.1 -0.2576 -1.68% 417 coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html │ │ 11.9 11.7 -0.2468 -2.07% 324 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 6.70 6.46 -0.2340 -3.49% 1288 coq-mathcomp-analysis/theories/derive.v.html │ │ 26.7 26.5 -0.2243 -0.84% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 133 133 -0.2213 -0.17% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 43.423 43.205 -0.2180 -0.50% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 41.9 41.7 -0.2173 -0.52% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 22.4 22.2 -0.2089 -0.93% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 3.55 3.34 -0.2065 -5.82% 957 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html │ │ 0.199 0.000175 -0.1984 -99.91% 16808 coq-coqprime/src/Coqprime/examples/BasePrimes.v.html │ │ 98.8 98.6 -0.1978 -0.20% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🔴 CI failures at commit 3b084a5 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 4043e70 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
@SkySkimmer this is a call to add-abbreviation-for-tactic. My hope was that it had no synterp action, a bit like abbreviations for regular terms. Eg MLCode(Pred("coq.notation.add-abbreviation-for-tactic",
In(B.string,"Name",
In(B.string,"TacticName",
CIn(CConv.(!>>) B.list tactic_arg,"FixedArgs",
Full(proof_context, {|Declares a parsing rule similar to
Notation Name X1..Xn := ltac:(elpi TacticName FixedArgs (X1)..(Xn))
so that Name can be used in the middle of a term to invoke an
elpi tactic. While FixedArgs can contain str, int, and trm all
other arguments will necessarily be terms, and their number is
not fixed (the user can pass as many as he likes).
The tactic receives as the elpi.loc attribute the precise location
at which the term is written (unlike if a regular abbreviation was
declared by hand).
A call to coq.notation.add-abbreviation-for-tactic TacName TacName []
is equivalent to Elpi Export TacName.|})))),
(fun name tacname more_args ~depth { options} _ -> grab_global_env "coq.notation.add-abbreviation-for-tactic" (fun state ->
...I think I could make it also available in the synterp phase to that one cann announce it, but it is really necessary? This is the code that triggers it let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = more_args } =
let action args loc =
let open Ltac_plugin in
let tac =
let open Tacexpr in
let elpi_tac = {
mltac_plugin = "rocq-elpi.elpi";
mltac_tactic = "elpi_tac"; } in
let elpi_tac_entry = {
mltac_name = elpi_tac;
mltac_index = 0; } in
let more_args = more_args |> List.map (function
| Rocq_elpi_arg_HOAS.Tac.Int _ as t -> t
| Rocq_elpi_arg_HOAS.Tac.String _ as t -> t
| Rocq_elpi_arg_HOAS.Tac.Term (t,_) ->
let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in
let rec aux () ({ CAst.v } as orig) = match v with
| Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None)
| _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in
Rocq_elpi_arg_HOAS.Tac.Term (aux () expr)
| _ -> assert false) in
let tacname = loc, tacname in
let tacname = Genarg.in_gen (Genarg.rawwit Rocq_elpi_arg_syntax.wit_qualified_name) tacname in
let args = args |> List.map (fun (arg,_) -> Rocq_elpi_arg_HOAS.Tac.Term(arg)) in
let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Rocq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in
(TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in
CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit wit_ltac_in_term) (CAst.make tac)) in
let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in
Pcoq.grammar_extend Pcoq.Constr.term (Pcoq.Fresh
(Gramlib.Gramext.Before "10",
[ (None, None, [ Pcoq.Production.make
(Pcoq.Rule.next rule (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg)))
action
])]))
let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = {
abbrev_name;
tac_name;
tac_fixed_args = List.map (Rocq_elpi_arg_HOAS.Tac.subst subst) tac_fixed_args
}
let inAbbreviationForTactic : tac_abbrev -> Libobject.obj =
Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED-TAC-ABBREV"
~cache:cache_abbrev_for_tac ~subst:(Some subst_abbrev_for_tac)Indeed it changes the grammar. My question is: can I achieve the same without changing the grammare? |
|
I think the
part is currently not possible without changing the grammar. Maybe we could extend the abbreviation system to support it but I'm not sure of the details. EDIT: supporting a non-ident abbrev_name is also not possible with current abbreviations |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hopefully detects issues like
https://rocq-prover.zulipchat.com/#narrow/channel/237662-VsCoq-devs-.26-users/topic/.E2.9C.94.20VSCoq.20resetting.20a.20lot.20on.202.2E2.2E5/near/520048311