Gmalecha/attributes on hooks#15
Closed
gmalecha-at-skylabs wants to merge 946 commits into
Closed
Conversation
Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
The main change is that we now split the function producing the unicode point into one computing the UTF8 size and one actually producing the code point. This allows making the code allocation-free, which is important for this kind of low-level functions.
…s, error if any issues found Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
…tion. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
(we only use it for its directory so it doesn't matter which one we use)
on master _build_ci got moved to saved_build_ci so the path in the deploy job was incorrect. Alternatively we could set save_build_ci and change the path in the deploy job.
We add a int uid to QGlobal.t, generated by safe_typing when adding the sort. The id is then useless so we remove it. The APIs change from combined `Global.push_qualities : QGlobal.Set.t * ElimConstraints.t -> unit` to separate `Global.new_global_sort : unit -> QGlobal.t` and `Global.merge_elim_constraints : ElimConstraints.t -> unit`. Fix rocq-prover#21717
…instead of coqc Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
We only need the constraints between the preexisting universes which are mentioned by new constraints (including implicit Set >= new univ constraints). Close rocq-prover#17523 (tested on the artificial example)
Using a shell script to greedily consume jobserver tokens. In principle we could also use it for dune build and remake calls in CI jobs.
Some of the data stored was never used.
This function was using spaghetti mutable code to simply carry along some well-scoped data. The new code is still not perfect and in particular, not efficient, but at least it is more readable. Up to involutary bugs, this commit should be semantic-preserving.
We avoid useless translations of data structures.
… parts of the graph Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Reviewed-by: proux01 Co-authored-by: proux01 <proux01@users.noreply.github.com>
The previous attempt changed both the copied path and the saved path so they continued to disagree. This commit only changes 1 of them so now they should agree.
Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
…ispatching Reviewed-by: thomas-lamiaux Co-authored-by: thomas-lamiaux <thomas-lamiaux@users.noreply.github.com>
… this time?) Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
OCaml channels have a built-in buffer that happens to be useless in our case, since lexbuf internals always read the data into its own buffer. Such implicit buffers are not great for memory consumption and tend in particular to live too long because they are custom blocks. We solve this by reading from the raw unix descriptor instead.
This function is performance critical for rocqdep parsing, as it reads most file contents except for Require data. The ocamllex generated function is not very efficient for this kind of dumb code, as it relies on a transition table and performs lexing on a per-character basis. We implement our own hand-writter lexer for this function, which tries to be as fast as possible by gobbling up all non-special characters in a single run without trying to refill the buffer. We could probably do better by exploiting SIMD instructions but OCaml does not seem to be able to generate this kind of code.
We extrude a costly file creation outside of a loop.
This is bad algorithmics as list concatenation is O(n) and we only need the resulting list for iteration. Instead, we use an ad-hoc tree datatype to store the result in O(1).
These are costly for no good reason, since we immediately print them after allocation.
…ed in separate modules Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
… variables and use this info to fix bugs Reviewed-by: gares Ack-by: yannl35133 Co-authored-by: gares <gares@users.noreply.github.com>
In the kernel we check the section variables used in another way (eg Constant_typing.check_section_variables)
…w.r.t. template levels. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
While this is currently unused, I had the need to have this function available in several POCs. For API expressivity and uniformity it does not hurt to expose it by default.
The internal details were barely used and should have been considered bad practice anyway. A good part of the reason for keeping the type transparent was likely to please serapi but this is now unnecessary.
…n rewrite fails Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
…ypes. Reviewed-by: SkySkimmer Reviewed-by: gares Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Fixes rocq-prover#22086 These patches enforce recording appropriate universe unifications in [unfold], [unlock] and [rw]. The matching phase for multiple occcurrences of a pattern is now done accumulating the necessary universe constraints.
…tially missing univ constraints
…tially missing univ constraints Also avoids an unecessary repeated call to solve_evars.
Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Reviewed-by: ppedrot Reviewed-by: PierreCorbineau Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
…handling Reviewed-by: gares Co-authored-by: gares <gares@users.noreply.github.com>
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 8fc3ef1 |
| fmdeps/BRiCk/ | main | 0136f2a |
| fmdeps/auto/ | main | 2a44deb |
| fmdeps/auto-docs/ | main | 2a67550 |
| bluerock/NOVA/ | skylabs-proof | f5ab5b0 |
| bluerock/bhv/ | skylabs-main | 54e9d1e |
| fmdeps/brick-libcpp/ | main | e41ed34 |
| fmdeps/ci/ | main | a8a51ea |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | 55aec02 |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | ca817a8 |
| fmdeps/rocq-agent-toolkit/ | main | 186cc3f |
| vendored/rocq-elpi/ | skylabs-master | 49a4a74 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 54a3e53 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.11% | 129259.5 | 129397.6 | +138.1 | total |
| -0.01% | 23462.1 | 23458.7 | -3.5 | ├ translation units |
| +0.13% | 105797.4 | 105939.0 | +141.6 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -16.77% | 11.3 | 9.4 | -1.9 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -0.83% | 196.8 | 195.1 | -1.6 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| +0.13% | 850.9 | 852.0 | +1.1 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| +0.14% | 758.0 | 759.0 | +1.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| +0.16% | 1805.9 | 1808.7 | +2.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| +0.16% | 929.2 | 930.7 | +1.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| +0.17% | 964.2 | 965.9 | +1.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| +0.20% | 871.7 | 873.4 | +1.8 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v |
| +0.23% | 530.3 | 531.5 | +1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| +0.24% | 538.2 | 539.5 | +1.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| +0.25% | 520.9 | 522.2 | +1.3 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| +0.26% | 474.1 | 475.4 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| +0.35% | 455.6 | 457.1 | +1.6 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| +0.37% | 338.9 | 340.1 | +1.3 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/dn.v |
| +0.40% | 472.6 | 474.5 | +1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| +0.41% | 1132.2 | 1136.8 | +4.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| +0.42% | 327.8 | 329.2 | +1.4 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v |
| +0.43% | 544.0 | 546.3 | +2.3 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| +0.47% | 347.9 | 349.5 | +1.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| +0.47% | 331.4 | 332.9 | +1.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| +0.53% | 259.9 | 261.3 | +1.4 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.54% | 227.4 | 228.6 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v |
| +0.54% | 207.4 | 208.6 | +1.1 | bluerock/bhv/apps/vmm/proof/main_cpp_spec.v |
| +0.58% | 339.7 | 341.7 | +2.0 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| +0.60% | 205.6 | 206.8 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| +0.62% | 197.6 | 198.8 | +1.2 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| +0.65% | 299.0 | 301.0 | +1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v |
| +0.73% | 191.0 | 192.4 | +1.4 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| +0.75% | 220.4 | 222.1 | +1.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| +0.75% | 167.6 | 168.8 | +1.3 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v |
| +0.76% | 162.8 | 164.0 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/reset.v |
| +0.78% | 138.6 | 139.7 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v |
| +0.82% | 142.8 | 143.9 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_msr_exit.v |
| +0.88% | 140.8 | 142.1 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v |
| +0.88% | 148.0 | 149.4 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| +0.88% | 144.9 | 146.1 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_cpp_proof.v |
| +0.89% | 143.3 | 144.6 | +1.3 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| +0.91% | 120.4 | 121.5 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v |
| +0.92% | 138.5 | 139.8 | +1.3 | bluerock/NOVA/build-proof/proof/iface/hypercall/pd.v |
| +0.99% | 124.2 | 125.5 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +0.99% | 132.2 | 133.6 | +1.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| +1.10% | 105.7 | 106.8 | +1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sc.v |
| +1.12% | 110.3 | 111.6 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/startup.v |
| +1.13% | 145.5 | 147.2 | +1.7 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/create.v |
| +1.19% | 94.3 | 95.4 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v |
| +1.20% | 115.2 | 116.5 | +1.4 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pt.v |
| +1.24% | 106.3 | 107.6 | +1.3 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v |
| +1.25% | 130.8 | 132.4 | +1.6 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v |
| +1.28% | 95.2 | 96.4 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| +1.30% | 121.3 | 122.9 | +1.6 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v |
| +1.31% | 92.7 | 93.9 | +1.2 | bluerock/bhv/apps/vswitch/proof/model/vswitch/lemmas.v |
| +1.35% | 90.3 | 91.5 | +1.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v |
| +1.37% | 122.4 | 124.1 | +1.7 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/init_info.v |
| +1.45% | 109.7 | 111.3 | +1.6 | bluerock/NOVA/build-proof/proof/syscall_hpp_proof.v |
| +1.45% | 83.8 | 85.0 | +1.2 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/private_dequeue.v |
| +1.52% | 121.3 | 123.1 | +1.8 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v |
| +1.61% | 70.3 | 71.4 | +1.1 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v |
| +1.70% | 73.0 | 74.3 | +1.2 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/client_dequeue.v |
| +1.70% | 86.6 | 88.1 | +1.5 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| +1.71% | 72.9 | 74.2 | +1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_finish.v |
| +1.83% | 231.2 | 235.4 | +4.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| +1.90% | 60.3 | 61.5 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| +1.93% | 63.2 | 64.4 | +1.2 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v |
| +1.98% | 85.5 | 87.2 | +1.7 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/proof.v |
| +2.01% | 123.1 | 125.5 | +2.5 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v |
| +2.07% | 65.6 | 67.0 | +1.4 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/unblock.v |
| +2.09% | 50.1 | 51.2 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v |
| +2.10% | 85.9 | 87.7 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +2.15% | 108.6 | 110.9 | +2.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +2.35% | 51.2 | 52.4 | +1.2 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v |
| +2.50% | 65.4 | 67.0 | +1.6 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/defs.v |
| +2.54% | 41.2 | 42.2 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v |
| +2.56% | 65.1 | 66.8 | +1.7 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume_all.v |
| +2.57% | 47.6 | 48.8 | +1.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v |
| +2.71% | 83.1 | 85.3 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| +2.71% | 51.4 | 52.8 | +1.4 | bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/proof.v |
| +2.72% | 43.0 | 44.2 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v |
| +2.82% | 45.0 | 46.2 | +1.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v |
| +3.02% | 37.4 | 38.5 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/descriptor/misc.v |
| +3.06% | 41.6 | 42.8 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v |
| +3.15% | 72.5 | 74.8 | +2.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v |
| +3.46% | 53.9 | 55.8 | +1.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v |
| +3.59% | 35.3 | 36.6 | +1.3 | bluerock/NOVA/build-proof/proof/refcnt_hpp_proof.v |
| +4.03% | 30.8 | 32.1 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_specs.v |
| +4.65% | 29.0 | 30.4 | +1.4 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/prelude.v |
| +5.42% | 57.3 | 60.4 | +3.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| +6.01% | 26.7 | 28.3 | +1.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/is_size_valid.v |
| +6.09% | 48.9 | 51.9 | +3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v |
| +6.79% | 25.1 | 26.8 | +1.7 | bluerock/NOVA/build-proof/proof/space_hpp_proof.v |
| +0.11% | 129259.5 | 129397.6 | +138.1 | total |
| -0.01% | 23462.1 | 23458.7 | -3.5 | ├ translation units |
| +0.13% | 105797.4 | 105939.0 | +141.6 | └ proofs and tests |
| (* - visibility (optional) one of [local], [export] or [global]; *) | ||
| (* omitted behaves like a plain [Hint Resolve] (i.e. *) | ||
| (* [local] inside a section, [export] otherwise). *) | ||
| (************************************************************************) |
There was a problem hiding this comment.
This comment does not answer whether hint patterns are supported. Please extend the comment.
(I don't think we can write terms or patterns in attributes, but I could be wrong)
There was a problem hiding this comment.
But to be clear, it seems an acceptable limitation, I'd just like to know.
Author
There was a problem hiding this comment.
Not supported, and I think for the reason that you can not have terms in attributes. We could see if we could relax that restriction, but it would be separate.
Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
This is a trivial quality of life improvement.
… output. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
gmalecha-at-skylabs
force-pushed
the
gmalecha/attributes-on-hooks
branch
from
52cc4bb to
7fe364c
Compare
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
15 participants
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.
This is an idea to extend the programmable attributes of Rocq and implement a
#[hint(...)]attribute that will automatically add a hint to a hint database when the lemma is finalized.