From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Andreas Politz Newsgroups: gmane.emacs.bugs Subject: bug#58158: 29.0.50; [overlay] Interval tree iteration considered harmful Date: Tue, 4 Oct 2022 12:50:54 +0200 Message-ID: <7B9B9541-E1D3-4553-BE8D-5197D3CB1018@andreas-politz.de> References: Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="1759"; mail-complaints-to="usenet@ciao.gmane.io" Cc: Eli Zaretskii , 58158@debbugs.gnu.org, Stefan Monnier To: Gerd =?UTF-8?Q?M=C3=B6llmann?= Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Tue Oct 04 13:19:21 2022 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1offxI-0000DR-T9 for geb-bug-gnu-emacs@m.gmane-mx.org; Tue, 04 Oct 2022 13:19:20 +0200 Original-Received: from localhost ([::1]:59818 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1offxH-0004DX-Tx for geb-bug-gnu-emacs@m.gmane-mx.org; Tue, 04 Oct 2022 07:19:19 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:60566) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1offkT-00018T-57 for bug-gnu-emacs@gnu.org; Tue, 04 Oct 2022 07:06:06 -0400 Original-Received: from debbugs.gnu.org ([209.51.188.43]:53585) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1offkS-0004Il-T9 for bug-gnu-emacs@gnu.org; Tue, 04 Oct 2022 07:06:04 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1offkS-0004Mu-Ni for bug-gnu-emacs@gnu.org; Tue, 04 Oct 2022 07:06:04 -0400 X-Loop: help-debbugs@gnu.org Resent-From: Andreas Politz Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Tue, 04 Oct 2022 11:06:04 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 58158 X-GNU-PR-Package: emacs Original-Received: via spool by 58158-submit@debbugs.gnu.org id=B58158.166488151816665 (code B ref 58158); Tue, 04 Oct 2022 11:06:04 +0000 Original-Received: (at 58158) by debbugs.gnu.org; 4 Oct 2022 11:05:18 +0000 Original-Received: from localhost ([127.0.0.1]:52648 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1offjh-0004Ke-RY for submit@debbugs.gnu.org; Tue, 04 Oct 2022 07:05:18 -0400 Original-Received: from mout.kundenserver.de ([212.227.17.13]:44571) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1offW0-0001lJ-Vm for 58158@debbugs.gnu.org; Tue, 04 Oct 2022 06:51:09 -0400 Original-Received: from smtpclient.apple ([77.179.162.75]) by mrelayeu.kundenserver.de (mreue109 [213.165.67.113]) with ESMTPSA (Nemesis) id 1MzQc2-1pSFt41yeu-00vOmH; Tue, 04 Oct 2022 12:50:58 +0200 In-Reply-To: X-Mailer: iPad Mail (19G82) X-Provags-ID: V03:K1:mWBVn8vHSxVVkx34Zk3YgZZW86yWkxc5Fa5QedFuBphb0F4M4jP LvUTY/i5gwIX2NUIFD8QyRJXyvW/WB2jvhgW3Y1na8xe8hU5rcpqPPQ3N8Q1VGKEoJXIBpg ufT8NJ9ga5K6s4q9k/BcwEqHVuvPgZswVSj8PFnEFVovovnHrUGrvNHHftaNql3SOj2Pk06 3avMgSiQ5mWU8sEeoFY9A== X-UI-Out-Filterresults: notjunk:1;V03:K0:U9FHf1GoFhY=:C5izIiVVlNFN8TB2xJdGNr pY7P6rIlLGcHBbm7A1f297MuJ3zzggShBkpb67mJNbXiybiRyozfF60hvhX9MFWqI5RI6W4Wb zApl3TCV3f03YaAhlFDATkKgj4fqVEkI7bI4trKpnpZI9Ev5DOua3Y3OcrRsiSwWs3p24hqkm X3QVgPLexvqt0oo3BX+iu+ICs3iatWfBE5ktgdH7DjZ5a+CNYBRhgjjvNJrd8lgUL0IqG1NUn PFQuZ2J4TyO8V7xQDeIykO8NnrEDyRq73M7aoxR+0OZXg5+e4kwUzpWFUq10BYVYLdQNohzHD tZ2SrM1/8ih7V2oeVQjwiGqHhZMHYZ+gqzEBlaUMH9T4+iMOYc3w9ckM/eSIs3g7cla6DYTZS vJ7uxlnsxrLXNu8VJRhtAlOFslQ8/HtB3zOnn1TmT4VrgtkTHTftfzTt+22qJfq9RQau0Jrz6 TtCpBDJF0GKBKPDQnOSPcmTTcHz5DaCTT/+4aV+5iP+erlZMjqx3IM4ZWTCc4V45HHJUGcQJN 04wETxi+0HW4UtPfLmBevfwEFjxV5FB4dP0v0ExecyZnY1ixwZNLSFUl7UqyPA2VtYMvigN9j iJHRIPS8P5VEpSZgrAohnZZ8GTkIcRVUq46OxzI7oejSkkVr07SpWCMk20uh5I45Z2wMJCcGN stKPns+VA0oJWbN/Avnjga5l6RmzcnY5ogjmCTjZyqHH3R63eGV6ek+lC+H8rgujv/QsrJbEr b4m0fVpaTmDukwjZdxkdFpNaivMFik93126JOFYvNZ6OHcl/RRvIiFX6FsIsF19OXkdzux+w X-Mailman-Approved-At: Tue, 04 Oct 2022 07:05:12 -0400 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.io gmane.emacs.bugs:244399 Archived-At: My implementation seems to work. The correctness of the algorithm would foll= ow from=20 1. The Rb tree algorithm produces a tree with left <=3D root <=3D right, 2. the algorithm you=E2=80=99ve posted, and I=E2=80=99ve adapted, produces a= n in=E2=80=93order of the tree and 3. the conditions guiding the traversal are correct, i.e. they don=E2=80=99t= exclude matching intervals. Since I believe these statements are true, I believe the algorithm is correc= t. Andreas > Am 03.10.2022 um 06:35 schrieb Gerd M=C3=B6llmann : >=20 > =EF=BB=BFAndreas Politz writes: >=20 >> It seems to work, at least buffer-tests are passing. >=20 > "seems to work" is a bit weak. Can we prove it? >=20 > I don't mean mathematically, but by reasoning like I tried in the > comments in successor function I posted,