Performance difference between pmaps and gmaps using vm_compute
There can be vast differences in performance between the use of
gmap for a sequence of inserts followed by a lookup.
Here is an example, using Coq 8.9.1 and std++ version 1.2.1:
From stdpp Require Import pmap gmap list fin_maps. Open Scope Z_scope. Definition big_list_pos := map (fun x => (Z.to_pos x, x)) (seqZ 0 5000). Definition big_map_pos : Pmap Z := list_to_map big_list_pos. Definition big_list := map (fun x => (x, x)) (seqZ 0 5000). Definition big_map : gmap Z Z := list_to_map big_list. Goal (lookup (50%positive) big_map_pos = Some 50). Proof. (* Time reflexivity. (* ~ 30 seconds *) *) Time vm_compute. (* < 1 second *) (* Time native_compute. (* 0.2 seconds *) *) reflexivity. Qed. Goal (lookup 50 big_map = Some 50). Proof. (* Time reflexivity. (* ~ 30 seconds *) *) Time vm_compute. (* Waited for ~3 minutes before giving up *) (* Time native_compute. (* same *) *) reflexivity. Qed.
Paolo seems to suggest here that the issue is the transparency of the second field of
Gmap, though it's unclear to me how opaque that can be made.